Merge remote-tracking branch 'upstream/master' into runtime-checks

viperproject · Sep 22, 2023 · 5cfb19a · 5cfb19a
2 parents 2f5d8e6 + 24bd4c5
commit 5cfb19a
Show file tree

Hide file tree

Showing 20 changed files with 313 additions and 253 deletions.
diff --git a/Cargo.lock b/Cargo.lock
diff --git a/analysis/src/bin/analysis-driver.rs b/analysis/src/bin/analysis-driver.rs
@@ -147,7 +147,6 @@ impl prusti_rustc_interface::driver::Callbacks for OurCompilerCalls {
 
     fn after_analysis<'tcx>(
         &mut self,
-        _error_handler: &EarlyErrorHandler,
         compiler: &interface::Compiler,
         queries: &'tcx Queries<'tcx>,
     ) -> Compilation {

diff --git a/analysis/src/bin/gen-accessibility-driver.rs b/analysis/src/bin/gen-accessibility-driver.rs
@@ -99,7 +99,6 @@ impl prusti_rustc_interface::driver::Callbacks for OurCompilerCalls {
 
     fn after_analysis<'tcx>(
         &mut self,
-        _error_handler: &EarlyErrorHandler,
         compiler: &interface::Compiler,
         queries: &'tcx Queries<'tcx>,
     ) -> Compilation {

diff --git a/analysis/tests/test_cases/definitely_initialized/abs.stdout b/analysis/tests/test_cases/definitely_initialized/abs.stdout
@@ -45,14 +45,6 @@ Result for function abs():
           "_6"
         ],
         "statement: _5 = Ge(move _6, const 0_i32)"
-      ],
-      [
-        "state:",
-        [
-          "_1",
-          "_5"
-        ],
-        "statement: StorageDead(_6)"
       ]
     ],
     "state before terminator:",
@@ -78,6 +70,13 @@ Result for function abs():
   ],
   "bb1": [
     [
+      [
+        "state:",
+        [
+          "_1"
+        ],
+        "statement: StorageDead(_6)"
+      ],
       [
         "state:",
         [
@@ -137,6 +136,13 @@ Result for function abs():
   ],
   "bb2": [
     [
+      [
+        "state:",
+        [
+          "_1"
+        ],
+        "statement: StorageDead(_6)"
+      ],
       [
         "state:",
         [

diff --git a/analysis/tests/test_cases/definitely_initialized/repeated_assignment.stdout b/analysis/tests/test_cases/definitely_initialized/repeated_assignment.stdout
@@ -131,15 +131,6 @@ Result for function main():
           "_6"
         ],
         "statement: _5 = Gt(move _6, const 2_i32)"
-      ],
-      [
-        "state:",
-        [
-          "_1",
-          "_2",
-          "_5"
-        ],
-        "statement: StorageDead(_6)"
       ]
     ],
     "state before terminator:",
@@ -168,6 +159,14 @@ Result for function main():
   ],
   "bb2": [
     [
+      [
+        "state:",
+        [
+          "_1",
+          "_2"
+        ],
+        "statement: StorageDead(_6)"
+      ],
       [
         "state:",
         [
@@ -205,6 +204,14 @@ Result for function main():
   ],
   "bb3": [
     [
+      [
+        "state:",
+        [
+          "_1",
+          "_2"
+        ],
+        "statement: StorageDead(_6)"
+      ],
       [
         "state:",
         [