Skip to content

Commit 9ad4342

Browse files
zjp-CNzjp-CN
committed
test: update snapshots due to deduplicated calles and new namd & kind fields
1 parent 5678b94 commit 9ad4342

File tree

8 files changed

+11232
-13852
lines changed

8 files changed

+11232
-13852
lines changed

‎tests/snapshots/ad_hoc.json‎

Lines changed: 55 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -1,73 +1,87 @@
11
[
22
{
3-
"hash": "240402353946165679413432703131261523692",
3+
"hash": "992735925007757375811560216797651727102",
44
"def_id": "DefId { id: 0, name: \"adhoc::callee_defined_in_proof\" }",
55
"attrs": [
66
"#[kanitool::proof]"
77
],
88
"func": {
9+
"name": "adhoc::callee_defined_in_proof",
10+
"kind": "Item",
911
"file": "tests/proofs/ad_hoc.rs",
1012
"src": "fn callee_defined_in_proof() {\n fn f() -> u8 {\n 1\n }\n assert!(f() == 1);\n }",
1113
"before_expansion": null
1214
},
1315
"callees_len": 2,
1416
"callees": [
15-
{
16-
"def_id": "DefId { id: 6, name: \"kani::assert\" }",
17-
"func": {
18-
"file": "kani/library/kani_core/src/lib.rs",
19-
"src": "pub const fn assert(cond: bool, msg: &'static str) {\n let _ = cond;\n let _ = msg;\n }",
20-
"before_expansion": "kani_core::kani_intrinsics!(std)"
21-
}
22-
},
2317
{
2418
"def_id": "DefId { id: 1, name: \"adhoc::callee_defined_in_proof::f\" }",
2519
"func": {
20+
"name": "adhoc::callee_defined_in_proof::f",
21+
"kind": "Item",
2622
"file": "tests/proofs/ad_hoc.rs",
2723
"src": "fn f() -> u8 {\n 1\n }",
2824
"before_expansion": null
2925
}
26+
},
27+
{
28+
"def_id": "DefId { id: 6, name: \"kani::assert\" }",
29+
"func": {
30+
"name": "kani::assert",
31+
"kind": "Item",
32+
"file": "kani/library/kani_core/src/lib.rs",
33+
"src": "pub const fn assert(cond: bool, msg: &'static str) {\n let _ = cond;\n let _ = msg;\n }",
34+
"before_expansion": "kani_core::kani_intrinsics!(std)"
35+
}
3036
}
3137
]
3238
},
3339
{
34-
"hash": "910297032864347757816118745588521867089",
40+
"hash": "445930972843662140314004119467706931293",
3541
"def_id": "DefId { id: 2, name: \"adhoc::closure_in_proof\" }",
3642
"attrs": [
3743
"#[kanitool::proof]"
3844
],
3945
"func": {
46+
"name": "adhoc::closure_in_proof",
47+
"kind": "Item",
4048
"file": "tests/proofs/ad_hoc.rs",
4149
"src": "fn closure_in_proof() {\n let f = || 1;\n assert!(f() == 1);\n }",
4250
"before_expansion": null
4351
},
4452
"callees_len": 2,
4553
"callees": [
46-
{
47-
"def_id": "DefId { id: 6, name: \"kani::assert\" }",
48-
"func": {
49-
"file": "kani/library/kani_core/src/lib.rs",
50-
"src": "pub const fn assert(cond: bool, msg: &'static str) {\n let _ = cond;\n let _ = msg;\n }",
51-
"before_expansion": "kani_core::kani_intrinsics!(std)"
52-
}
53-
},
5454
{
5555
"def_id": "DefId { id: 3, name: \"adhoc::closure_in_proof::{closure#0}\" }",
5656
"func": {
57+
"name": "adhoc::closure_in_proof::{closure#0}",
58+
"kind": "Item",
5759
"file": "tests/proofs/ad_hoc.rs",
5860
"src": "|| 1",
5961
"before_expansion": null
6062
}
63+
},
64+
{
65+
"def_id": "DefId { id: 6, name: \"kani::assert\" }",
66+
"func": {
67+
"name": "kani::assert",
68+
"kind": "Item",
69+
"file": "kani/library/kani_core/src/lib.rs",
70+
"src": "pub const fn assert(cond: bool, msg: &'static str) {\n let _ = cond;\n let _ = msg;\n }",
71+
"before_expansion": "kani_core::kani_intrinsics!(std)"
72+
}
6173
}
6274
]
6375
},
6476
{
65-
"hash": "210930681113882741614289248380189671885",
77+
"hash": "92040403138609719983524684892610030464",
6678
"def_id": "DefId { id: 5, name: \"adhoc::proof_in_fn_item::proof\" }",
6779
"attrs": [
6880
"#[kanitool::proof]"
6981
],
7082
"func": {
83+
"name": "adhoc::proof_in_fn_item::proof",
84+
"kind": "Item",
7185
"file": "tests/proofs/ad_hoc.rs",
7286
"src": "fn proof() {\n assert!(kani::any::<u8>() == 1);\n }",
7387
"before_expansion": null
@@ -77,48 +91,60 @@
7791
{
7892
"def_id": "DefId { id: 10, name: \"<u8 as kani::Arbitrary>::any\" }",
7993
"func": {
94+
"name": "<u8 as kani::Arbitrary>::any",
95+
"kind": "Item",
8096
"file": "kani/library/kani_core/src/arbitrary.rs",
8197
"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 }",
8298
"before_expansion": "trivial_arbitrary!(u8)"
8399
}
84100
},
85101
{
86-
"def_id": "DefId { id: 12, name: \"kani::any_raw\" }",
102+
"def_id": "DefId { id: 8, name: \"kani::any\" }",
87103
"func": {
104+
"name": "kani::any::<u8>",
105+
"kind": "Item",
88106
"file": "kani/library/kani_core/src/lib.rs",
89-
"src": "fn any_raw<T: Copy>() -> T {\n kani_intrinsic()\n }",
107+
"src": "pub fn any<T: Arbitrary>() -> T {\n T::any()\n }",
90108
"before_expansion": "kani_core::kani_intrinsics!(std)"
91109
}
92110
},
93111
{
94-
"def_id": "DefId { id: 13, name: \"kani::kani_intrinsic\" }",
112+
"def_id": "DefId { id: 12, name: \"kani::any_raw\" }",
95113
"func": {
114+
"name": "kani::any_raw::<u8>",
115+
"kind": "Item",
96116
"file": "kani/library/kani_core/src/lib.rs",
97-
"src": "fn kani_intrinsic<T>() -> T {\n #[allow(clippy::empty_loop)]\n loop {}\n }",
117+
"src": "fn any_raw<T: Copy>() -> T {\n kani_intrinsic()\n }",
98118
"before_expansion": "kani_core::kani_intrinsics!(std)"
99119
}
100120
},
101121
{
102-
"def_id": "DefId { id: 6, name: \"kani::assert\" }",
122+
"def_id": "DefId { id: 11, name: \"kani::any_raw_internal\" }",
103123
"func": {
124+
"name": "kani::any_raw_internal::<u8>",
125+
"kind": "Item",
104126
"file": "kani/library/kani_core/src/lib.rs",
105-
"src": "pub const fn assert(cond: bool, msg: &'static str) {\n let _ = cond;\n let _ = msg;\n }",
127+
"src": "unsafe fn any_raw_internal<T: Copy>() -> T {\n any_raw::<T>()\n }",
106128
"before_expansion": "kani_core::kani_intrinsics!(std)"
107129
}
108130
},
109131
{
110-
"def_id": "DefId { id: 8, name: \"kani::any\" }",
132+
"def_id": "DefId { id: 6, name: \"kani::assert\" }",
111133
"func": {
134+
"name": "kani::assert",
135+
"kind": "Item",
112136
"file": "kani/library/kani_core/src/lib.rs",
113-
"src": "pub fn any<T: Arbitrary>() -> T {\n T::any()\n }",
137+
"src": "pub const fn assert(cond: bool, msg: &'static str) {\n let _ = cond;\n let _ = msg;\n }",
114138
"before_expansion": "kani_core::kani_intrinsics!(std)"
115139
}
116140
},
117141
{
118-
"def_id": "DefId { id: 11, name: \"kani::any_raw_internal\" }",
142+
"def_id": "DefId { id: 13, name: \"kani::kani_intrinsic\" }",
119143
"func": {
144+
"name": "kani::kani_intrinsic::<u8>",
145+
"kind": "Item",
120146
"file": "kani/library/kani_core/src/lib.rs",
121-
"src": "unsafe fn any_raw_internal<T: Copy>() -> T {\n any_raw::<T>()\n }",
147+
"src": "fn kani_intrinsic<T>() -> T {\n #[allow(clippy::empty_loop)]\n loop {}\n }",
122148
"before_expansion": "kani_core::kani_intrinsics!(std)"
123149
}
124150
}

0 commit comments

Comments
 (0)