Skip to content

Commit c47088c

Browse files
maximebuysemaximebuyse
committed
Fix rustc coverage tests for new rustc pin.
1 parent 0806201 commit c47088c

26 files changed

+151
-157
lines changed

‎hax-lib/proof-libs/fstar/core/Core.Fmt.Rt.fsti‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,11 @@ val impl_1__new_debug (#t:Type0) (x: t): t_Argument
77
val impl_4__new_v1_formatted (#t:Type0) (x: t) : t_Argument
88
val impl_1__new_binary (#t:Type0) (x: t) : t_Argument
99
val impl_1__new_lower_hex (#t:Type0) (x: t) : t_Argument
10+
val impl_2__new_const (#t:Type0) (#u:Type0) (xconst: t) (yconst: u): t_Argument
11+
val impl_2__new_v1 (#t1:Type0) (#t2:Type0) (#t3:Type0) (#t4:Type0)
12+
(x1: t1) (x2: t2) (x3: t3) (x4: t4) : t_Argument
13+
val impl__new_display (#t:Type0) (x: t): t_Argument
14+
val impl__new_debug (#t:Type0) (x: t): t_Argument
1015

1116
val impl_1__none : unit -> t_Array Core.Fmt.Rt.t_Argument (MkInt 0)
1217

‎hax-lib/proof-libs/fstar/core/Core.Fmt.fsti‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@ class t_Debug t_Self = {
1919
f_dbg_fmt: t_Self -> Core.Fmt.t_Formatter -> (Core.Fmt.t_Formatter & Core.Result.t_Result Prims.unit Core.Fmt.t_Error)
2020
}
2121

22-
val t_Arguments: Type0
22+
let t_Arguments = Rt.t_Argument
2323
val impl_4__new_v1 (sz1: usize) (sz2: usize) (pieces: t_Slice string) (args: t_Slice Core.Fmt.Rt.t_Argument): t_Arguments
2424
val impl_7__write_fmt (fmt: t_Formatter) (args: t_Arguments): t_Formatter & t_Result
2525
val impl_4__new_const (u:usize) (args: t_Slice string): t_Arguments

‎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.impl_4__new_const (mk_usize 1)
10+
Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__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.impl_4__new_const (mk_usize
18+
Rust_primitives.Hax.never_to_any (Core.Panicking.panic_fmt (Core.Fmt.Rt.impl_2__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.impl_4__new_const (mk_usize 1)
29+
Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__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: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -5,14 +5,12 @@ open FStar.Mul
55

66
let might_fail_assert (one_plus_one: u32) : Prims.unit =
77
let _:Prims.unit =
8-
Std.Io.Stdio.e_print (Core.Fmt.impl_4__new_v1 (mk_usize 2)
8+
Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2)
99
(mk_usize 1)
1010
(let list = ["does 1 + 1 = "; "?\n"] in
1111
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
1212
Rust_primitives.Hax.array_of_list 2 list)
13-
(let list =
14-
[Core.Fmt.Rt.impl_1__new_display #u32 one_plus_one <: Core.Fmt.Rt.t_Argument]
15-
in
13+
(let list = [Core.Fmt.Rt.impl__new_display #u32 one_plus_one <: Core.Fmt.Rt.t_Argument] in
1614
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
1715
Rust_primitives.Hax.array_of_list 1 list)
1816
<:

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

Lines changed: 9 additions & 10 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::impl_4__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_2__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 =
@@ -38,26 +38,25 @@ Last AST:
3838
}
3939
});
4040
path =
41-
[{ Types.data = (Types.TypeNs (Some "attr"));
41+
[{ Types.data = (Types.TypeNs "attr");
4242
disambiguator = 0 }
4343
]
4444
}
4545
}
4646
});
4747
path =
48-
[{ Types.data = (Types.TypeNs (Some "attr"));
49-
disambiguator = 0 };
50-
{ Types.data = (Types.TypeNs (Some "trait_impl_inherit"));
48+
[{ Types.data = (Types.TypeNs "attr"); disambiguator = 0 };
49+
{ Types.data = (Types.TypeNs "trait_impl_inherit");
5150
disambiguator = 0 }
5251
]
5352
}
5453
}
5554
});
5655
path =
57-
[{ Types.data = (Types.TypeNs (Some "attr")); disambiguator = 0 };
58-
{ Types.data = (Types.TypeNs (Some "trait_impl_inherit"));
59-
disambiguator = 0 };
60-
{ Types.data = (Types.TypeNs (Some "T")); disambiguator = 0 }]
56+
[{ Types.data = (Types.TypeNs "attr"); disambiguator = 0 };
57+
{ Types.data = (Types.TypeNs "trait_impl_inherit"); disambiguator = 0
58+
};
59+
{ Types.data = (Types.TypeNs "T"); disambiguator = 0 }]
6160
}
6261
};
6362
moved = None; suffix = None }) */
@@ -75,7 +74,7 @@ let impl: t_T t_S =
7574
=
7675
fun (self: t_S) ->
7776
let _:Prims.unit =
78-
Std.Io.Stdio.e_print (Core.Fmt.impl_4__new_const (mk_usize 1)
77+
Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
7978
(let list = ["impl S\n"] in
8079
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
8180
Rust_primitives.Hax.array_of_list 1 list)

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

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -15,12 +15,12 @@ let used_only_from_bin_crate_generic_function
1515
(arg: v_T)
1616
: Prims.unit =
1717
let _:Prims.unit =
18-
Std.Io.Stdio.e_print (Core.Fmt.impl_4__new_v1 (mk_usize 2)
18+
Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2)
1919
(mk_usize 1)
2020
(let list = ["used_only_from_bin_crate_generic_function with "; "\n"] in
2121
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
2222
Rust_primitives.Hax.array_of_list 2 list)
23-
(let list = [Core.Fmt.Rt.impl_1__new_debug #v_T arg <: Core.Fmt.Rt.t_Argument] in
23+
(let list = [Core.Fmt.Rt.impl__new_debug #v_T arg <: Core.Fmt.Rt.t_Argument] in
2424
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
2525
Rust_primitives.Hax.array_of_list 1 list)
2626
<:
@@ -35,12 +35,12 @@ let used_only_from_this_lib_crate_generic_function
3535
(arg: v_T)
3636
: Prims.unit =
3737
let _:Prims.unit =
38-
Std.Io.Stdio.e_print (Core.Fmt.impl_4__new_v1 (mk_usize 2)
38+
Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2)
3939
(mk_usize 1)
4040
(let list = ["used_only_from_this_lib_crate_generic_function with "; "\n"] in
4141
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
4242
Rust_primitives.Hax.array_of_list 2 list)
43-
(let list = [Core.Fmt.Rt.impl_1__new_debug #v_T arg <: Core.Fmt.Rt.t_Argument] in
43+
(let list = [Core.Fmt.Rt.impl__new_debug #v_T arg <: Core.Fmt.Rt.t_Argument] in
4444
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
4545
Rust_primitives.Hax.array_of_list 1 list)
4646
<:
@@ -55,12 +55,12 @@ let used_from_bin_crate_and_lib_crate_generic_function
5555
(arg: v_T)
5656
: Prims.unit =
5757
let _:Prims.unit =
58-
Std.Io.Stdio.e_print (Core.Fmt.impl_4__new_v1 (mk_usize 2)
58+
Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2)
5959
(mk_usize 1)
6060
(let list = ["used_from_bin_crate_and_lib_crate_generic_function with "; "\n"] in
6161
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
6262
Rust_primitives.Hax.array_of_list 2 list)
63-
(let list = [Core.Fmt.Rt.impl_1__new_debug #v_T arg <: Core.Fmt.Rt.t_Argument] in
63+
(let list = [Core.Fmt.Rt.impl__new_debug #v_T arg <: Core.Fmt.Rt.t_Argument] in
6464
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
6565
Rust_primitives.Hax.array_of_list 1 list)
6666
<:
@@ -75,14 +75,14 @@ let used_with_same_type_from_bin_crate_and_lib_crate_generic_function
7575
(arg: v_T)
7676
: Prims.unit =
7777
let _:Prims.unit =
78-
Std.Io.Stdio.e_print (Core.Fmt.impl_4__new_v1 (mk_usize 2)
78+
Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2)
7979
(mk_usize 1)
8080
(let list =
8181
["used_with_same_type_from_bin_crate_and_lib_crate_generic_function with "; "\n"]
8282
in
8383
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
8484
Rust_primitives.Hax.array_of_list 2 list)
85-
(let list = [Core.Fmt.Rt.impl_1__new_debug #v_T arg <: Core.Fmt.Rt.t_Argument] in
85+
(let list = [Core.Fmt.Rt.impl__new_debug #v_T arg <: Core.Fmt.Rt.t_Argument] in
8686
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
8787
Rust_primitives.Hax.array_of_list 1 list)
8888
<:
@@ -97,12 +97,12 @@ let unused_generic_function
9797
(arg: v_T)
9898
: Prims.unit =
9999
let _:Prims.unit =
100-
Std.Io.Stdio.e_print (Core.Fmt.impl_4__new_v1 (mk_usize 2)
100+
Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2)
101101
(mk_usize 1)
102102
(let list = ["unused_generic_function with "; "\n"] in
103103
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
104104
Rust_primitives.Hax.array_of_list 2 list)
105-
(let list = [Core.Fmt.Rt.impl_1__new_debug #v_T arg <: Core.Fmt.Rt.t_Argument] in
105+
(let list = [Core.Fmt.Rt.impl__new_debug #v_T arg <: Core.Fmt.Rt.t_Argument] in
106106
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
107107
Rust_primitives.Hax.array_of_list 1 list)
108108
<:

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

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -15,12 +15,12 @@ let used_only_from_bin_crate_generic_function
1515
(arg: v_T)
1616
: Prims.unit =
1717
let _:Prims.unit =
18-
Std.Io.Stdio.e_print (Core.Fmt.impl_4__new_v1 (mk_usize 2)
18+
Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2)
1919
(mk_usize 1)
2020
(let list = ["used_only_from_bin_crate_generic_function with "; "\n"] in
2121
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
2222
Rust_primitives.Hax.array_of_list 2 list)
23-
(let list = [Core.Fmt.Rt.impl_1__new_debug #v_T arg <: Core.Fmt.Rt.t_Argument] in
23+
(let list = [Core.Fmt.Rt.impl__new_debug #v_T arg <: Core.Fmt.Rt.t_Argument] in
2424
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
2525
Rust_primitives.Hax.array_of_list 1 list)
2626
<:
@@ -35,12 +35,12 @@ let used_only_from_this_lib_crate_generic_function
3535
(arg: v_T)
3636
: Prims.unit =
3737
let _:Prims.unit =
38-
Std.Io.Stdio.e_print (Core.Fmt.impl_4__new_v1 (mk_usize 2)
38+
Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2)
3939
(mk_usize 1)
4040
(let list = ["used_only_from_this_lib_crate_generic_function with "; "\n"] in
4141
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
4242
Rust_primitives.Hax.array_of_list 2 list)
43-
(let list = [Core.Fmt.Rt.impl_1__new_debug #v_T arg <: Core.Fmt.Rt.t_Argument] in
43+
(let list = [Core.Fmt.Rt.impl__new_debug #v_T arg <: Core.Fmt.Rt.t_Argument] in
4444
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
4545
Rust_primitives.Hax.array_of_list 1 list)
4646
<:
@@ -55,12 +55,12 @@ let used_from_bin_crate_and_lib_crate_generic_function
5555
(arg: v_T)
5656
: Prims.unit =
5757
let _:Prims.unit =
58-
Std.Io.Stdio.e_print (Core.Fmt.impl_4__new_v1 (mk_usize 2)
58+
Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2)
5959
(mk_usize 1)
6060
(let list = ["used_from_bin_crate_and_lib_crate_generic_function with "; "\n"] in
6161
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
6262
Rust_primitives.Hax.array_of_list 2 list)
63-
(let list = [Core.Fmt.Rt.impl_1__new_debug #v_T arg <: Core.Fmt.Rt.t_Argument] in
63+
(let list = [Core.Fmt.Rt.impl__new_debug #v_T arg <: Core.Fmt.Rt.t_Argument] in
6464
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
6565
Rust_primitives.Hax.array_of_list 1 list)
6666
<:
@@ -75,14 +75,14 @@ let used_with_same_type_from_bin_crate_and_lib_crate_generic_function
7575
(arg: v_T)
7676
: Prims.unit =
7777
let _:Prims.unit =
78-
Std.Io.Stdio.e_print (Core.Fmt.impl_4__new_v1 (mk_usize 2)
78+
Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2)
7979
(mk_usize 1)
8080
(let list =
8181
["used_with_same_type_from_bin_crate_and_lib_crate_generic_function with "; "\n"]
8282
in
8383
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
8484
Rust_primitives.Hax.array_of_list 2 list)
85-
(let list = [Core.Fmt.Rt.impl_1__new_debug #v_T arg <: Core.Fmt.Rt.t_Argument] in
85+
(let list = [Core.Fmt.Rt.impl__new_debug #v_T arg <: Core.Fmt.Rt.t_Argument] in
8686
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
8787
Rust_primitives.Hax.array_of_list 1 list)
8888
<:
@@ -97,12 +97,12 @@ let unused_generic_function
9797
(arg: v_T)
9898
: Prims.unit =
9999
let _:Prims.unit =
100-
Std.Io.Stdio.e_print (Core.Fmt.impl_4__new_v1 (mk_usize 2)
100+
Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2)
101101
(mk_usize 1)
102102
(let list = ["unused_generic_function with "; "\n"] in
103103
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
104104
Rust_primitives.Hax.array_of_list 2 list)
105-
(let list = [Core.Fmt.Rt.impl_1__new_debug #v_T arg <: Core.Fmt.Rt.t_Argument] in
105+
(let list = [Core.Fmt.Rt.impl__new_debug #v_T arg <: Core.Fmt.Rt.t_Argument] in
106106
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
107107
Rust_primitives.Hax.array_of_list 1 list)
108108
<:

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

Lines changed: 24 additions & 22 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.impl_4__new_const (mk_usize 1)
15+
Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__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,36 +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 res:Alloc.String.t_String =
33-
Alloc.Fmt.format (Core.Fmt.impl_4__new_v1 (mk_usize 1)
34-
(mk_usize 1)
35-
(let list = ["Error loading configs: "] in
36-
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
37-
Rust_primitives.Hax.array_of_list 1 list)
38-
(let list =
39-
[
40-
Core.Fmt.Rt.impl_1__new_display #Alloc.String.t_String e
41-
<:
42-
Core.Fmt.Rt.t_Argument
43-
]
44-
in
45-
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
46-
Rust_primitives.Hax.array_of_list 1 list)
32+
let message:Alloc.String.t_String =
33+
Core.Hint.must_use #Alloc.String.t_String
34+
(Alloc.Fmt.format (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 1)
35+
(mk_usize 1)
36+
(let list = ["Error loading configs: "] in
37+
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
38+
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)
48+
<:
49+
Core.Fmt.t_Arguments)
4750
<:
48-
Core.Fmt.t_Arguments)
51+
Alloc.String.t_String)
4952
in
50-
let message:Alloc.String.t_String = Core.Hint.must_use #Alloc.String.t_String res in
5153
if (Alloc.String.impl_String__len message <: usize) >. mk_usize 0
5254
then
5355
let _:Prims.unit =
54-
Std.Io.Stdio.e_print (Core.Fmt.impl_4__new_v1 (mk_usize 2)
56+
Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2)
5557
(mk_usize 1)
5658
(let list = [""; "\n"] in
5759
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
5860
Rust_primitives.Hax.array_of_list 2 list)
5961
(let list =
6062
[
61-
Core.Fmt.Rt.impl_1__new_display #Alloc.String.t_String message
63+
Core.Fmt.Rt.impl__new_display #Alloc.String.t_String message
6264
<:
6365
Core.Fmt.Rt.t_Argument
6466
]
@@ -81,7 +83,7 @@ let main (_: Prims.unit) : Core.Result.t_Result Prims.unit Alloc.String.t_String
8183
if (Core.Str.impl_str__len "error" <: usize) >. mk_usize 0
8284
then
8385
let _:Prims.unit =
84-
Std.Io.Stdio.e_print (Core.Fmt.impl_4__new_const (mk_usize 1)
86+
Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
8587
(let list = ["no msg\n"] in
8688
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
8789
Rust_primitives.Hax.array_of_list 1 list)
@@ -92,7 +94,7 @@ let main (_: Prims.unit) : Core.Result.t_Result Prims.unit Alloc.String.t_String
9294
()
9395
else
9496
let _:Prims.unit =
95-
Std.Io.Stdio.e_print (Core.Fmt.impl_4__new_const (mk_usize 1)
97+
Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1)
9698
(let list = ["error\n"] in
9799
FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
98100
Rust_primitives.Hax.array_of_list 1 list)

0 commit comments

Comments
 (0)