test: automatically generate jsons for proofs

This commit moves standard_proofs and standard_proofs_with_contracts
to proofs folder.

Since the file path to proofs change, hash values change.

Author: zjp-CN

tests/proofs.rs

@@ -0,0 +1,32 @@
+mod utils;
+use utils::*;
+
+#[test]
+fn test_proofs() -> eyre::Result<()> {
+    let mut proofs = vec![];
+    for entry in std::fs::read_dir("tests/proofs")? {
+        let entry = entry?;
+        let path = entry.path();
+        if path.is_file()
+            && path.extension().and_then(|ext| Some(ext.to_str()? == "rs")).unwrap_or(false)
+        {
+            proofs.push(path);
+        }
+    }
+
+    expect![[r#"
+        [
+            "tests/proofs/standard_proofs_with_contracts.rs",
+            "tests/proofs/standard_proofs.rs",
+        ]
+    "#]]
+    .assert_debug_eq(&proofs);
+
+    for path in &proofs {
+        let file_stem = path.file_stem().and_then(|f| f.to_str()).unwrap();
+        let json = cmd(&[&format!("tests/proofs/{file_stem}.rs")]);
+        expect_file![format!("./snapshots/{file_stem}.json")].assert_eq(&json);
+    }
+
+    Ok(())
+}

tests/standard_proofs.rs renamed to tests/proofs/standard_proofs.rs

@@ -1,18 +1,18 @@
 [
   {
-    "hash": "42109808322873561223875447740690337681",
+    "hash": "46975737574545431849805961234274153517",
     "def_id": "DefId { id: 1, name: \"verify::standard_proof_empty\" }",
-    "file": "tests/standard_proofs.rs",
+    "file": "tests/proofs/standard_proofs.rs",
     "attrs": [
       "#[kanitool::proof]"
     ],
     "func": "fn standard_proof_empty() {}",
     "callees": []
   },
   {
-    "hash": "119935654822495658609677948466451012436",
+    "hash": "154269283551974763216917429380903124467",
     "def_id": "DefId { id: 0, name: \"verify::standard_proof\" }",
-    "file": "tests/standard_proofs.rs",
+    "file": "tests/proofs/standard_proofs.rs",
     "attrs": [
       "#[kanitool::proof]"
     ],
@@ -51,9 +51,9 @@
     ]
   },
   {
-    "hash": "353125589356689115114026576863231049982",
+    "hash": "58801092890548413495612860413695445693",
     "def_id": "DefId { id: 2, name: \"verify::recursive_callees\" }",
-    "file": "tests/standard_proofs.rs",
+    "file": "tests/proofs/standard_proofs.rs",
     "attrs": [
       "#[kanitool::proof]"
     ],
@@ -596,12 +596,12 @@
       },
       {
         "def_id": "DefId { id: 4, name: \"m::func1\" }",
-        "file": "tests/standard_proofs.rs",
+        "file": "tests/proofs/standard_proofs.rs",
         "func": "pub fn func1() {\n        let _a = \"\".trim();\n    }"
       },
       {
         "def_id": "DefId { id: 3, name: \"top_level\" }",
-        "file": "tests/standard_proofs.rs",
+        "file": "tests/proofs/standard_proofs.rs",
         "func": "pub fn top_level() {\n    m::func1();\n}"
       }
     ]

tests/standard_proofs_with_contracts.rs renamed to tests/proofs/standard_proofs_with_contracts.rs

@@ -1,8 +1,8 @@
 [
   {
-    "hash": "883956136257843376812272307543917525328",
+    "hash": "638100731549357801415843699110435929671",
     "def_id": "DefId { id: 13, name: \"verify::standard_proof_with_contract_requires\" }",
-    "file": "tests/standard_proofs_with_contracts.rs",
+    "file": "tests/proofs/standard_proofs_with_contracts.rs",
     "attrs": [
       "#[kanitool::proof]"
     ],
@@ -1225,40 +1225,40 @@
       },
       {
         "def_id": "DefId { id: 0, name: \"verify::contract_requires\" }",
-        "file": "tests/standard_proofs_with_contracts.rs",
+        "file": "tests/proofs/standard_proofs_with_contracts.rs",
         "func": "#[kani::requires(a > 0)]"
       },
       {
         "def_id": "DefId { id: 1, name: \"verify::contract_requires::kani_register_contract\" }",
-        "file": "tests/standard_proofs_with_contracts.rs",
+        "file": "tests/proofs/standard_proofs_with_contracts.rs",
         "func": "#[kani::requires(a > 0)]"
       },
       {
         "def_id": "DefId { id: 1, name: \"verify::contract_requires::kani_register_contract\" }",
-        "file": "tests/standard_proofs_with_contracts.rs",
+        "file": "tests/proofs/standard_proofs_with_contracts.rs",
         "func": "#[kani::requires(a > 0)]"
       },
       {
         "def_id": "DefId { id: 2, name: \"verify::contract_requires::kani_contract_mode\" }",
-        "file": "tests/standard_proofs_with_contracts.rs",
+        "file": "tests/proofs/standard_proofs_with_contracts.rs",
         "func": "#[kani::requires(a > 0)]"
       },
       {
         "def_id": "DefId { id: 1, name: \"verify::contract_requires::kani_register_contract\" }",
-        "file": "tests/standard_proofs_with_contracts.rs",
+        "file": "tests/proofs/standard_proofs_with_contracts.rs",
         "func": "#[kani::requires(a > 0)]"
       },
       {
         "def_id": "DefId { id: 1, name: \"verify::contract_requires::kani_register_contract\" }",
-        "file": "tests/standard_proofs_with_contracts.rs",
+        "file": "tests/proofs/standard_proofs_with_contracts.rs",
         "func": "#[kani::requires(a > 0)]"
       }
     ]
   },
   {
-    "hash": "1209015469125850433012148577517296907918",
+    "hash": "153447193349631547573109754293264803070",
     "def_id": "DefId { id: 32, name: \"verify::standard_proof_with_contract_ensures\" }",
-    "file": "tests/standard_proofs_with_contracts.rs",
+    "file": "tests/proofs/standard_proofs_with_contracts.rs",
     "attrs": [
       "#[kanitool::proof]"
     ],
@@ -2481,32 +2481,32 @@
       },
       {
         "def_id": "DefId { id: 14, name: \"verify::contract_ensures\" }",
-        "file": "tests/standard_proofs_with_contracts.rs",
+        "file": "tests/proofs/standard_proofs_with_contracts.rs",
         "func": "#[kani::ensures(|&ret| ret > 0)]"
       },
       {
         "def_id": "DefId { id: 16, name: \"verify::contract_ensures::kani_contract_mode\" }",
-        "file": "tests/standard_proofs_with_contracts.rs",
+        "file": "tests/proofs/standard_proofs_with_contracts.rs",
         "func": "#[kani::ensures(|&ret| ret > 0)]"
       },
       {
         "def_id": "DefId { id: 15, name: \"verify::contract_ensures::kani_register_contract\" }",
-        "file": "tests/standard_proofs_with_contracts.rs",
+        "file": "tests/proofs/standard_proofs_with_contracts.rs",
         "func": "#[kani::ensures(|&ret| ret > 0)]"
       },
       {
         "def_id": "DefId { id: 15, name: \"verify::contract_ensures::kani_register_contract\" }",
-        "file": "tests/standard_proofs_with_contracts.rs",
+        "file": "tests/proofs/standard_proofs_with_contracts.rs",
         "func": "#[kani::ensures(|&ret| ret > 0)]"
       },
       {
         "def_id": "DefId { id: 15, name: \"verify::contract_ensures::kani_register_contract\" }",
-        "file": "tests/standard_proofs_with_contracts.rs",
+        "file": "tests/proofs/standard_proofs_with_contracts.rs",
         "func": "#[kani::ensures(|&ret| ret > 0)]"
       },
       {
         "def_id": "DefId { id: 15, name: \"verify::contract_ensures::kani_register_contract\" }",
-        "file": "tests/standard_proofs_with_contracts.rs",
+        "file": "tests/proofs/standard_proofs_with_contracts.rs",
         "func": "#[kani::ensures(|&ret| ret > 0)]"
       }
     ]

tests/snapshots.rs

@@ -1,6 +1,7 @@
 use assert_cmd::Command;
 
-pub use expect_test::expect_file;
+#[allow(unused_imports)] // seems a bug in clippy
+pub use expect_test::{expect, expect_file};
 #[allow(unused_imports)] // seems a bug in clippy
 pub use pretty_assertions::assert_eq;