test: update snapshots

zjp-CN · zjp-CN · commit 93ae1a8b4d3b · 2025-04-14T21:06:34.000+08:00
diff --git a/tests/snapshots/contract1.json b/tests/snapshots/contract1.json
@@ -1,6 +1,6 @@
 [
   {
-    "hash": "184105753039686079962266322442922933558",
+    "hash": "1333061076946858250810580638840992453503",
     "def_id": "DefId { id: 13, name: \"verify::f\" }",
     "file": "tests/compare/contract.rs",
     "attrs": [
@@ -1220,7 +1220,7 @@
       },
       {
         "def_id": "DefId { id: 14, name: \"kani::panic\" }",
-        "file": "/home/zjp/rust/kani/library/kani_core/src/lib.rs",
+        "file": "/home/zjp/rust/distributed-verification/kani/library/kani_core/src/lib.rs",
         "func": "pub const fn panic(message: &'static str) -> ! {\n            panic!(\"{}\", message)\n        }"
       },
       {
diff --git a/tests/snapshots/contract2.json b/tests/snapshots/contract2.json
@@ -1,6 +1,6 @@
 [
   {
-    "hash": "184105753039686079962266322442922933558",
+    "hash": "1333061076946858250810580638840992453503",
     "def_id": "DefId { id: 13, name: \"verify::f\" }",
     "file": "tests/compare/contract.rs",
     "attrs": [
@@ -1220,7 +1220,7 @@
       },
       {
         "def_id": "DefId { id: 27, name: \"kani::panic\" }",
-        "file": "/home/zjp/rust/kani/library/kani_core/src/lib.rs",
+        "file": "/home/zjp/rust/distributed-verification/kani/library/kani_core/src/lib.rs",
         "func": "pub const fn panic(message: &'static str) -> ! {\n            panic!(\"{}\", message)\n        }"
       },
       {
diff --git a/tests/snapshots/proof1.json b/tests/snapshots/proof1.json
@@ -1,6 +1,6 @@
 [
   {
-    "hash": "575801690269439979516926484838947128219",
+    "hash": "1080390447388388208111011526646376797302",
     "def_id": "DefId { id: 0, name: \"verify::f\" }",
     "file": "tests/compare/proof.rs",
     "attrs": [
@@ -10,7 +10,7 @@
     "callees": [
       {
         "def_id": "DefId { id: 1, name: \"kani::assert\" }",
-        "file": "/home/zjp/rust/kani/library/kani_core/src/lib.rs",
+        "file": "/home/zjp/rust/distributed-verification/kani/library/kani_core/src/lib.rs",
         "func": "pub const fn assert(cond: bool, msg: &'static str) {\n            let _ = cond;\n            let _ = msg;\n        }"
       }
     ]
diff --git a/tests/snapshots/proof2.json b/tests/snapshots/proof2.json
@@ -1,6 +1,6 @@
 [
   {
-    "hash": "575801690269439979516926484838947128219",
+    "hash": "1080390447388388208111011526646376797302",
     "def_id": "DefId { id: 0, name: \"verify::f\" }",
     "file": "tests/compare/proof.rs",
     "attrs": [
@@ -10,13 +10,13 @@
     "callees": [
       {
         "def_id": "DefId { id: 2, name: \"kani::assert\" }",
-        "file": "/home/zjp/rust/kani/library/kani_core/src/lib.rs",
+        "file": "/home/zjp/rust/distributed-verification/kani/library/kani_core/src/lib.rs",
         "func": "pub const fn assert(cond: bool, msg: &'static str) {\n            let _ = cond;\n            let _ = msg;\n        }"
       }
     ]
   },
   {
-    "hash": "288546599094382361312687918975298218807",
+    "hash": "111100297692849598313316231646472092130",
     "def_id": "DefId { id: 1, name: \"verify::g\" }",
     "file": "tests/compare/proof.rs",
     "attrs": [
@@ -26,7 +26,7 @@
     "callees": [
       {
         "def_id": "DefId { id: 2, name: \"kani::assert\" }",
-        "file": "/home/zjp/rust/kani/library/kani_core/src/lib.rs",
+        "file": "/home/zjp/rust/distributed-verification/kani/library/kani_core/src/lib.rs",
         "func": "pub const fn assert(cond: bool, msg: &'static str) {\n            let _ = cond;\n            let _ = msg;\n        }"
       }
     ]
diff --git a/tests/snapshots/standard_proofs.json b/tests/snapshots/standard_proofs.json
@@ -10,7 +10,7 @@
     "callees": []
   },
   {
-    "hash": "154269283551974763216917429380903124467",
+    "hash": "598200882196848966016444482128164260930",
     "def_id": "DefId { id: 0, name: \"verify::standard_proof\" }",
     "file": "tests/proofs/standard_proofs.rs",
     "attrs": [
@@ -20,32 +20,32 @@
     "callees": [
       {
         "def_id": "DefId { id: 8, name: \"<u8 as kani::Arbitrary>::any\" }",
-        "file": "/home/zjp/rust/kani/library/kani_core/src/arbitrary.rs",
+        "file": "/home/zjp/rust/distributed-verification/kani/library/kani_core/src/arbitrary.rs",
         "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                    }"
       },
       {
         "def_id": "DefId { id: 10, name: \"kani::any_raw\" }",
-        "file": "/home/zjp/rust/kani/library/kani_core/src/lib.rs",
+        "file": "/home/zjp/rust/distributed-verification/kani/library/kani_core/src/lib.rs",
         "func": "fn any_raw<T: Copy>() -> T {\n            kani_intrinsic()\n        }"
       },
       {
         "def_id": "DefId { id: 11, name: \"kani::kani_intrinsic\" }",
-        "file": "/home/zjp/rust/kani/library/kani_core/src/lib.rs",
+        "file": "/home/zjp/rust/distributed-verification/kani/library/kani_core/src/lib.rs",
         "func": "fn kani_intrinsic<T>() -> T {\n            #[allow(clippy::empty_loop)]\n            loop {}\n        }"
       },
       {
         "def_id": "DefId { id: 6, name: \"kani::assert\" }",
-        "file": "/home/zjp/rust/kani/library/kani_core/src/lib.rs",
+        "file": "/home/zjp/rust/distributed-verification/kani/library/kani_core/src/lib.rs",
         "func": "pub const fn assert(cond: bool, msg: &'static str) {\n            let _ = cond;\n            let _ = msg;\n        }"
       },
       {
         "def_id": "DefId { id: 5, name: \"kani::any\" }",
-        "file": "/home/zjp/rust/kani/library/kani_core/src/lib.rs",
+        "file": "/home/zjp/rust/distributed-verification/kani/library/kani_core/src/lib.rs",
         "func": "pub fn any<T: Arbitrary>() -> T {\n            T::any()\n        }"
       },
       {
         "def_id": "DefId { id: 9, name: \"kani::any_raw_internal\" }",
-        "file": "/home/zjp/rust/kani/library/kani_core/src/lib.rs",
+        "file": "/home/zjp/rust/distributed-verification/kani/library/kani_core/src/lib.rs",
         "func": "unsafe fn any_raw_internal<T: Copy>() -> T {\n            any_raw::<T>()\n        }"
       }
     ]
diff --git a/tests/snapshots/standard_proofs_with_contracts.json b/tests/snapshots/standard_proofs_with_contracts.json
@@ -1,6 +1,6 @@
 [
   {
-    "hash": "638100731549357801415843699110435929671",
+    "hash": "1025309838735755950413656814657831068918",
     "def_id": "DefId { id: 13, name: \"verify::standard_proof_with_contract_requires\" }",
     "file": "tests/proofs/standard_proofs_with_contracts.rs",
     "attrs": [
@@ -1220,7 +1220,7 @@
       },
       {
         "def_id": "DefId { id: 33, name: \"kani::panic\" }",
-        "file": "/home/zjp/rust/kani/library/kani_core/src/lib.rs",
+        "file": "/home/zjp/rust/distributed-verification/kani/library/kani_core/src/lib.rs",
         "func": "pub const fn panic(message: &'static str) -> ! {\n            panic!(\"{}\", message)\n        }"
       },
       {
@@ -1256,7 +1256,7 @@
     ]
   },
   {
-    "hash": "153447193349631547573109754293264803070",
+    "hash": "1317424779862856706714064197163667502053",
     "def_id": "DefId { id: 32, name: \"verify::standard_proof_with_contract_ensures\" }",
     "file": "tests/proofs/standard_proofs_with_contracts.rs",
     "attrs": [
@@ -2476,7 +2476,7 @@
       },
       {
         "def_id": "DefId { id: 33, name: \"kani::panic\" }",
-        "file": "/home/zjp/rust/kani/library/kani_core/src/lib.rs",
+        "file": "/home/zjp/rust/distributed-verification/kani/library/kani_core/src/lib.rs",
         "func": "pub const fn panic(message: &'static str) -> ! {\n            panic!(\"{}\", message)\n        }"
       },
       {

Original file line number	Diff line number	Diff line change
`@@ -1,6 +1,6 @@`
`1`	`1`	`[`
`2`	`2`	`{`
`3`		`- "hash": "184105753039686079962266322442922933558",`
	`3`	`+ "hash": "1333061076946858250810580638840992453503",`
`4`	`4`	`"def_id": "DefId { id: 13, name: \"verify::f\" }",`
`5`	`5`	`"file": "tests/compare/contract.rs",`
`6`	`6`	`"attrs": [`
`@@ -1220,7 +1220,7 @@`
`1220`	`1220`	`},`
`1221`	`1221`	`{`
`1222`	`1222`	`"def_id": "DefId { id: 14, name: \"kani::panic\" }",`
`1223`		`- "file": "/home/zjp/rust/kani/library/kani_core/src/lib.rs",`
	`1223`	`+ "file": "/home/zjp/rust/distributed-verification/kani/library/kani_core/src/lib.rs",`
`1224`	`1224`	`"func": "pub const fn panic(message: &'static str) -> ! {\n panic!(\"{}\", message)\n }"`
`1225`	`1225`	`},`
`1226`	`1226`	`{`
Original file line number	Diff line number	Diff line change
`@@ -1,6 +1,6 @@`
`1`	`1`	`[`
`2`	`2`	`{`
`3`		`- "hash": "575801690269439979516926484838947128219",`
	`3`	`+ "hash": "1080390447388388208111011526646376797302",`
`4`	`4`	`"def_id": "DefId { id: 0, name: \"verify::f\" }",`
`5`	`5`	`"file": "tests/compare/proof.rs",`
`6`	`6`	`"attrs": [`
`@@ -10,7 +10,7 @@`
`10`	`10`	`"callees": [`
`11`	`11`	`{`
`12`	`12`	`"def_id": "DefId { id: 1, name: \"kani::assert\" }",`
`13`		`- "file": "/home/zjp/rust/kani/library/kani_core/src/lib.rs",`
	`13`	`+ "file": "/home/zjp/rust/distributed-verification/kani/library/kani_core/src/lib.rs",`
`14`	`14`	`"func": "pub const fn assert(cond: bool, msg: &'static str) {\n let _ = cond;\n let _ = msg;\n }"`
`15`	`15`	`}`
`16`	`16`	`]`
Original file line number	Diff line number	Diff line change
`@@ -1,6 +1,6 @@`
`1`	`1`	`[`
`2`	`2`	`{`
`3`		`- "hash": "638100731549357801415843699110435929671",`
	`3`	`+ "hash": "1025309838735755950413656814657831068918",`
`4`	`4`	`"def_id": "DefId { id: 13, name: \"verify::standard_proof_with_contract_requires\" }",`
`5`	`5`	`"file": "tests/proofs/standard_proofs_with_contracts.rs",`
`6`	`6`	`"attrs": [`
`@@ -1220,7 +1220,7 @@`
`1220`	`1220`	`},`
`1221`	`1221`	`{`
`1222`	`1222`	`"def_id": "DefId { id: 33, name: \"kani::panic\" }",`
`1223`		`- "file": "/home/zjp/rust/kani/library/kani_core/src/lib.rs",`
	`1223`	`+ "file": "/home/zjp/rust/distributed-verification/kani/library/kani_core/src/lib.rs",`
`1224`	`1224`	`"func": "pub const fn panic(message: &'static str) -> ! {\n panic!(\"{}\", message)\n }"`
`1225`	`1225`	`},`
`1226`	`1226`	`{`
`@@ -1256,7 +1256,7 @@`
`1256`	`1256`	`]`
`1257`	`1257`	`},`
`1258`	`1258`	`{`
`1259`		`- "hash": "153447193349631547573109754293264803070",`
	`1259`	`+ "hash": "1317424779862856706714064197163667502053",`
`1260`	`1260`	`"def_id": "DefId { id: 32, name: \"verify::standard_proof_with_contract_ensures\" }",`
`1261`	`1261`	`"file": "tests/proofs/standard_proofs_with_contracts.rs",`
`1262`	`1262`	`"attrs": [`
`@@ -2476,7 +2476,7 @@`
`2476`	`2476`	`},`
`2477`	`2477`	`{`
`2478`	`2478`	`"def_id": "DefId { id: 33, name: \"kani::panic\" }",`
`2479`		`- "file": "/home/zjp/rust/kani/library/kani_core/src/lib.rs",`
	`2479`	`+ "file": "/home/zjp/rust/distributed-verification/kani/library/kani_core/src/lib.rs",`
`2480`	`2480`	`"func": "pub const fn panic(message: &'static str) -> ! {\n panic!(\"{}\", message)\n }"`
`2481`	`2481`	`},`
`2482`	`2482`	`{`