11use assert_cmd:: Command ;
2- use expect_test:: expect ;
2+ use expect_test:: expect_file ;
33
44fn cmd ( ) -> Command {
55 Command :: cargo_bin ( env ! ( "CARGO_PKG_NAME" ) ) . unwrap ( )
@@ -8,86 +8,12 @@ fn cmd() -> Command {
88#[ test]
99fn standard_proof ( ) {
1010 let output = cmd ( ) . args ( [ "tests/standard_proof.rs" ] ) . output ( ) . unwrap ( ) ;
11- assert ! ( output. status. success( ) ) ;
11+ assert ! (
12+ output. status. success( ) ,
13+ "Failed to test standard_proof.rs:\n {}" ,
14+ std:: str :: from_utf8( & output. stderr) . unwrap( )
15+ ) ;
16+
1217 let stdout = String :: from_utf8_lossy ( & output. stdout ) ;
13- expect ! [ [ r##"
14- [
15- {
16- "file": "tests/standard_proof.rs",
17- "attrs": [
18- "#[kani::proof]",
19- "#[kani::proof]"
20- ],
21- "func": "fn standard_proof() {\n let val: u8 = kani::any();\n assert_eq!(val, 1, \"Not eq to 1.\");\n }",
22- "callees": [
23- "FnDef(DefId { id: 5, name: \"kani::any\" })",
24- "FnDef(DefId { id: 6, name: \"kani::assert\" })",
25- "FnDef(DefId { id: 7, name: \"kani::Arbitrary::any\" })"
26- ]
27- },
28- {
29- "file": "tests/standard_proof.rs",
30- "attrs": [
31- "#[kani::proof]",
32- "#[kani::proof]",
33- "#[allow(unused_mut)]"
34- ],
35- "func": "fn standard_proof_empty() {}",
36- "callees": []
37- },
38- {
39- "file": "tests/standard_proof.rs",
40- "attrs": [
41- "#[kani::proof]",
42- "#[kani::proof]"
43- ],
44- "func": "fn recursive_callees() {\n crate::top_level();\n }",
45- "callees": [
46- "FnDef(DefId { id: 3, name: \"top_level\" })",
47- "FnDef(DefId { id: 4, name: \"m::func1\" })",
48- "FnDef(DefId { id: 8, name: \"core::str::<impl str>::trim\" })",
49- "FnDef(DefId { id: 9, name: \"core::str::<impl str>::trim_matches\" })",
50- "FnDef(DefId { id: 15, name: \"core::str::<impl str>::get_unchecked\" })",
51- "FnDef(DefId { id: 16, name: \"std::slice::SliceIndex::get_unchecked\" })",
52- "FnDef(DefId { id: 14, name: \"std::str::pattern::ReverseSearcher::next_reject_back\" })",
53- "FnDef(DefId { id: 18, name: \"std::str::pattern::ReverseSearcher::next_back\" })",
54- "FnDef(DefId { id: 13, name: \"std::str::pattern::Searcher::next_reject\" })",
55- "FnDef(DefId { id: 19, name: \"std::str::pattern::Searcher::next\" })",
56- "FnDef(DefId { id: 12, name: \"std::str::pattern::Pattern::into_searcher\" })"
57- ]
58- },
59- {
60- "file": "tests/standard_proof.rs",
61- "attrs": [],
62- "func": "pub fn top_level() {\n m::func1();\n}",
63- "callees": [
64- "FnDef(DefId { id: 4, name: \"m::func1\" })",
65- "FnDef(DefId { id: 8, name: \"core::str::<impl str>::trim\" })",
66- "FnDef(DefId { id: 9, name: \"core::str::<impl str>::trim_matches\" })",
67- "FnDef(DefId { id: 15, name: \"core::str::<impl str>::get_unchecked\" })",
68- "FnDef(DefId { id: 16, name: \"std::slice::SliceIndex::get_unchecked\" })",
69- "FnDef(DefId { id: 14, name: \"std::str::pattern::ReverseSearcher::next_reject_back\" })",
70- "FnDef(DefId { id: 18, name: \"std::str::pattern::ReverseSearcher::next_back\" })",
71- "FnDef(DefId { id: 13, name: \"std::str::pattern::Searcher::next_reject\" })",
72- "FnDef(DefId { id: 19, name: \"std::str::pattern::Searcher::next\" })",
73- "FnDef(DefId { id: 12, name: \"std::str::pattern::Pattern::into_searcher\" })"
74- ]
75- },
76- {
77- "file": "tests/standard_proof.rs",
78- "attrs": [],
79- "func": "pub fn func1() {\n let _a = \"\".trim();\n }",
80- "callees": [
81- "FnDef(DefId { id: 8, name: \"core::str::<impl str>::trim\" })",
82- "FnDef(DefId { id: 9, name: \"core::str::<impl str>::trim_matches\" })",
83- "FnDef(DefId { id: 15, name: \"core::str::<impl str>::get_unchecked\" })",
84- "FnDef(DefId { id: 16, name: \"std::slice::SliceIndex::get_unchecked\" })",
85- "FnDef(DefId { id: 14, name: \"std::str::pattern::ReverseSearcher::next_reject_back\" })",
86- "FnDef(DefId { id: 18, name: \"std::str::pattern::ReverseSearcher::next_back\" })",
87- "FnDef(DefId { id: 13, name: \"std::str::pattern::Searcher::next_reject\" })",
88- "FnDef(DefId { id: 19, name: \"std::str::pattern::Searcher::next\" })",
89- "FnDef(DefId { id: 12, name: \"std::str::pattern::Pattern::into_searcher\" })"
90- ]
91- }
92- ]"## ] ] . assert_eq ( & stdout) ;
18+ expect_file ! [ "./snapshots/standard_proof.json" ] . assert_eq ( & stdout) ;
9319}
0 commit comments