Skip to content

Commit d0a8e7f

Browse files
zjp-CNzjp-CN
committed
test: update snapshots due to back to get calls from Instance
1 parent 933af65 commit d0a8e7f

File tree

7 files changed

+16841
-6781
lines changed

7 files changed

+16841
-6781
lines changed

‎tests/snapshots/by_macros/gen_contracts_by_macros.json‎

Lines changed: 96 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
[
22
{
3-
"hash": "845442505770887177010392654257959311323",
3+
"hash": "50317602858703944474094180767144751790",
44
"def_id": "DefId { id: 13, name: \"verify::proof1\" }",
55
"attrs": [
66
"#[kanitool::proof_for_contract = \"contract1\"]"
@@ -12,7 +12,7 @@
1212
"src": "fn $proof() {\n $contract_name(kani::any::<u8>());\n }",
1313
"before_expansion": "gen! { proof1: contract1(arg), arg > 0}"
1414
},
15-
"callees_len": 3,
15+
"callees_len": 6,
1616
"callees": [
1717
{
1818
"def_id": "DefId { id: 0, name: \"verify::contract1\" }",
@@ -34,6 +34,36 @@
3434
"before_expansion": "#[kani::requires($e)]"
3535
}
3636
},
37+
{
38+
"def_id": "DefId { id: 1, name: \"verify::contract1::kani_register_contract\" }",
39+
"func": {
40+
"name": "verify::contract1::kani_register_contract::<u8, {closure@tests/proofs/gen_contracts_by_macros.rs:3:9: 3:30}>",
41+
"kind": "Item",
42+
"file": "tests/proofs/gen_contracts_by_macros.rs",
43+
"src": "#[kani::requires($e)]",
44+
"before_expansion": "#[kani::requires($e)]"
45+
}
46+
},
47+
{
48+
"def_id": "DefId { id: 1, name: \"verify::contract1::kani_register_contract\" }",
49+
"func": {
50+
"name": "verify::contract1::kani_register_contract::<u8, {closure@tests/proofs/gen_contracts_by_macros.rs:3:9: 3:30}>",
51+
"kind": "Item",
52+
"file": "tests/proofs/gen_contracts_by_macros.rs",
53+
"src": "#[kani::requires($e)]",
54+
"before_expansion": "#[kani::requires($e)]"
55+
}
56+
},
57+
{
58+
"def_id": "DefId { id: 1, name: \"verify::contract1::kani_register_contract\" }",
59+
"func": {
60+
"name": "verify::contract1::kani_register_contract::<u8, {closure@tests/proofs/gen_contracts_by_macros.rs:3:9: 3:30}>",
61+
"kind": "Item",
62+
"file": "tests/proofs/gen_contracts_by_macros.rs",
63+
"src": "#[kani::requires($e)]",
64+
"before_expansion": "#[kani::requires($e)]"
65+
}
66+
},
3767
{
3868
"def_id": "DefId { id: 1, name: \"verify::contract1::kani_register_contract\" }",
3969
"func": {
@@ -47,7 +77,7 @@
4777
]
4878
},
4979
{
50-
"hash": "626547758136143336212812375568748807677",
80+
"hash": "123668483634893862457299768406549499156",
5181
"def_id": "DefId { id: 27, name: \"verify::proof2\" }",
5282
"attrs": [
5383
"#[kanitool::proof_for_contract = \"contract2\"]"
@@ -59,7 +89,7 @@
5989
"src": "fn $proof() {\n $contract_name(kani::any::<u8>());\n }",
6090
"before_expansion": "gen! { proof2: contract2(arg), arg != 0}"
6191
},
62-
"callees_len": 3,
92+
"callees_len": 6,
6393
"callees": [
6494
{
6595
"def_id": "DefId { id: 14, name: \"verify::contract2\" }",
@@ -81,6 +111,36 @@
81111
"before_expansion": "#[kani::requires($e)]"
82112
}
83113
},
114+
{
115+
"def_id": "DefId { id: 15, name: \"verify::contract2::kani_register_contract\" }",
116+
"func": {
117+
"name": "verify::contract2::kani_register_contract::<u8, {closure@tests/proofs/gen_contracts_by_macros.rs:3:9: 3:30}>",
118+
"kind": "Item",
119+
"file": "tests/proofs/gen_contracts_by_macros.rs",
120+
"src": "#[kani::requires($e)]",
121+
"before_expansion": "#[kani::requires($e)]"
122+
}
123+
},
124+
{
125+
"def_id": "DefId { id: 15, name: \"verify::contract2::kani_register_contract\" }",
126+
"func": {
127+
"name": "verify::contract2::kani_register_contract::<u8, {closure@tests/proofs/gen_contracts_by_macros.rs:3:9: 3:30}>",
128+
"kind": "Item",
129+
"file": "tests/proofs/gen_contracts_by_macros.rs",
130+
"src": "#[kani::requires($e)]",
131+
"before_expansion": "#[kani::requires($e)]"
132+
}
133+
},
134+
{
135+
"def_id": "DefId { id: 15, name: \"verify::contract2::kani_register_contract\" }",
136+
"func": {
137+
"name": "verify::contract2::kani_register_contract::<u8, {closure@tests/proofs/gen_contracts_by_macros.rs:3:9: 3:30}>",
138+
"kind": "Item",
139+
"file": "tests/proofs/gen_contracts_by_macros.rs",
140+
"src": "#[kani::requires($e)]",
141+
"before_expansion": "#[kani::requires($e)]"
142+
}
143+
},
84144
{
85145
"def_id": "DefId { id: 15, name: \"verify::contract2::kani_register_contract\" }",
86146
"func": {
@@ -94,7 +154,7 @@
94154
]
95155
},
96156
{
97-
"hash": "1808781832361317200114116752328221501869",
157+
"hash": "55432547161220750194751943225746429104",
98158
"def_id": "DefId { id: 41, name: \"verify::proof3\" }",
99159
"attrs": [
100160
"#[kanitool::proof_for_contract = \"contract3\"]"
@@ -106,7 +166,7 @@
106166
"src": "fn $proof() {\n $contract_name(kani::any::<u8>());\n }",
107167
"before_expansion": "gen! { proof3: contract3(arg), arg < 10}"
108168
},
109-
"callees_len": 3,
169+
"callees_len": 6,
110170
"callees": [
111171
{
112172
"def_id": "DefId { id: 28, name: \"verify::contract3\" }",
@@ -128,6 +188,36 @@
128188
"before_expansion": "#[kani::requires($e)]"
129189
}
130190
},
191+
{
192+
"def_id": "DefId { id: 29, name: \"verify::contract3::kani_register_contract\" }",
193+
"func": {
194+
"name": "verify::contract3::kani_register_contract::<u8, {closure@tests/proofs/gen_contracts_by_macros.rs:3:9: 3:30}>",
195+
"kind": "Item",
196+
"file": "tests/proofs/gen_contracts_by_macros.rs",
197+
"src": "#[kani::requires($e)]",
198+
"before_expansion": "#[kani::requires($e)]"
199+
}
200+
},
201+
{
202+
"def_id": "DefId { id: 29, name: \"verify::contract3::kani_register_contract\" }",
203+
"func": {
204+
"name": "verify::contract3::kani_register_contract::<u8, {closure@tests/proofs/gen_contracts_by_macros.rs:3:9: 3:30}>",
205+
"kind": "Item",
206+
"file": "tests/proofs/gen_contracts_by_macros.rs",
207+
"src": "#[kani::requires($e)]",
208+
"before_expansion": "#[kani::requires($e)]"
209+
}
210+
},
211+
{
212+
"def_id": "DefId { id: 29, name: \"verify::contract3::kani_register_contract\" }",
213+
"func": {
214+
"name": "verify::contract3::kani_register_contract::<u8, {closure@tests/proofs/gen_contracts_by_macros.rs:3:9: 3:30}>",
215+
"kind": "Item",
216+
"file": "tests/proofs/gen_contracts_by_macros.rs",
217+
"src": "#[kani::requires($e)]",
218+
"before_expansion": "#[kani::requires($e)]"
219+
}
220+
},
131221
{
132222
"def_id": "DefId { id: 29, name: \"verify::contract3::kani_register_contract\" }",
133223
"func": {

0 commit comments

Comments
 (0)