Skip to content

Commit 4544ee2

Browse files
zjp-CNzjp-CN
committed
test: update snapshots due to MacroBacktrace field added
1 parent 14b7f02 commit 4544ee2

17 files changed

+12778
-3553
lines changed

‎tests/proofs.rs‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -114,6 +114,8 @@ fn test_compare_unique_hash() -> Result<()> {
114114
[
115115
"tests/compare/contract1.rs",
116116
"tests/compare/contract2.rs",
117+
"tests/compare/gen_proofs_by_nested_macros1.rs",
118+
"tests/compare/gen_proofs_by_nested_macros2.rs",
117119
"tests/compare/proof1.rs",
118120
"tests/compare/proof2.rs",
119121
]

‎tests/snapshots/ad_hoc.json‎

Lines changed: 105 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
[
22
{
3-
"hash": "115532895332902626963853966127921584592",
3+
"hash": "1399750479570041979215775816393145646123",
44
"def_id": "DefId { id: 0, name: \"adhoc::callee_defined_in_proof\" }",
55
"attrs": [
66
"#[kanitool::proof]"
@@ -11,7 +11,8 @@
1111
"kind": "Item",
1212
"file": "tests/proofs/ad_hoc.rs",
1313
"src": "fn callee_defined_in_proof() {\n fn f() -> u8 {\n 1\n }\n assert!(f() == 1);\n }",
14-
"before_expansion": null
14+
"macro_backtrace_len": 0,
15+
"macro_backtrace": []
1516
},
1617
"callees_len": 2,
1718
"callees": [
@@ -23,7 +24,8 @@
2324
"kind": "Item",
2425
"file": "tests/proofs/ad_hoc.rs",
2526
"src": "fn f() -> u8 {\n 1\n }",
26-
"before_expansion": null
27+
"macro_backtrace_len": 0,
28+
"macro_backtrace": []
2729
}
2830
},
2931
{
@@ -34,13 +36,23 @@
3436
"kind": "Item",
3537
"file": "kani/library/kani_core/src/lib.rs",
3638
"src": "pub const fn assert(cond: bool, msg: &'static str) {\n let _ = cond;\n let _ = msg;\n }",
37-
"before_expansion": "kani_core::kani_intrinsics!(std)"
39+
"macro_backtrace_len": 2,
40+
"macro_backtrace": [
41+
{
42+
"callsite": "kani_core::kani_intrinsics!(std)",
43+
"defsite": "macro_rules! kani_intrinsics"
44+
},
45+
{
46+
"callsite": "kani_core::kani_lib!(kani)",
47+
"defsite": "macro_rules! kani_lib"
48+
}
49+
]
3850
}
3951
}
4052
]
4153
},
4254
{
43-
"hash": "948578847723761908816026719336720175756",
55+
"hash": "865811375693261858618344779187018167127",
4456
"def_id": "DefId { id: 2, name: \"adhoc::closure_in_proof\" }",
4557
"attrs": [
4658
"#[kanitool::proof]"
@@ -51,7 +63,8 @@
5163
"kind": "Item",
5264
"file": "tests/proofs/ad_hoc.rs",
5365
"src": "fn closure_in_proof() {\n let f = || 1;\n assert!(f() == 1);\n }",
54-
"before_expansion": null
66+
"macro_backtrace_len": 0,
67+
"macro_backtrace": []
5568
},
5669
"callees_len": 2,
5770
"callees": [
@@ -63,7 +76,8 @@
6376
"kind": "Item",
6477
"file": "tests/proofs/ad_hoc.rs",
6578
"src": "|| 1",
66-
"before_expansion": null
79+
"macro_backtrace_len": 0,
80+
"macro_backtrace": []
6781
}
6882
},
6983
{
@@ -74,13 +88,23 @@
7488
"kind": "Item",
7589
"file": "kani/library/kani_core/src/lib.rs",
7690
"src": "pub const fn assert(cond: bool, msg: &'static str) {\n let _ = cond;\n let _ = msg;\n }",
77-
"before_expansion": "kani_core::kani_intrinsics!(std)"
91+
"macro_backtrace_len": 2,
92+
"macro_backtrace": [
93+
{
94+
"callsite": "kani_core::kani_intrinsics!(std)",
95+
"defsite": "macro_rules! kani_intrinsics"
96+
},
97+
{
98+
"callsite": "kani_core::kani_lib!(kani)",
99+
"defsite": "macro_rules! kani_lib"
100+
}
101+
]
78102
}
79103
}
80104
]
81105
},
82106
{
83-
"hash": "154741629691533277149647678297539545731",
107+
"hash": "60735437944941787725246177079802085936",
84108
"def_id": "DefId { id: 5, name: \"adhoc::proof_in_fn_item::proof\" }",
85109
"attrs": [
86110
"#[kanitool::proof]"
@@ -91,7 +115,8 @@
91115
"kind": "Item",
92116
"file": "tests/proofs/ad_hoc.rs",
93117
"src": "fn proof() {\n assert!(kani::any::<u8>() == 1);\n }",
94-
"before_expansion": null
118+
"macro_backtrace_len": 0,
119+
"macro_backtrace": []
95120
},
96121
"callees_len": 6,
97122
"callees": [
@@ -103,7 +128,21 @@
103128
"kind": "Item",
104129
"file": "kani/library/kani_core/src/arbitrary.rs",
105130
"src": "fn any() -> Self {\n // This size_of call does not use generic_const_exprs feature. It's inside a macro, and Self isn't generic.\n unsafe { crate::kani::any_raw_internal::<Self>() }\n }",
106-
"before_expansion": "trivial_arbitrary!(u8)"
131+
"macro_backtrace_len": 3,
132+
"macro_backtrace": [
133+
{
134+
"callsite": "trivial_arbitrary!(u8)",
135+
"defsite": "macro_rules! trivial_arbitrary {\n ( $type: ty ) => {\n impl Arbitrary for $type {\n #[inline(always)]\n fn any() -> Self {\n // This size_of call does not use generic_const_exprs feature. It's inside a macro, and Self isn't generic.\n unsafe { crate::kani::any_raw_internal::<Self>() }\n }\n fn any_array<const MAX_ARRAY_LENGTH: usize>() -> [Self; MAX_ARRAY_LENGTH] {\n unsafe { crate::kani::any_raw_array::<Self, MAX_ARRAY_LENGTH>() }\n }\n }\n };\n }"
136+
},
137+
{
138+
"callsite": "kani_core::generate_arbitrary!(std)",
139+
"defsite": "macro_rules! generate_arbitrary"
140+
},
141+
{
142+
"callsite": "kani_core::kani_lib!(kani)",
143+
"defsite": "macro_rules! kani_lib"
144+
}
145+
]
107146
}
108147
},
109148
{
@@ -114,7 +153,17 @@
114153
"kind": "Item",
115154
"file": "kani/library/kani_core/src/lib.rs",
116155
"src": "pub fn any<T: Arbitrary>() -> T {\n T::any()\n }",
117-
"before_expansion": "kani_core::kani_intrinsics!(std)"
156+
"macro_backtrace_len": 2,
157+
"macro_backtrace": [
158+
{
159+
"callsite": "kani_core::kani_intrinsics!(std)",
160+
"defsite": "macro_rules! kani_intrinsics"
161+
},
162+
{
163+
"callsite": "kani_core::kani_lib!(kani)",
164+
"defsite": "macro_rules! kani_lib"
165+
}
166+
]
118167
}
119168
},
120169
{
@@ -125,7 +174,17 @@
125174
"kind": "Item",
126175
"file": "kani/library/kani_core/src/lib.rs",
127176
"src": "fn any_raw<T: Copy>() -> T {\n kani_intrinsic()\n }",
128-
"before_expansion": "kani_core::kani_intrinsics!(std)"
177+
"macro_backtrace_len": 2,
178+
"macro_backtrace": [
179+
{
180+
"callsite": "kani_core::kani_intrinsics!(std)",
181+
"defsite": "macro_rules! kani_intrinsics"
182+
},
183+
{
184+
"callsite": "kani_core::kani_lib!(kani)",
185+
"defsite": "macro_rules! kani_lib"
186+
}
187+
]
129188
}
130189
},
131190
{
@@ -136,7 +195,17 @@
136195
"kind": "Item",
137196
"file": "kani/library/kani_core/src/lib.rs",
138197
"src": "unsafe fn any_raw_internal<T: Copy>() -> T {\n any_raw::<T>()\n }",
139-
"before_expansion": "kani_core::kani_intrinsics!(std)"
198+
"macro_backtrace_len": 2,
199+
"macro_backtrace": [
200+
{
201+
"callsite": "kani_core::kani_intrinsics!(std)",
202+
"defsite": "macro_rules! kani_intrinsics"
203+
},
204+
{
205+
"callsite": "kani_core::kani_lib!(kani)",
206+
"defsite": "macro_rules! kani_lib"
207+
}
208+
]
140209
}
141210
},
142211
{
@@ -147,7 +216,17 @@
147216
"kind": "Item",
148217
"file": "kani/library/kani_core/src/lib.rs",
149218
"src": "pub const fn assert(cond: bool, msg: &'static str) {\n let _ = cond;\n let _ = msg;\n }",
150-
"before_expansion": "kani_core::kani_intrinsics!(std)"
219+
"macro_backtrace_len": 2,
220+
"macro_backtrace": [
221+
{
222+
"callsite": "kani_core::kani_intrinsics!(std)",
223+
"defsite": "macro_rules! kani_intrinsics"
224+
},
225+
{
226+
"callsite": "kani_core::kani_lib!(kani)",
227+
"defsite": "macro_rules! kani_lib"
228+
}
229+
]
151230
}
152231
},
153232
{
@@ -158,7 +237,17 @@
158237
"kind": "Item",
159238
"file": "kani/library/kani_core/src/lib.rs",
160239
"src": "fn kani_intrinsic<T>() -> T {\n #[allow(clippy::empty_loop)]\n loop {}\n }",
161-
"before_expansion": "kani_core::kani_intrinsics!(std)"
240+
"macro_backtrace_len": 2,
241+
"macro_backtrace": [
242+
{
243+
"callsite": "kani_core::kani_intrinsics!(std)",
244+
"defsite": "macro_rules! kani_intrinsics"
245+
},
246+
{
247+
"callsite": "kani_core::kani_lib!(kani)",
248+
"defsite": "macro_rules! kani_lib"
249+
}
250+
]
162251
}
163252
}
164253
]

0 commit comments

Comments
 (0)