Skip to content

Commit 561af07

Browse files
zjp-CNzjp-CN
committed
test: update snapshots due to newly added SourceCode field type
1 parent 80c0976 commit 561af07

File tree

9 files changed

+10872
-2820
lines changed

9 files changed

+10872
-2820
lines changed

‎tests/snapshots/ad_hoc.json‎

Lines changed: 55 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -1,84 +1,123 @@
11
[
22
{
3-
"hash": "952175153267326104817555187587143859995",
3+
"hash": "240402353946165679413432703131261523692",
44
"def_id": "DefId { id: 0, name: \"adhoc::callee_defined_in_proof\" }",
55
"file": "tests/proofs/ad_hoc.rs",
66
"attrs": [
77
"#[kanitool::proof]"
88
],
9-
"func": "fn callee_defined_in_proof() {\n fn f() -> u8 {\n 1\n }\n assert!(f() == 1);\n }",
9+
"func": {
10+
"src": "fn callee_defined_in_proof() {\n fn f() -> u8 {\n 1\n }\n assert!(f() == 1);\n }",
11+
"before_expansion": null
12+
},
1013
"callees": [
1114
{
1215
"def_id": "DefId { id: 6, name: \"kani::assert\" }",
1316
"file": "kani/library/kani_core/src/lib.rs",
14-
"func": "pub const fn assert(cond: bool, msg: &'static str) {\n let _ = cond;\n let _ = msg;\n }"
17+
"func": {
18+
"src": "pub const fn assert(cond: bool, msg: &'static str) {\n let _ = cond;\n let _ = msg;\n }",
19+
"before_expansion": "kani_core::kani_intrinsics!(std)"
20+
}
1521
},
1622
{
1723
"def_id": "DefId { id: 1, name: \"adhoc::callee_defined_in_proof::f\" }",
1824
"file": "tests/proofs/ad_hoc.rs",
19-
"func": "fn f() -> u8 {\n 1\n }"
25+
"func": {
26+
"src": "fn f() -> u8 {\n 1\n }",
27+
"before_expansion": null
28+
}
2029
}
2130
]
2231
},
2332
{
24-
"hash": "75621983092344117614099719256493026487",
33+
"hash": "910297032864347757816118745588521867089",
2534
"def_id": "DefId { id: 2, name: \"adhoc::closure_in_proof\" }",
2635
"file": "tests/proofs/ad_hoc.rs",
2736
"attrs": [
2837
"#[kanitool::proof]"
2938
],
30-
"func": "fn closure_in_proof() {\n let f = || 1;\n assert!(f() == 1);\n }",
39+
"func": {
40+
"src": "fn closure_in_proof() {\n let f = || 1;\n assert!(f() == 1);\n }",
41+
"before_expansion": null
42+
},
3143
"callees": [
3244
{
3345
"def_id": "DefId { id: 6, name: \"kani::assert\" }",
3446
"file": "kani/library/kani_core/src/lib.rs",
35-
"func": "pub const fn assert(cond: bool, msg: &'static str) {\n let _ = cond;\n let _ = msg;\n }"
47+
"func": {
48+
"src": "pub const fn assert(cond: bool, msg: &'static str) {\n let _ = cond;\n let _ = msg;\n }",
49+
"before_expansion": "kani_core::kani_intrinsics!(std)"
50+
}
3651
},
3752
{
3853
"def_id": "DefId { id: 3, name: \"adhoc::closure_in_proof::{closure#0}\" }",
3954
"file": "tests/proofs/ad_hoc.rs",
40-
"func": "|| 1"
55+
"func": {
56+
"src": "|| 1",
57+
"before_expansion": null
58+
}
4159
}
4260
]
4361
},
4462
{
45-
"hash": "767440852073129240514318853477184375838",
63+
"hash": "210930681113882741614289248380189671885",
4664
"def_id": "DefId { id: 5, name: \"adhoc::proof_in_fn_item::proof\" }",
4765
"file": "tests/proofs/ad_hoc.rs",
4866
"attrs": [
4967
"#[kanitool::proof]"
5068
],
51-
"func": "fn proof() {\n assert!(kani::any::<u8>() == 1);\n }",
69+
"func": {
70+
"src": "fn proof() {\n assert!(kani::any::<u8>() == 1);\n }",
71+
"before_expansion": null
72+
},
5273
"callees": [
5374
{
5475
"def_id": "DefId { id: 10, name: \"<u8 as kani::Arbitrary>::any\" }",
5576
"file": "kani/library/kani_core/src/arbitrary.rs",
56-
"func": "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 }"
77+
"func": {
78+
"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 }",
79+
"before_expansion": "trivial_arbitrary!(u8)"
80+
}
5781
},
5882
{
5983
"def_id": "DefId { id: 12, name: \"kani::any_raw\" }",
6084
"file": "kani/library/kani_core/src/lib.rs",
61-
"func": "fn any_raw<T: Copy>() -> T {\n kani_intrinsic()\n }"
85+
"func": {
86+
"src": "fn any_raw<T: Copy>() -> T {\n kani_intrinsic()\n }",
87+
"before_expansion": "kani_core::kani_intrinsics!(std)"
88+
}
6289
},
6390
{
6491
"def_id": "DefId { id: 13, name: \"kani::kani_intrinsic\" }",
6592
"file": "kani/library/kani_core/src/lib.rs",
66-
"func": "fn kani_intrinsic<T>() -> T {\n #[allow(clippy::empty_loop)]\n loop {}\n }"
93+
"func": {
94+
"src": "fn kani_intrinsic<T>() -> T {\n #[allow(clippy::empty_loop)]\n loop {}\n }",
95+
"before_expansion": "kani_core::kani_intrinsics!(std)"
96+
}
6797
},
6898
{
6999
"def_id": "DefId { id: 6, name: \"kani::assert\" }",
70100
"file": "kani/library/kani_core/src/lib.rs",
71-
"func": "pub const fn assert(cond: bool, msg: &'static str) {\n let _ = cond;\n let _ = msg;\n }"
101+
"func": {
102+
"src": "pub const fn assert(cond: bool, msg: &'static str) {\n let _ = cond;\n let _ = msg;\n }",
103+
"before_expansion": "kani_core::kani_intrinsics!(std)"
104+
}
72105
},
73106
{
74107
"def_id": "DefId { id: 8, name: \"kani::any\" }",
75108
"file": "kani/library/kani_core/src/lib.rs",
76-
"func": "pub fn any<T: Arbitrary>() -> T {\n T::any()\n }"
109+
"func": {
110+
"src": "pub fn any<T: Arbitrary>() -> T {\n T::any()\n }",
111+
"before_expansion": "kani_core::kani_intrinsics!(std)"
112+
}
77113
},
78114
{
79115
"def_id": "DefId { id: 11, name: \"kani::any_raw_internal\" }",
80116
"file": "kani/library/kani_core/src/lib.rs",
81-
"func": "unsafe fn any_raw_internal<T: Copy>() -> T {\n any_raw::<T>()\n }"
117+
"func": {
118+
"src": "unsafe fn any_raw_internal<T: Copy>() -> T {\n any_raw::<T>()\n }",
119+
"before_expansion": "kani_core::kani_intrinsics!(std)"
120+
}
82121
}
83122
]
84123
}

0 commit comments

Comments
 (0)