Skip to content

Commit 130be69

Browse files
zjp-CNzjp-CN
committed
test: update snapshots due to newly added mangled_name field
1 parent 294c9a1 commit 130be69

12 files changed

+3507
-31
lines changed

‎tests/snapshots/ad_hoc.json‎

Lines changed: 16 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,13 @@
11
[
22
{
3-
"hash": "992735925007757375811560216797651727102",
3+
"hash": "115532895332902626963853966127921584592",
44
"def_id": "DefId { id: 0, name: \"adhoc::callee_defined_in_proof\" }",
55
"attrs": [
66
"#[kanitool::proof]"
77
],
88
"func": {
99
"name": "adhoc::callee_defined_in_proof",
10+
"mangled_name": "_ZN6ad_hoc5adhoc23callee_defined_in_proof17h9b15884d9d9d9404E",
1011
"kind": "Item",
1112
"file": "tests/proofs/ad_hoc.rs",
1213
"src": "fn callee_defined_in_proof() {\n fn f() -> u8 {\n 1\n }\n assert!(f() == 1);\n }",
@@ -18,6 +19,7 @@
1819
"def_id": "DefId { id: 1, name: \"adhoc::callee_defined_in_proof::f\" }",
1920
"func": {
2021
"name": "adhoc::callee_defined_in_proof::f",
22+
"mangled_name": "_ZN6ad_hoc5adhoc23callee_defined_in_proof1f17h0abef16a51e1e181E",
2123
"kind": "Item",
2224
"file": "tests/proofs/ad_hoc.rs",
2325
"src": "fn f() -> u8 {\n 1\n }",
@@ -28,6 +30,7 @@
2830
"def_id": "DefId { id: 6, name: \"kani::assert\" }",
2931
"func": {
3032
"name": "kani::assert",
33+
"mangled_name": "_ZN4kani6assert17hcc89e8c2e0f13823E",
3134
"kind": "Item",
3235
"file": "kani/library/kani_core/src/lib.rs",
3336
"src": "pub const fn assert(cond: bool, msg: &'static str) {\n let _ = cond;\n let _ = msg;\n }",
@@ -37,13 +40,14 @@
3740
]
3841
},
3942
{
40-
"hash": "445930972843662140314004119467706931293",
43+
"hash": "948578847723761908816026719336720175756",
4144
"def_id": "DefId { id: 2, name: \"adhoc::closure_in_proof\" }",
4245
"attrs": [
4346
"#[kanitool::proof]"
4447
],
4548
"func": {
4649
"name": "adhoc::closure_in_proof",
50+
"mangled_name": "_ZN6ad_hoc5adhoc16closure_in_proof17h4b84872472ae10c5E",
4751
"kind": "Item",
4852
"file": "tests/proofs/ad_hoc.rs",
4953
"src": "fn closure_in_proof() {\n let f = || 1;\n assert!(f() == 1);\n }",
@@ -55,6 +59,7 @@
5559
"def_id": "DefId { id: 3, name: \"adhoc::closure_in_proof::{closure#0}\" }",
5660
"func": {
5761
"name": "adhoc::closure_in_proof::{closure#0}",
62+
"mangled_name": "_ZN6ad_hoc5adhoc16closure_in_proof28_$u7b$$u7b$closure$u7d$$u7d$17h92b80c5c3414e3eaE",
5863
"kind": "Item",
5964
"file": "tests/proofs/ad_hoc.rs",
6065
"src": "|| 1",
@@ -65,6 +70,7 @@
6570
"def_id": "DefId { id: 6, name: \"kani::assert\" }",
6671
"func": {
6772
"name": "kani::assert",
73+
"mangled_name": "_ZN4kani6assert17hcc89e8c2e0f13823E",
6874
"kind": "Item",
6975
"file": "kani/library/kani_core/src/lib.rs",
7076
"src": "pub const fn assert(cond: bool, msg: &'static str) {\n let _ = cond;\n let _ = msg;\n }",
@@ -74,13 +80,14 @@
7480
]
7581
},
7682
{
77-
"hash": "92040403138609719983524684892610030464",
83+
"hash": "154741629691533277149647678297539545731",
7884
"def_id": "DefId { id: 5, name: \"adhoc::proof_in_fn_item::proof\" }",
7985
"attrs": [
8086
"#[kanitool::proof]"
8187
],
8288
"func": {
8389
"name": "adhoc::proof_in_fn_item::proof",
90+
"mangled_name": "_ZN6ad_hoc5adhoc16proof_in_fn_item5proof17h897129ce606edafeE",
8491
"kind": "Item",
8592
"file": "tests/proofs/ad_hoc.rs",
8693
"src": "fn proof() {\n assert!(kani::any::<u8>() == 1);\n }",
@@ -92,6 +99,7 @@
9299
"def_id": "DefId { id: 10, name: \"<u8 as kani::Arbitrary>::any\" }",
93100
"func": {
94101
"name": "<u8 as kani::Arbitrary>::any",
102+
"mangled_name": "_ZN38_$LT$u8$u20$as$u20$kani..Arbitrary$GT$3any17hfd29445e7b2cdd95E",
95103
"kind": "Item",
96104
"file": "kani/library/kani_core/src/arbitrary.rs",
97105
"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 }",
@@ -102,6 +110,7 @@
102110
"def_id": "DefId { id: 8, name: \"kani::any\" }",
103111
"func": {
104112
"name": "kani::any::<u8>",
113+
"mangled_name": "_ZN4kani3any17hbb3849d6db385d2bE",
105114
"kind": "Item",
106115
"file": "kani/library/kani_core/src/lib.rs",
107116
"src": "pub fn any<T: Arbitrary>() -> T {\n T::any()\n }",
@@ -112,6 +121,7 @@
112121
"def_id": "DefId { id: 12, name: \"kani::any_raw\" }",
113122
"func": {
114123
"name": "kani::any_raw::<u8>",
124+
"mangled_name": "_ZN4kani7any_raw17he1d5f207e37d9300E",
115125
"kind": "Item",
116126
"file": "kani/library/kani_core/src/lib.rs",
117127
"src": "fn any_raw<T: Copy>() -> T {\n kani_intrinsic()\n }",
@@ -122,6 +132,7 @@
122132
"def_id": "DefId { id: 11, name: \"kani::any_raw_internal\" }",
123133
"func": {
124134
"name": "kani::any_raw_internal::<u8>",
135+
"mangled_name": "_ZN4kani16any_raw_internal17h7b9f8f23c4240680E",
125136
"kind": "Item",
126137
"file": "kani/library/kani_core/src/lib.rs",
127138
"src": "unsafe fn any_raw_internal<T: Copy>() -> T {\n any_raw::<T>()\n }",
@@ -132,6 +143,7 @@
132143
"def_id": "DefId { id: 6, name: \"kani::assert\" }",
133144
"func": {
134145
"name": "kani::assert",
146+
"mangled_name": "_ZN4kani6assert17hcc89e8c2e0f13823E",
135147
"kind": "Item",
136148
"file": "kani/library/kani_core/src/lib.rs",
137149
"src": "pub const fn assert(cond: bool, msg: &'static str) {\n let _ = cond;\n let _ = msg;\n }",
@@ -142,6 +154,7 @@
142154
"def_id": "DefId { id: 13, name: \"kani::kani_intrinsic\" }",
143155
"func": {
144156
"name": "kani::kani_intrinsic::<u8>",
157+
"mangled_name": "_ZN4kani14kani_intrinsic17h5075915a9093bedeE",
145158
"kind": "Item",
146159
"file": "kani/library/kani_core/src/lib.rs",
147160
"src": "fn kani_intrinsic<T>() -> T {\n #[allow(clippy::empty_loop)]\n loop {}\n }",

‎tests/snapshots/by_macros/gen_contracts_by_macros.json‎

Lines changed: 24 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,13 @@
11
[
22
{
3-
"hash": "50317602858703944474094180767144751790",
3+
"hash": "53883336862579689525661064515327026093",
44
"def_id": "DefId { id: 13, name: \"verify::proof1\" }",
55
"attrs": [
66
"#[kanitool::proof_for_contract = \"contract1\"]"
77
],
88
"func": {
99
"name": "verify::proof1",
10+
"mangled_name": "_ZN23gen_contracts_by_macros6verify6proof117h9828d0e50eee99deE",
1011
"kind": "Item",
1112
"file": "tests/proofs/gen_contracts_by_macros.rs",
1213
"src": "fn $proof() {\n $contract_name(kani::any::<u8>());\n }",
@@ -18,6 +19,7 @@
1819
"def_id": "DefId { id: 0, name: \"verify::contract1\" }",
1920
"func": {
2021
"name": "verify::contract1",
22+
"mangled_name": "_ZN23gen_contracts_by_macros6verify9contract117hb3bd984f06359a3eE",
2123
"kind": "Item",
2224
"file": "tests/proofs/gen_contracts_by_macros.rs",
2325
"src": "fn",
@@ -28,6 +30,7 @@
2830
"def_id": "DefId { id: 2, name: \"verify::contract1::kani_contract_mode\" }",
2931
"func": {
3032
"name": "verify::contract1::kani_contract_mode",
33+
"mangled_name": "_ZN23gen_contracts_by_macros6verify9contract118kani_contract_mode17h72db9759cd9f3f19E",
3134
"kind": "Item",
3235
"file": "tests/proofs/gen_contracts_by_macros.rs",
3336
"src": "#[kani::requires($e)]",
@@ -38,6 +41,7 @@
3841
"def_id": "DefId { id: 1, name: \"verify::contract1::kani_register_contract\" }",
3942
"func": {
4043
"name": "verify::contract1::kani_register_contract::<u8, {closure@tests/proofs/gen_contracts_by_macros.rs:3:9: 3:30}>",
44+
"mangled_name": "_ZN23gen_contracts_by_macros6verify9contract122kani_register_contract17h18a02e24ad3aea9fE",
4145
"kind": "Item",
4246
"file": "tests/proofs/gen_contracts_by_macros.rs",
4347
"src": "#[kani::requires($e)]",
@@ -48,6 +52,7 @@
4852
"def_id": "DefId { id: 1, name: \"verify::contract1::kani_register_contract\" }",
4953
"func": {
5054
"name": "verify::contract1::kani_register_contract::<u8, {closure@tests/proofs/gen_contracts_by_macros.rs:3:9: 3:30}>",
55+
"mangled_name": "_ZN23gen_contracts_by_macros6verify9contract122kani_register_contract17h9d0ccc93fbf12912E",
5156
"kind": "Item",
5257
"file": "tests/proofs/gen_contracts_by_macros.rs",
5358
"src": "#[kani::requires($e)]",
@@ -58,6 +63,7 @@
5863
"def_id": "DefId { id: 1, name: \"verify::contract1::kani_register_contract\" }",
5964
"func": {
6065
"name": "verify::contract1::kani_register_contract::<u8, {closure@tests/proofs/gen_contracts_by_macros.rs:3:9: 3:30}>",
66+
"mangled_name": "_ZN23gen_contracts_by_macros6verify9contract122kani_register_contract17hbf2da10a70b88b4fE",
6167
"kind": "Item",
6268
"file": "tests/proofs/gen_contracts_by_macros.rs",
6369
"src": "#[kani::requires($e)]",
@@ -68,6 +74,7 @@
6874
"def_id": "DefId { id: 1, name: \"verify::contract1::kani_register_contract\" }",
6975
"func": {
7076
"name": "verify::contract1::kani_register_contract::<u8, {closure@tests/proofs/gen_contracts_by_macros.rs:3:9: 3:30}>",
77+
"mangled_name": "_ZN23gen_contracts_by_macros6verify9contract122kani_register_contract17hc798f030eb131ab8E",
7178
"kind": "Item",
7279
"file": "tests/proofs/gen_contracts_by_macros.rs",
7380
"src": "#[kani::requires($e)]",
@@ -77,13 +84,14 @@
7784
]
7885
},
7986
{
80-
"hash": "123668483634893862457299768406549499156",
87+
"hash": "9746173011318684529009241340785190655",
8188
"def_id": "DefId { id: 27, name: \"verify::proof2\" }",
8289
"attrs": [
8390
"#[kanitool::proof_for_contract = \"contract2\"]"
8491
],
8592
"func": {
8693
"name": "verify::proof2",
94+
"mangled_name": "_ZN23gen_contracts_by_macros6verify6proof217h2843955b7716bef5E",
8795
"kind": "Item",
8896
"file": "tests/proofs/gen_contracts_by_macros.rs",
8997
"src": "fn $proof() {\n $contract_name(kani::any::<u8>());\n }",
@@ -95,6 +103,7 @@
95103
"def_id": "DefId { id: 14, name: \"verify::contract2\" }",
96104
"func": {
97105
"name": "verify::contract2",
106+
"mangled_name": "_ZN23gen_contracts_by_macros6verify9contract217h0d04df09eb11b527E",
98107
"kind": "Item",
99108
"file": "tests/proofs/gen_contracts_by_macros.rs",
100109
"src": "fn",
@@ -105,6 +114,7 @@
105114
"def_id": "DefId { id: 16, name: \"verify::contract2::kani_contract_mode\" }",
106115
"func": {
107116
"name": "verify::contract2::kani_contract_mode",
117+
"mangled_name": "_ZN23gen_contracts_by_macros6verify9contract218kani_contract_mode17h79ec39961c5f6f44E",
108118
"kind": "Item",
109119
"file": "tests/proofs/gen_contracts_by_macros.rs",
110120
"src": "#[kani::requires($e)]",
@@ -115,6 +125,7 @@
115125
"def_id": "DefId { id: 15, name: \"verify::contract2::kani_register_contract\" }",
116126
"func": {
117127
"name": "verify::contract2::kani_register_contract::<u8, {closure@tests/proofs/gen_contracts_by_macros.rs:3:9: 3:30}>",
128+
"mangled_name": "_ZN23gen_contracts_by_macros6verify9contract222kani_register_contract17h04a40b6780f61d7aE",
118129
"kind": "Item",
119130
"file": "tests/proofs/gen_contracts_by_macros.rs",
120131
"src": "#[kani::requires($e)]",
@@ -125,6 +136,7 @@
125136
"def_id": "DefId { id: 15, name: \"verify::contract2::kani_register_contract\" }",
126137
"func": {
127138
"name": "verify::contract2::kani_register_contract::<u8, {closure@tests/proofs/gen_contracts_by_macros.rs:3:9: 3:30}>",
139+
"mangled_name": "_ZN23gen_contracts_by_macros6verify9contract222kani_register_contract17h33c8f341cd7588c9E",
128140
"kind": "Item",
129141
"file": "tests/proofs/gen_contracts_by_macros.rs",
130142
"src": "#[kani::requires($e)]",
@@ -135,6 +147,7 @@
135147
"def_id": "DefId { id: 15, name: \"verify::contract2::kani_register_contract\" }",
136148
"func": {
137149
"name": "verify::contract2::kani_register_contract::<u8, {closure@tests/proofs/gen_contracts_by_macros.rs:3:9: 3:30}>",
150+
"mangled_name": "_ZN23gen_contracts_by_macros6verify9contract222kani_register_contract17h6687bf63f16f4f09E",
138151
"kind": "Item",
139152
"file": "tests/proofs/gen_contracts_by_macros.rs",
140153
"src": "#[kani::requires($e)]",
@@ -145,6 +158,7 @@
145158
"def_id": "DefId { id: 15, name: \"verify::contract2::kani_register_contract\" }",
146159
"func": {
147160
"name": "verify::contract2::kani_register_contract::<u8, {closure@tests/proofs/gen_contracts_by_macros.rs:3:9: 3:30}>",
161+
"mangled_name": "_ZN23gen_contracts_by_macros6verify9contract222kani_register_contract17h8a622067dd78d423E",
148162
"kind": "Item",
149163
"file": "tests/proofs/gen_contracts_by_macros.rs",
150164
"src": "#[kani::requires($e)]",
@@ -154,13 +168,14 @@
154168
]
155169
},
156170
{
157-
"hash": "55432547161220750194751943225746429104",
171+
"hash": "9281657212352396567602207150619318725",
158172
"def_id": "DefId { id: 41, name: \"verify::proof3\" }",
159173
"attrs": [
160174
"#[kanitool::proof_for_contract = \"contract3\"]"
161175
],
162176
"func": {
163177
"name": "verify::proof3",
178+
"mangled_name": "_ZN23gen_contracts_by_macros6verify6proof317h2d7e1f5e5fbd0d23E",
164179
"kind": "Item",
165180
"file": "tests/proofs/gen_contracts_by_macros.rs",
166181
"src": "fn $proof() {\n $contract_name(kani::any::<u8>());\n }",
@@ -172,6 +187,7 @@
172187
"def_id": "DefId { id: 28, name: \"verify::contract3\" }",
173188
"func": {
174189
"name": "verify::contract3",
190+
"mangled_name": "_ZN23gen_contracts_by_macros6verify9contract317h9ebb9c77f3355fbcE",
175191
"kind": "Item",
176192
"file": "tests/proofs/gen_contracts_by_macros.rs",
177193
"src": "fn",
@@ -182,6 +198,7 @@
182198
"def_id": "DefId { id: 30, name: \"verify::contract3::kani_contract_mode\" }",
183199
"func": {
184200
"name": "verify::contract3::kani_contract_mode",
201+
"mangled_name": "_ZN23gen_contracts_by_macros6verify9contract318kani_contract_mode17h3d488cf5d9cd84b9E",
185202
"kind": "Item",
186203
"file": "tests/proofs/gen_contracts_by_macros.rs",
187204
"src": "#[kani::requires($e)]",
@@ -192,6 +209,7 @@
192209
"def_id": "DefId { id: 29, name: \"verify::contract3::kani_register_contract\" }",
193210
"func": {
194211
"name": "verify::contract3::kani_register_contract::<u8, {closure@tests/proofs/gen_contracts_by_macros.rs:3:9: 3:30}>",
212+
"mangled_name": "_ZN23gen_contracts_by_macros6verify9contract322kani_register_contract17h2472f64cc64d7dd1E",
195213
"kind": "Item",
196214
"file": "tests/proofs/gen_contracts_by_macros.rs",
197215
"src": "#[kani::requires($e)]",
@@ -202,6 +220,7 @@
202220
"def_id": "DefId { id: 29, name: \"verify::contract3::kani_register_contract\" }",
203221
"func": {
204222
"name": "verify::contract3::kani_register_contract::<u8, {closure@tests/proofs/gen_contracts_by_macros.rs:3:9: 3:30}>",
223+
"mangled_name": "_ZN23gen_contracts_by_macros6verify9contract322kani_register_contract17h28ecc6a1cf09997aE",
205224
"kind": "Item",
206225
"file": "tests/proofs/gen_contracts_by_macros.rs",
207226
"src": "#[kani::requires($e)]",
@@ -212,6 +231,7 @@
212231
"def_id": "DefId { id: 29, name: \"verify::contract3::kani_register_contract\" }",
213232
"func": {
214233
"name": "verify::contract3::kani_register_contract::<u8, {closure@tests/proofs/gen_contracts_by_macros.rs:3:9: 3:30}>",
234+
"mangled_name": "_ZN23gen_contracts_by_macros6verify9contract322kani_register_contract17ha62f383d8b7dac00E",
215235
"kind": "Item",
216236
"file": "tests/proofs/gen_contracts_by_macros.rs",
217237
"src": "#[kani::requires($e)]",
@@ -222,6 +242,7 @@
222242
"def_id": "DefId { id: 29, name: \"verify::contract3::kani_register_contract\" }",
223243
"func": {
224244
"name": "verify::contract3::kani_register_contract::<u8, {closure@tests/proofs/gen_contracts_by_macros.rs:3:9: 3:30}>",
245+
"mangled_name": "_ZN23gen_contracts_by_macros6verify9contract322kani_register_contract17hb593ddcf4c3b408aE",
225246
"kind": "Item",
226247
"file": "tests/proofs/gen_contracts_by_macros.rs",
227248
"src": "#[kani::requires($e)]",

‎tests/snapshots/by_macros/gen_proofs_by_macros.json‎

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,13 @@
11
[
22
{
3-
"hash": "142324393913032614161438847443070542401",
3+
"hash": "172515572526024733973663110246078682042",
44
"def_id": "DefId { id: 0, name: \"verify::proof1\" }",
55
"attrs": [
66
"#[kanitool::proof]"
77
],
88
"func": {
99
"name": "verify::proof1",
10+
"mangled_name": "_ZN20gen_proofs_by_macros6verify6proof117hc4255bc4f41f2540E",
1011
"kind": "Item",
1112
"file": "tests/proofs/gen_proofs_by_macros.rs",
1213
"src": "fn $name() $block",
@@ -16,13 +17,14 @@
1617
"callees": []
1718
},
1819
{
19-
"hash": "1225837020836258327313751040515830526577",
20+
"hash": "1498844359471053435818444414434108506651",
2021
"def_id": "DefId { id: 1, name: \"verify::proof2\" }",
2122
"attrs": [
2223
"#[kanitool::proof]"
2324
],
2425
"func": {
2526
"name": "verify::proof2",
27+
"mangled_name": "_ZN20gen_proofs_by_macros6verify6proof217h7837bdff9d68a0f1E",
2628
"kind": "Item",
2729
"file": "tests/proofs/gen_proofs_by_macros.rs",
2830
"src": "fn $name() $block",
@@ -32,13 +34,14 @@
3234
"callees": []
3335
},
3436
{
35-
"hash": "19747672167383027672278738792967795470",
37+
"hash": "112512525167431077293054940275626137814",
3638
"def_id": "DefId { id: 2, name: \"verify::proof3\" }",
3739
"attrs": [
3840
"#[kanitool::proof]"
3941
],
4042
"func": {
4143
"name": "verify::proof3",
44+
"mangled_name": "_ZN20gen_proofs_by_macros6verify6proof317h628c936d75d70951E",
4245
"kind": "Item",
4346
"file": "tests/proofs/gen_proofs_by_macros.rs",
4447
"src": "fn $name() $block",

0 commit comments

Comments
 (0)