Skip to content

Commit

Permalink
fix(tests): update snapshots
Browse files Browse the repository at this point in the history
  • Loading branch information
W95Psp committed Oct 28, 2024
1 parent 06b2071 commit 3be504d
Show file tree
Hide file tree
Showing 2 changed files with 26 additions and 6 deletions.
28 changes: 24 additions & 4 deletions test-harness/src/snapshots/toolchain__functions into-coq.snap
Original file line number Diff line number Diff line change
Expand Up @@ -20,10 +20,12 @@ info:
include_flag: ~
backend_options: ~
---
exit = 0

[stdout]
diagnostics = []
exit = 1
[[stdout.diagnostics]]
message = '''
(Coq backend) something is not implemented yet.
[ty] node typ'''
spans = ['Span { lo: Loc { line: 11, col: 4 }, hi: Loc { line: 17, col: 5 }, filename: Real(LocalPath("functions/src/lib.rs")), rust_span_data: None }']

[stdout.files]
"Functions.v" = '''
Expand All @@ -36,6 +38,8 @@ Open Scope bool_scope.

(*Not implemented yet? todo(item)*)

(*Not implemented yet? todo(item)*)

Definition calling_function_pointer__f (_ : unit) : unit :=
tt.

Expand All @@ -44,3 +48,19 @@ Definition calling_function_pointer (_ : unit) : unit :=
let _ := calling_function_pointer__f tt : unit in
tt.
'''
"Functions_Issue_1048_.v" = '''
(* File automatically generated by Hacspec *)
From Hacspec Require Import Hacspec_Lib MachineIntegers.
From Coq Require Import ZArith.
Import List.ListNotations.
Open Scope Z_scope.
Open Scope bool_scope.

Record t_CallableViaDeref : Type := {
}.

(*item error backend*)

Definition call_via_deref (_ : unit) : bool :=
f_deref CallableViaDereft_CallableViaDeref_t tt.
'''
4 changes: 2 additions & 2 deletions test-harness/src/snapshots/toolchain__traits into-fstar.snap
Original file line number Diff line number Diff line change
Expand Up @@ -387,11 +387,11 @@ let method_caller
()

class t_SubTrait (v_Self: Type0) (v_TypeArg: Type0) (v_ConstArg: usize) = {
[@@@ FStar.Tactics.Typeclasses.no_method]_super_8779313392680198588:t_Trait v_Self
[@@@ FStar.Tactics.Typeclasses.no_method]_super_11748868061750783190:t_Trait v_Self
v_TypeArg
v_ConstArg;
f_AssocType:Type0;
f_AssocType_6369404467997533198:t_Trait f_AssocType v_TypeArg v_ConstArg
f_AssocType_10469511598065652520:t_Trait f_AssocType v_TypeArg v_ConstArg
}
'''
"Traits.Interlaced_consts_types.fst" = '''
Expand Down

0 comments on commit 3be504d

Please sign in to comment.