Skip to content

Commit 8379bd1

Browse files
W95PspNadrieril
W95Psp
authored and
Nadrieril
committed
chore(rustc-tests): update snapshots
1 parent 0fd5b75 commit 8379bd1

24 files changed

+268
-225
lines changed

‎rustc-coverage-tests/snapshots/fstar/Coverage.Abort.fst‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -7,15 +7,15 @@ let might_abort (should_abort: bool) : Prims.unit =
77
if should_abort
88
then
99
let _:Prims.unit =
10-
Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
10+
Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
1111
(let list = ["aborting...\n"] in
1212
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
1313
Rust_primitives.Hax.array_of_list 1 list)
1414
<:
1515
Core.Fmt.t_Arguments)
1616
in
1717
let _:Prims.unit = () in
18-
Rust_primitives.Hax.never_to_any (Core.Panicking.panic_fmt (Core.Fmt.Rt.impl_2__new_const (mk_usize
18+
Rust_primitives.Hax.never_to_any (Core.Panicking.panic_fmt (Core.Fmt.Rt.impl_1__new_const (mk_usize
1919
1)
2020
(let list = ["panics and aborts"] in
2121
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
@@ -26,7 +26,7 @@ let might_abort (should_abort: bool) : Prims.unit =
2626
Rust_primitives.Hax.t_Never)
2727
else
2828
let _:Prims.unit =
29-
Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
29+
Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
3030
(let list = ["Don't Panic\n"] in
3131
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
3232
Rust_primitives.Hax.array_of_list 1 list)

‎rustc-coverage-tests/snapshots/fstar/Coverage.Assert.fst‎

Lines changed: 7 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -4,15 +4,18 @@ open Core
44
open FStar.Mul
55

66
let might_fail_assert (one_plus_one: u32) : Prims.unit =
7+
let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) =
8+
let list = [Core.Fmt.Rt.impl__new_display #u32 one_plus_one] in
9+
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
10+
Rust_primitives.Hax.array_of_list 1 list
11+
in
712
let _:Prims.unit =
8-
Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2)
13+
Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2)
914
(mk_usize 1)
1015
(let list = ["does 1 + 1 = "; "?\n"] in
1116
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
1217
Rust_primitives.Hax.array_of_list 2 list)
13-
(let list = [Core.Fmt.Rt.impl__new_display #u32 one_plus_one <: Core.Fmt.Rt.t_Argument] in
14-
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
15-
Rust_primitives.Hax.array_of_list 1 list)
18+
args
1619
<:
1720
Core.Fmt.t_Arguments)
1821
in

‎rustc-coverage-tests/snapshots/fstar/Coverage.Attr.Trait_impl_inherit.fst‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ open FStar.Mul
77
Last available AST for this item:
88
99
#[path()]#[<cfg>(any(feature = "json"))]#[feature(coverage_attribute)]#[<cfg>(any(feature = "json", feature = "fstar", feature = "fstar-lax", feature =
10-
"coq"))]#[feature(coverage_attribute)]#[allow(unused_attributes)]#[allow(dead_code)]#[allow(unreachable_code)]#[feature(register_tool)]#[register_tool(_hax)]trait t_T<Self_>{fn f_f((self: Self)) -> tuple0{{let _: tuple0 = {std::io::stdio::e_print(core::fmt::rt::impl_2__new_const::<generic_value!(todo)>(["default\n"]))};{let _: tuple0 = {Tuple0};Tuple0}}}}
10+
"coq"))]#[feature(coverage_attribute)]#[allow(unused_attributes)]#[allow(dead_code)]#[allow(unreachable_code)]#[feature(register_tool)]#[register_tool(_hax)]trait t_T<Self_>{fn f_f((self: Self)) -> tuple0{{let _: tuple0 = {std::io::stdio::e_print(core::fmt::rt::impl_1__new_const::<generic_value!(todo)>(["default\n"]))};{let _: tuple0 = {Tuple0};Tuple0}}}}
1111
1212
Last AST:
1313
/** print_rust: pitem: not implemented (item: { Concrete_ident.T.def_id =
@@ -74,7 +74,7 @@ let impl: t_T t_S =
7474
=
7575
fun (self: t_S) ->
7676
let _:Prims.unit =
77-
Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
77+
Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
7878
(let list = ["impl S\n"] in
7979
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
8080
Rust_primitives.Hax.array_of_list 1 list)

‎rustc-coverage-tests/snapshots/fstar/Coverage.Auxiliary.Used_crate.fst‎

Lines changed: 35 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -14,15 +14,18 @@ let used_only_from_bin_crate_generic_function
1414
(#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Fmt.t_Debug v_T)
1515
(arg: v_T)
1616
: Prims.unit =
17+
let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) =
18+
let list = [Core.Fmt.Rt.impl__new_debug #v_T arg] in
19+
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
20+
Rust_primitives.Hax.array_of_list 1 list
21+
in
1722
let _:Prims.unit =
18-
Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2)
23+
Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2)
1924
(mk_usize 1)
2025
(let list = ["used_only_from_bin_crate_generic_function with "; "\n"] in
2126
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
2227
Rust_primitives.Hax.array_of_list 2 list)
23-
(let list = [Core.Fmt.Rt.impl__new_debug #v_T arg <: Core.Fmt.Rt.t_Argument] in
24-
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
25-
Rust_primitives.Hax.array_of_list 1 list)
28+
args
2629
<:
2730
Core.Fmt.t_Arguments)
2831
in
@@ -34,15 +37,18 @@ let used_only_from_this_lib_crate_generic_function
3437
(#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Fmt.t_Debug v_T)
3538
(arg: v_T)
3639
: Prims.unit =
40+
let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) =
41+
let list = [Core.Fmt.Rt.impl__new_debug #v_T arg] in
42+
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
43+
Rust_primitives.Hax.array_of_list 1 list
44+
in
3745
let _:Prims.unit =
38-
Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2)
46+
Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2)
3947
(mk_usize 1)
4048
(let list = ["used_only_from_this_lib_crate_generic_function with "; "\n"] in
4149
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
4250
Rust_primitives.Hax.array_of_list 2 list)
43-
(let list = [Core.Fmt.Rt.impl__new_debug #v_T arg <: Core.Fmt.Rt.t_Argument] in
44-
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
45-
Rust_primitives.Hax.array_of_list 1 list)
51+
args
4652
<:
4753
Core.Fmt.t_Arguments)
4854
in
@@ -54,15 +60,18 @@ let used_from_bin_crate_and_lib_crate_generic_function
5460
(#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Fmt.t_Debug v_T)
5561
(arg: v_T)
5662
: Prims.unit =
63+
let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) =
64+
let list = [Core.Fmt.Rt.impl__new_debug #v_T arg] in
65+
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
66+
Rust_primitives.Hax.array_of_list 1 list
67+
in
5768
let _:Prims.unit =
58-
Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2)
69+
Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2)
5970
(mk_usize 1)
6071
(let list = ["used_from_bin_crate_and_lib_crate_generic_function with "; "\n"] in
6172
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
6273
Rust_primitives.Hax.array_of_list 2 list)
63-
(let list = [Core.Fmt.Rt.impl__new_debug #v_T arg <: Core.Fmt.Rt.t_Argument] in
64-
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
65-
Rust_primitives.Hax.array_of_list 1 list)
74+
args
6675
<:
6776
Core.Fmt.t_Arguments)
6877
in
@@ -74,17 +83,20 @@ let used_with_same_type_from_bin_crate_and_lib_crate_generic_function
7483
(#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Fmt.t_Debug v_T)
7584
(arg: v_T)
7685
: Prims.unit =
86+
let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) =
87+
let list = [Core.Fmt.Rt.impl__new_debug #v_T arg] in
88+
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
89+
Rust_primitives.Hax.array_of_list 1 list
90+
in
7791
let _:Prims.unit =
78-
Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2)
92+
Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2)
7993
(mk_usize 1)
8094
(let list =
8195
["used_with_same_type_from_bin_crate_and_lib_crate_generic_function with "; "\n"]
8296
in
8397
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
8498
Rust_primitives.Hax.array_of_list 2 list)
85-
(let list = [Core.Fmt.Rt.impl__new_debug #v_T arg <: Core.Fmt.Rt.t_Argument] in
86-
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
87-
Rust_primitives.Hax.array_of_list 1 list)
99+
args
88100
<:
89101
Core.Fmt.t_Arguments)
90102
in
@@ -96,15 +108,18 @@ let unused_generic_function
96108
(#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Fmt.t_Debug v_T)
97109
(arg: v_T)
98110
: Prims.unit =
111+
let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) =
112+
let list = [Core.Fmt.Rt.impl__new_debug #v_T arg] in
113+
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
114+
Rust_primitives.Hax.array_of_list 1 list
115+
in
99116
let _:Prims.unit =
100-
Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2)
117+
Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2)
101118
(mk_usize 1)
102119
(let list = ["unused_generic_function with "; "\n"] in
103120
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
104121
Rust_primitives.Hax.array_of_list 2 list)
105-
(let list = [Core.Fmt.Rt.impl__new_debug #v_T arg <: Core.Fmt.Rt.t_Argument] in
106-
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
107-
Rust_primitives.Hax.array_of_list 1 list)
122+
args
108123
<:
109124
Core.Fmt.t_Arguments)
110125
in

‎rustc-coverage-tests/snapshots/fstar/Coverage.Auxiliary.Used_inline_crate.fst‎

Lines changed: 35 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -14,15 +14,18 @@ let used_only_from_bin_crate_generic_function
1414
(#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Fmt.t_Debug v_T)
1515
(arg: v_T)
1616
: Prims.unit =
17+
let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) =
18+
let list = [Core.Fmt.Rt.impl__new_debug #v_T arg] in
19+
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
20+
Rust_primitives.Hax.array_of_list 1 list
21+
in
1722
let _:Prims.unit =
18-
Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2)
23+
Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2)
1924
(mk_usize 1)
2025
(let list = ["used_only_from_bin_crate_generic_function with "; "\n"] in
2126
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
2227
Rust_primitives.Hax.array_of_list 2 list)
23-
(let list = [Core.Fmt.Rt.impl__new_debug #v_T arg <: Core.Fmt.Rt.t_Argument] in
24-
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
25-
Rust_primitives.Hax.array_of_list 1 list)
28+
args
2629
<:
2730
Core.Fmt.t_Arguments)
2831
in
@@ -34,15 +37,18 @@ let used_only_from_this_lib_crate_generic_function
3437
(#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Fmt.t_Debug v_T)
3538
(arg: v_T)
3639
: Prims.unit =
40+
let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) =
41+
let list = [Core.Fmt.Rt.impl__new_debug #v_T arg] in
42+
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
43+
Rust_primitives.Hax.array_of_list 1 list
44+
in
3745
let _:Prims.unit =
38-
Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2)
46+
Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2)
3947
(mk_usize 1)
4048
(let list = ["used_only_from_this_lib_crate_generic_function with "; "\n"] in
4149
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
4250
Rust_primitives.Hax.array_of_list 2 list)
43-
(let list = [Core.Fmt.Rt.impl__new_debug #v_T arg <: Core.Fmt.Rt.t_Argument] in
44-
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
45-
Rust_primitives.Hax.array_of_list 1 list)
51+
args
4652
<:
4753
Core.Fmt.t_Arguments)
4854
in
@@ -54,15 +60,18 @@ let used_from_bin_crate_and_lib_crate_generic_function
5460
(#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Fmt.t_Debug v_T)
5561
(arg: v_T)
5662
: Prims.unit =
63+
let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) =
64+
let list = [Core.Fmt.Rt.impl__new_debug #v_T arg] in
65+
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
66+
Rust_primitives.Hax.array_of_list 1 list
67+
in
5768
let _:Prims.unit =
58-
Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2)
69+
Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2)
5970
(mk_usize 1)
6071
(let list = ["used_from_bin_crate_and_lib_crate_generic_function with "; "\n"] in
6172
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
6273
Rust_primitives.Hax.array_of_list 2 list)
63-
(let list = [Core.Fmt.Rt.impl__new_debug #v_T arg <: Core.Fmt.Rt.t_Argument] in
64-
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
65-
Rust_primitives.Hax.array_of_list 1 list)
74+
args
6675
<:
6776
Core.Fmt.t_Arguments)
6877
in
@@ -74,17 +83,20 @@ let used_with_same_type_from_bin_crate_and_lib_crate_generic_function
7483
(#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Fmt.t_Debug v_T)
7584
(arg: v_T)
7685
: Prims.unit =
86+
let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) =
87+
let list = [Core.Fmt.Rt.impl__new_debug #v_T arg] in
88+
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
89+
Rust_primitives.Hax.array_of_list 1 list
90+
in
7791
let _:Prims.unit =
78-
Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2)
92+
Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2)
7993
(mk_usize 1)
8094
(let list =
8195
["used_with_same_type_from_bin_crate_and_lib_crate_generic_function with "; "\n"]
8296
in
8397
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
8498
Rust_primitives.Hax.array_of_list 2 list)
85-
(let list = [Core.Fmt.Rt.impl__new_debug #v_T arg <: Core.Fmt.Rt.t_Argument] in
86-
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
87-
Rust_primitives.Hax.array_of_list 1 list)
99+
args
88100
<:
89101
Core.Fmt.t_Arguments)
90102
in
@@ -96,15 +108,18 @@ let unused_generic_function
96108
(#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Fmt.t_Debug v_T)
97109
(arg: v_T)
98110
: Prims.unit =
111+
let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) =
112+
let list = [Core.Fmt.Rt.impl__new_debug #v_T arg] in
113+
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
114+
Rust_primitives.Hax.array_of_list 1 list
115+
in
99116
let _:Prims.unit =
100-
Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2)
117+
Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2)
101118
(mk_usize 1)
102119
(let list = ["unused_generic_function with "; "\n"] in
103120
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
104121
Rust_primitives.Hax.array_of_list 2 list)
105-
(let list = [Core.Fmt.Rt.impl__new_debug #v_T arg <: Core.Fmt.Rt.t_Argument] in
106-
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
107-
Rust_primitives.Hax.array_of_list 1 list)
122+
args
108123
<:
109124
Core.Fmt.t_Arguments)
110125
in

‎rustc-coverage-tests/snapshots/fstar/Coverage.Closure_macro.fst‎

Lines changed: 17 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ let load_configuration_files (_: Prims.unit)
1212

1313
let main (_: Prims.unit) : Core.Result.t_Result Prims.unit Alloc.String.t_String =
1414
let _:Prims.unit =
15-
Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
15+
Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
1616
(let list = ["Starting service\n"] in
1717
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
1818
Rust_primitives.Hax.array_of_list 1 list)
@@ -29,44 +29,38 @@ let main (_: Prims.unit) : Core.Result.t_Result Prims.unit Alloc.String.t_String
2929
Core.Result.t_Result Alloc.String.t_String Alloc.String.t_String)
3030
(fun e ->
3131
let e:Alloc.String.t_String = e in
32+
let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) =
33+
let list = [Core.Fmt.Rt.impl__new_display #Alloc.String.t_String e] in
34+
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
35+
Rust_primitives.Hax.array_of_list 1 list
36+
in
3237
let message:Alloc.String.t_String =
3338
Core.Hint.must_use #Alloc.String.t_String
34-
(Alloc.Fmt.format (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 1)
39+
(Alloc.Fmt.format (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 1)
3540
(mk_usize 1)
3641
(let list = ["Error loading configs: "] in
3742
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
3843
Rust_primitives.Hax.array_of_list 1 list)
39-
(let list =
40-
[
41-
Core.Fmt.Rt.impl__new_display #Alloc.String.t_String e
42-
<:
43-
Core.Fmt.Rt.t_Argument
44-
]
45-
in
46-
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
47-
Rust_primitives.Hax.array_of_list 1 list)
44+
args
4845
<:
4946
Core.Fmt.t_Arguments)
5047
<:
5148
Alloc.String.t_String)
5249
in
5350
if (Alloc.String.impl_String__len message <: usize) >. mk_usize 0
5451
then
52+
let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) =
53+
let list = [Core.Fmt.Rt.impl__new_display #Alloc.String.t_String message] in
54+
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
55+
Rust_primitives.Hax.array_of_list 1 list
56+
in
5557
let _:Prims.unit =
56-
Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2)
58+
Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2)
5759
(mk_usize 1)
5860
(let list = [""; "\n"] in
5961
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
6062
Rust_primitives.Hax.array_of_list 2 list)
61-
(let list =
62-
[
63-
Core.Fmt.Rt.impl__new_display #Alloc.String.t_String message
64-
<:
65-
Core.Fmt.Rt.t_Argument
66-
]
67-
in
68-
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
69-
Rust_primitives.Hax.array_of_list 1 list)
63+
args
7064
<:
7165
Core.Fmt.t_Arguments)
7266
in
@@ -83,7 +77,7 @@ let main (_: Prims.unit) : Core.Result.t_Result Prims.unit Alloc.String.t_String
8377
if (Core.Str.impl_str__len "error" <: usize) >. mk_usize 0
8478
then
8579
let _:Prims.unit =
86-
Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
80+
Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
8781
(let list = ["no msg\n"] in
8882
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
8983
Rust_primitives.Hax.array_of_list 1 list)
@@ -94,7 +88,7 @@ let main (_: Prims.unit) : Core.Result.t_Result Prims.unit Alloc.String.t_String
9488
()
9589
else
9690
let _:Prims.unit =
97-
Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
91+
Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)
9892
(let list = ["error\n"] in
9993
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
10094
Rust_primitives.Hax.array_of_list 1 list)

0 commit comments

Comments
 (0)