Update the expected output (#234)

viperproject · Oct 9, 2023 · dd19b51 · dd19b51
1 parent 5987a2d
commit dd19b51
Show file tree

Hide file tree

Showing 5 changed files with 70 additions and 26 deletions.
diff --git a/src/test/scenarios/shared/crates/latest_contracts/Cargo.toml b/src/test/scenarios/shared/crates/latest_contracts/Cargo.toml
@@ -4,4 +4,4 @@ version = "0.1.0"
 edition = "2018"
 
 [dependencies]
-prusti-contracts = "0.1"
+prusti-contracts = "*"
diff --git a/src/test/scenarios/shared/programs/failing_post.rs.json b/src/test/scenarios/shared/programs/failing_post.rs.json
@@ -1,34 +1,78 @@
 [
     {
-        "message": "[Prusti: verification error] postcondition might not hold.",
-        "range": {
-            "end": {
-                "character": 35,
-                "line": 9
-            },
-            "start": {
-                "character": 10,
-                "line": 9
-            }
+        "filter": {
+            "prustiVersion": "Tag",
+            "prustiTag": "v-2023-08-22-1715"
         },
-        "relatedInformation": [
+        "diagnostics": [
             {
-                "location": {
-                    "range": {
-                        "end": {
-                            "character": 20,
-                            "line": 10
+                "message": "[Prusti: verification error] postcondition might not hold.",
+                "range": {
+                    "end": {
+                        "character": 35,
+                        "line": 9
+                    },
+                    "start": {
+                        "character": 10,
+                        "line": 9
+                    }
+                },
+                "relatedInformation": [
+                    {
+                        "location": {
+                            "range": {
+                                "end": {
+                                    "character": 20,
+                                    "line": 10
+                                },
+                                "start": {
+                                    "character": 0,
+                                    "line": 10
+                                }
+                            },
+                            "uri": "programs/failing_post.rs"
                         },
-                        "start": {
-                            "character": 0,
-                            "line": 10
-                        }
+                        "message": "the error originates here"
+                    }
+                ],
+                "severity": 0
+            }
+        ]
+    },
+    {
+        "diagnostics": [
+            {
+                "message": "[Prusti: verification error] postcondition might not hold.",
+                "range": {
+                    "end": {
+                        "character": 35,
+                        "line": 9
                     },
-                    "uri": "programs/failing_post.rs"
+                    "start": {
+                        "character": 30,
+                        "line": 9
+                    }
                 },
-                "message": "the error originates here"
+                "relatedInformation": [
+                    {
+                        "location": {
+                            "range": {
+                                "end": {
+                                    "character": 20,
+                                    "line": 10
+                                },
+                                "start": {
+                                    "character": 0,
+                                    "line": 10
+                                }
+                            },
+                            "uri": "programs/failing_post.rs"
+                        },
+                        "message": "the error originates here"
+                    }
+                ],
+                "severity": 0
             }
-        ],
-        "severity": 0
+        ]
     }
 ]
diff --git a/...os/shared/crates/contracts_0.1/Cargo.toml → ...edVersion/crates/contracts_0.1/Cargo.toml b/...os/shared/crates/contracts_0.1/Cargo.toml → ...edVersion/crates/contracts_0.1/Cargo.toml
@@ -4,4 +4,4 @@ version = "0.1.0"
 edition = "2018"
 
 [dependencies]
-prusti-contracts = "*"
+prusti-contracts = "0.1"
diff --git a/...s/shared/crates/contracts_0.1/src/main.rs → ...dVersion/crates/contracts_0.1/src/main.rs b/...s/shared/crates/contracts_0.1/src/main.rs → ...dVersion/crates/contracts_0.1/src/main.rs
diff --git a/...red/crates/contracts_0.1/src/main.rs.json → ...ion/crates/contracts_0.1/src/main.rs.json b/...red/crates/contracts_0.1/src/main.rs.json → ...ion/crates/contracts_0.1/src/main.rs.json