test: update snapshots

zjp-CN · zjp-CN · commit cb4e38b0d834 · 2025-04-12T18:16:46.000+08:00
diff --git a/tests/snapshots/standard_proofs.json b/tests/snapshots/standard_proofs.json
@@ -1,5 +1,6 @@
 [
   {
+    "hash": "42109808322873561223875447740690337681",
     "def_id": "DefId { id: 1, name: \"verify::standard_proof_empty\" }",
     "file": "tests/standard_proofs.rs",
     "attrs": [
@@ -9,6 +10,7 @@
     "callees": []
   },
   {
+    "hash": "98192936616641250112552906219302378668",
     "def_id": "DefId { id: 0, name: \"verify::standard_proof\" }",
     "file": "tests/standard_proofs.rs",
     "attrs": [
@@ -49,6 +51,7 @@
     ]
   },
   {
+    "hash": "119307450917325760212416660484109988218",
     "def_id": "DefId { id: 2, name: \"verify::recursive_callees\" }",
     "file": "tests/standard_proofs.rs",
     "attrs": [
diff --git a/tests/snapshots/standard_proofs_with_contracts.json b/tests/snapshots/standard_proofs_with_contracts.json
@@ -1,15 +1,16 @@
-[2m2025-04-12T09:32:48.206104Z[0m [31mERROR[0m [1mall_local_items[0m[1m{[0m[3mitem[0m[2m=[0mCrateItem(DefId { id: 1, name: "verify::contract1::kani_register_contract" })[1m}[0m[2m:[0m [2mdistributed_verification::functions[0m[2m:[0m [3merr[0m[2m=[0mError("Item requires monomorphization")
-[2m2025-04-12T09:32:48.206533Z[0m [31mERROR[0m [1mall_local_items[0m[1m{[0m[3mitem[0m[2m=[0mCrateItem(DefId { id: 3, name: "verify::contract1::{closure#0}" })[1m}[0m[2m:[0m [2mdistributed_verification::functions[0m[2m:[0m [3merr[0m[2m=[0mError("Item requires monomorphization")
-[2m2025-04-12T09:32:48.206913Z[0m [31mERROR[0m [1mall_local_items[0m[1m{[0m[3mitem[0m[2m=[0mCrateItem(DefId { id: 5, name: "verify::contract1::{closure#0}::{closure#0}" })[1m}[0m[2m:[0m [2mdistributed_verification::functions[0m[2m:[0m [3merr[0m[2m=[0mError("Item requires monomorphization")
-[2m2025-04-12T09:32:48.207167Z[0m [31mERROR[0m [1mall_local_items[0m[1m{[0m[3mitem[0m[2m=[0mCrateItem(DefId { id: 6, name: "verify::contract1::{closure#0}::{closure#1}" })[1m}[0m[2m:[0m [2mdistributed_verification::functions[0m[2m:[0m [3merr[0m[2m=[0mError("Item requires monomorphization")
-[2m2025-04-12T09:32:48.207418Z[0m [31mERROR[0m [1mall_local_items[0m[1m{[0m[3mitem[0m[2m=[0mCrateItem(DefId { id: 7, name: "verify::contract1::{closure#0}::{closure#1}::{closure#0}" })[1m}[0m[2m:[0m [2mdistributed_verification::functions[0m[2m:[0m [3merr[0m[2m=[0mError("Item requires monomorphization")
-[2m2025-04-12T09:32:48.207668Z[0m [31mERROR[0m [1mall_local_items[0m[1m{[0m[3mitem[0m[2m=[0mCrateItem(DefId { id: 8, name: "verify::contract1::{closure#1}" })[1m}[0m[2m:[0m [2mdistributed_verification::functions[0m[2m:[0m [3merr[0m[2m=[0mError("Item requires monomorphization")
-[2m2025-04-12T09:32:48.207918Z[0m [31mERROR[0m [1mall_local_items[0m[1m{[0m[3mitem[0m[2m=[0mCrateItem(DefId { id: 9, name: "verify::contract1::{closure#2}" })[1m}[0m[2m:[0m [2mdistributed_verification::functions[0m[2m:[0m [3merr[0m[2m=[0mError("Item requires monomorphization")
-[2m2025-04-12T09:32:48.208169Z[0m [31mERROR[0m [1mall_local_items[0m[1m{[0m[3mitem[0m[2m=[0mCrateItem(DefId { id: 10, name: "verify::contract1::{closure#2}::{closure#0}" })[1m}[0m[2m:[0m [2mdistributed_verification::functions[0m[2m:[0m [3merr[0m[2m=[0mError("Item requires monomorphization")
-[2m2025-04-12T09:32:48.208419Z[0m [31mERROR[0m [1mall_local_items[0m[1m{[0m[3mitem[0m[2m=[0mCrateItem(DefId { id: 11, name: "verify::contract1::{closure#3}" })[1m}[0m[2m:[0m [2mdistributed_verification::functions[0m[2m:[0m [3merr[0m[2m=[0mError("Item requires monomorphization")
-[2m2025-04-12T09:32:48.208670Z[0m [31mERROR[0m [1mall_local_items[0m[1m{[0m[3mitem[0m[2m=[0mCrateItem(DefId { id: 12, name: "verify::contract1::{closure#3}::{closure#0}" })[1m}[0m[2m:[0m [2mdistributed_verification::functions[0m[2m:[0m [3merr[0m[2m=[0mError("Item requires monomorphization")
+[2m2025-04-12T10:16:11.295073Z[0m [31mERROR[0m [1mall_local_items[0m[1m{[0m[3mitem[0m[2m=[0mCrateItem(DefId { id: 1, name: "verify::contract1::kani_register_contract" })[1m}[0m[2m:[0m [2mdistributed_verification::functions[0m[2m:[0m [3merr[0m[2m=[0mError("Item requires monomorphization")
+[2m2025-04-12T10:16:11.295497Z[0m [31mERROR[0m [1mall_local_items[0m[1m{[0m[3mitem[0m[2m=[0mCrateItem(DefId { id: 3, name: "verify::contract1::{closure#0}" })[1m}[0m[2m:[0m [2mdistributed_verification::functions[0m[2m:[0m [3merr[0m[2m=[0mError("Item requires monomorphization")
+[2m2025-04-12T10:16:11.295816Z[0m [31mERROR[0m [1mall_local_items[0m[1m{[0m[3mitem[0m[2m=[0mCrateItem(DefId { id: 5, name: "verify::contract1::{closure#0}::{closure#0}" })[1m}[0m[2m:[0m [2mdistributed_verification::functions[0m[2m:[0m [3merr[0m[2m=[0mError("Item requires monomorphization")
+[2m2025-04-12T10:16:11.296068Z[0m [31mERROR[0m [1mall_local_items[0m[1m{[0m[3mitem[0m[2m=[0mCrateItem(DefId { id: 6, name: "verify::contract1::{closure#0}::{closure#1}" })[1m}[0m[2m:[0m [2mdistributed_verification::functions[0m[2m:[0m [3merr[0m[2m=[0mError("Item requires monomorphization")
+[2m2025-04-12T10:16:11.296318Z[0m [31mERROR[0m [1mall_local_items[0m[1m{[0m[3mitem[0m[2m=[0mCrateItem(DefId { id: 7, name: "verify::contract1::{closure#0}::{closure#1}::{closure#0}" })[1m}[0m[2m:[0m [2mdistributed_verification::functions[0m[2m:[0m [3merr[0m[2m=[0mError("Item requires monomorphization")
+[2m2025-04-12T10:16:11.296567Z[0m [31mERROR[0m [1mall_local_items[0m[1m{[0m[3mitem[0m[2m=[0mCrateItem(DefId { id: 8, name: "verify::contract1::{closure#1}" })[1m}[0m[2m:[0m [2mdistributed_verification::functions[0m[2m:[0m [3merr[0m[2m=[0mError("Item requires monomorphization")
+[2m2025-04-12T10:16:11.296815Z[0m [31mERROR[0m [1mall_local_items[0m[1m{[0m[3mitem[0m[2m=[0mCrateItem(DefId { id: 9, name: "verify::contract1::{closure#2}" })[1m}[0m[2m:[0m [2mdistributed_verification::functions[0m[2m:[0m [3merr[0m[2m=[0mError("Item requires monomorphization")
+[2m2025-04-12T10:16:11.297064Z[0m [31mERROR[0m [1mall_local_items[0m[1m{[0m[3mitem[0m[2m=[0mCrateItem(DefId { id: 10, name: "verify::contract1::{closure#2}::{closure#0}" })[1m}[0m[2m:[0m [2mdistributed_verification::functions[0m[2m:[0m [3merr[0m[2m=[0mError("Item requires monomorphization")
+[2m2025-04-12T10:16:11.297311Z[0m [31mERROR[0m [1mall_local_items[0m[1m{[0m[3mitem[0m[2m=[0mCrateItem(DefId { id: 11, name: "verify::contract1::{closure#3}" })[1m}[0m[2m:[0m [2mdistributed_verification::functions[0m[2m:[0m [3merr[0m[2m=[0mError("Item requires monomorphization")
+[2m2025-04-12T10:16:11.297559Z[0m [31mERROR[0m [1mall_local_items[0m[1m{[0m[3mitem[0m[2m=[0mCrateItem(DefId { id: 12, name: "verify::contract1::{closure#3}::{closure#0}" })[1m}[0m[2m:[0m [2mdistributed_verification::functions[0m[2m:[0m [3merr[0m[2m=[0mError("Item requires monomorphization")
 [
   {
+    "hash": "17238183815665182814913666463002909661",
     "def_id": "DefId { id: 13, name: \"verify::standard_proof_with_contract_requires\" }",
     "file": "tests/standard_proofs_with_contracts.rs",
     "attrs": [

Original file line number	Diff line number	Diff line change
`@@ -1,5 +1,6 @@`
`1`	`1`	`[`
`2`	`2`	`{`
	`3`	`+ "hash": "42109808322873561223875447740690337681",`
`3`	`4`	`"def_id": "DefId { id: 1, name: \"verify::standard_proof_empty\" }",`
`4`	`5`	`"file": "tests/standard_proofs.rs",`
`5`	`6`	`"attrs": [`
`@@ -9,6 +10,7 @@`
`9`	`10`	`"callees": []`
`10`	`11`	`},`
`11`	`12`	`{`
	`13`	`+ "hash": "98192936616641250112552906219302378668",`
`12`	`14`	`"def_id": "DefId { id: 0, name: \"verify::standard_proof\" }",`
`13`	`15`	`"file": "tests/standard_proofs.rs",`
`14`	`16`	`"attrs": [`
`@@ -49,6 +51,7 @@`
`49`	`51`	`]`
`50`	`52`	`},`
`51`	`53`	`{`
	`54`	`+ "hash": "119307450917325760212416660484109988218",`
`52`	`55`	`"def_id": "DefId { id: 2, name: \"verify::recursive_callees\" }",`
`53`	`56`	`"file": "tests/standard_proofs.rs",`
`54`	`57`	`"attrs": [`
-Original file line number
+Diff line change
@@ @@ -1,15 +1,16 @@ @@
 -[2m2025-04-12T09:32:48.206104Z[0m [31mERROR[0m [1mall_local_items[0m[1m{[0m[3mitem[0m[2m=[0mCrateItem(DefId { id: 1, name: "verify::contract1::kani_register_contract" })[1m}[0m[2m:[0m [2mdistributed_verification::functions[0m[2m:[0m [3merr[0m[2m=[0mError("Item requires monomorphization")
 -[2m2025-04-12T09:32:48.206533Z[0m [31mERROR[0m [1mall_local_items[0m[1m{[0m[3mitem[0m[2m=[0mCrateItem(DefId { id: 3, name: "verify::contract1::{closure#0}" })[1m}[0m[2m:[0m [2mdistributed_verification::functions[0m[2m:[0m [3merr[0m[2m=[0mError("Item requires monomorphization")
 -[2m2025-04-12T09:32:48.206913Z[0m [31mERROR[0m [1mall_local_items[0m[1m{[0m[3mitem[0m[2m=[0mCrateItem(DefId { id: 5, name: "verify::contract1::{closure#0}::{closure#0}" })[1m}[0m[2m:[0m [2mdistributed_verification::functions[0m[2m:[0m [3merr[0m[2m=[0mError("Item requires monomorphization")
 -[2m2025-04-12T09:32:48.207167Z[0m [31mERROR[0m [1mall_local_items[0m[1m{[0m[3mitem[0m[2m=[0mCrateItem(DefId { id: 6, name: "verify::contract1::{closure#0}::{closure#1}" })[1m}[0m[2m:[0m [2mdistributed_verification::functions[0m[2m:[0m [3merr[0m[2m=[0mError("Item requires monomorphization")
 -[2m2025-04-12T09:32:48.207418Z[0m [31mERROR[0m [1mall_local_items[0m[1m{[0m[3mitem[0m[2m=[0mCrateItem(DefId { id: 7, name: "verify::contract1::{closure#0}::{closure#1}::{closure#0}" })[1m}[0m[2m:[0m [2mdistributed_verification::functions[0m[2m:[0m [3merr[0m[2m=[0mError("Item requires monomorphization")
 -[2m2025-04-12T09:32:48.207668Z[0m [31mERROR[0m [1mall_local_items[0m[1m{[0m[3mitem[0m[2m=[0mCrateItem(DefId { id: 8, name: "verify::contract1::{closure#1}" })[1m}[0m[2m:[0m [2mdistributed_verification::functions[0m[2m:[0m [3merr[0m[2m=[0mError("Item requires monomorphization")
 -[2m2025-04-12T09:32:48.207918Z[0m [31mERROR[0m [1mall_local_items[0m[1m{[0m[3mitem[0m[2m=[0mCrateItem(DefId { id: 9, name: "verify::contract1::{closure#2}" })[1m}[0m[2m:[0m [2mdistributed_verification::functions[0m[2m:[0m [3merr[0m[2m=[0mError("Item requires monomorphization")
 -[2m2025-04-12T09:32:48.208169Z[0m [31mERROR[0m [1mall_local_items[0m[1m{[0m[3mitem[0m[2m=[0mCrateItem(DefId { id: 10, name: "verify::contract1::{closure#2}::{closure#0}" })[1m}[0m[2m:[0m [2mdistributed_verification::functions[0m[2m:[0m [3merr[0m[2m=[0mError("Item requires monomorphization")
 -[2m2025-04-12T09:32:48.208419Z[0m [31mERROR[0m [1mall_local_items[0m[1m{[0m[3mitem[0m[2m=[0mCrateItem(DefId { id: 11, name: "verify::contract1::{closure#3}" })[1m}[0m[2m:[0m [2mdistributed_verification::functions[0m[2m:[0m [3merr[0m[2m=[0mError("Item requires monomorphization")
 -[2m2025-04-12T09:32:48.208670Z[0m [31mERROR[0m [1mall_local_items[0m[1m{[0m[3mitem[0m[2m=[0mCrateItem(DefId { id: 12, name: "verify::contract1::{closure#3}::{closure#0}" })[1m}[0m[2m:[0m [2mdistributed_verification::functions[0m[2m:[0m [3merr[0m[2m=[0mError("Item requires monomorphization")
 +[2m2025-04-12T10:16:11.295073Z[0m [31mERROR[0m [1mall_local_items[0m[1m{[0m[3mitem[0m[2m=[0mCrateItem(DefId { id: 1, name: "verify::contract1::kani_register_contract" })[1m}[0m[2m:[0m [2mdistributed_verification::functions[0m[2m:[0m [3merr[0m[2m=[0mError("Item requires monomorphization")
 +[2m2025-04-12T10:16:11.295497Z[0m [31mERROR[0m [1mall_local_items[0m[1m{[0m[3mitem[0m[2m=[0mCrateItem(DefId { id: 3, name: "verify::contract1::{closure#0}" })[1m}[0m[2m:[0m [2mdistributed_verification::functions[0m[2m:[0m [3merr[0m[2m=[0mError("Item requires monomorphization")
 +[2m2025-04-12T10:16:11.295816Z[0m [31mERROR[0m [1mall_local_items[0m[1m{[0m[3mitem[0m[2m=[0mCrateItem(DefId { id: 5, name: "verify::contract1::{closure#0}::{closure#0}" })[1m}[0m[2m:[0m [2mdistributed_verification::functions[0m[2m:[0m [3merr[0m[2m=[0mError("Item requires monomorphization")
 +[2m2025-04-12T10:16:11.296068Z[0m [31mERROR[0m [1mall_local_items[0m[1m{[0m[3mitem[0m[2m=[0mCrateItem(DefId { id: 6, name: "verify::contract1::{closure#0}::{closure#1}" })[1m}[0m[2m:[0m [2mdistributed_verification::functions[0m[2m:[0m [3merr[0m[2m=[0mError("Item requires monomorphization")
 +[2m2025-04-12T10:16:11.296318Z[0m [31mERROR[0m [1mall_local_items[0m[1m{[0m[3mitem[0m[2m=[0mCrateItem(DefId { id: 7, name: "verify::contract1::{closure#0}::{closure#1}::{closure#0}" })[1m}[0m[2m:[0m [2mdistributed_verification::functions[0m[2m:[0m [3merr[0m[2m=[0mError("Item requires monomorphization")
 +[2m2025-04-12T10:16:11.296567Z[0m [31mERROR[0m [1mall_local_items[0m[1m{[0m[3mitem[0m[2m=[0mCrateItem(DefId { id: 8, name: "verify::contract1::{closure#1}" })[1m}[0m[2m:[0m [2mdistributed_verification::functions[0m[2m:[0m [3merr[0m[2m=[0mError("Item requires monomorphization")
 +[2m2025-04-12T10:16:11.296815Z[0m [31mERROR[0m [1mall_local_items[0m[1m{[0m[3mitem[0m[2m=[0mCrateItem(DefId { id: 9, name: "verify::contract1::{closure#2}" })[1m}[0m[2m:[0m [2mdistributed_verification::functions[0m[2m:[0m [3merr[0m[2m=[0mError("Item requires monomorphization")
 +[2m2025-04-12T10:16:11.297064Z[0m [31mERROR[0m [1mall_local_items[0m[1m{[0m[3mitem[0m[2m=[0mCrateItem(DefId { id: 10, name: "verify::contract1::{closure#2}::{closure#0}" })[1m}[0m[2m:[0m [2mdistributed_verification::functions[0m[2m:[0m [3merr[0m[2m=[0mError("Item requires monomorphization")
 +[2m2025-04-12T10:16:11.297311Z[0m [31mERROR[0m [1mall_local_items[0m[1m{[0m[3mitem[0m[2m=[0mCrateItem(DefId { id: 11, name: "verify::contract1::{closure#3}" })[1m}[0m[2m:[0m [2mdistributed_verification::functions[0m[2m:[0m [3merr[0m[2m=[0mError("Item requires monomorphization")
 +[2m2025-04-12T10:16:11.297559Z[0m [31mERROR[0m [1mall_local_items[0m[1m{[0m[3mitem[0m[2m=[0mCrateItem(DefId { id: 12, name: "verify::contract1::{closure#3}::{closure#0}" })[1m}[0m[2m:[0m [2mdistributed_verification::functions[0m[2m:[0m [3merr[0m[2m=[0mError("Item requires monomorphization")
+[
+  {
 +    "hash": "17238183815665182814913666463002909661",
     "def_id": "DefId { id: 13, name: \"verify::standard_proof_with_contract_requires\" }",
     "file": "tests/standard_proofs_with_contracts.rs",
     "attrs": [