bless, add surrounding error context for postconditions too

viperproject · Jul 18, 2023 · d49abc7 · d49abc7
1 parent 8188d32
commit d49abc7
Show file tree

Hide file tree

Showing 31 changed files with 615 additions and 446 deletions.
diff --git a/prusti-interface/src/environment/loops.rs b/prusti-interface/src/environment/loops.rs
@@ -123,6 +123,7 @@ impl<'b, 'tcx> Visitor<'tcx> for AccessCollector<'b, 'tcx> {
                 NonMutatingUse(mir::visit::NonMutatingUseContext::Copy) => PlaceAccessKind::Read,
                 NonMutatingUse(mir::visit::NonMutatingUseContext::Move) => PlaceAccessKind::Move,
                 NonMutatingUse(mir::visit::NonMutatingUseContext::Inspect) => PlaceAccessKind::Read,
+                NonMutatingUse(mir::visit::NonMutatingUseContext::PlaceMention) => PlaceAccessKind::Read,
                 NonMutatingUse(mir::visit::NonMutatingUseContext::SharedBorrow) => {
                     PlaceAccessKind::SharedBorrow
                 }

diff --git a/prusti-tests/tests/compiletest.rs b/prusti-tests/tests/compiletest.rs
@@ -178,7 +178,7 @@ fn test_runner(_tests: &[&()]) {
 
     // Filter the tests to run
     let filter = env::args().nth(1);
-
+    /*
     // Test the parsing of specifications. This doesn't run the verifier.
     println!("[parse]");
     run_no_verification("parse", &filter);
@@ -191,7 +191,7 @@ fn test_runner(_tests: &[&()]) {
     println!("[verify]");
     run_verification_no_overflow("verify", &filter);
     save_verification_cache();
-
+*/
     // Test the verifier with overflow checks enabled.
     println!("[verify_overflow]");
     run_verification_overflow("verify_overflow", &filter);

diff --git a/prusti-tests/tests/parse/ui/after_expiry.stdout b/prusti-tests/tests/parse/ui/after_expiry.stdout
@@ -8,7 +8,6 @@
 
 
 
-#![feature(type_ascription)]
 #![feature(stmt_expr_attributes)]
 #![feature(register_tool)]
 #![register_tool(prusti)]
@@ -23,7 +22,8 @@ non_snake_case)]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pledge_item_test1_$(NUM_UUID)(a: bool,
     result: ()) -> bool {
-    !!((a): bool)
+    let prusti_result: bool = a;
+    prusti_result
 }
 #[prusti::pledge_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -34,7 +34,8 @@ non_snake_case)]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pledge_item_test2_$(NUM_UUID)(a: bool,
     result: ()) -> bool {
-    !!((a): bool)
+    let prusti_result: bool = a;
+    prusti_result
 }
 #[prusti::pledge_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -45,7 +46,8 @@ non_snake_case)]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pledge_item_test3_$(NUM_UUID)(x: u32,
     result: u32) -> bool {
-    !!((result == match x { 1 => 1, 2 => 2, _ => 0, }): bool)
+    let prusti_result: bool = result == match x { 1 => 1, 2 => 2, _ => 0, };
+    prusti_result
 }
 #[prusti::pledge_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]

diff --git a/prusti-tests/tests/parse/ui/and.stdout b/prusti-tests/tests/parse/ui/and.stdout
@@ -10,7 +10,6 @@
 
 
 
-#![feature(type_ascription)]
 #![feature(stmt_expr_attributes)]
 #![feature(register_tool)]
 #![register_tool(prusti)]
@@ -24,7 +23,8 @@ non_snake_case)]
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test1_$(NUM_UUID)() -> bool {
-    !!(((true) && (true)): bool)
+    let prusti_result: bool = (true) && (true);
+    prusti_result
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -34,7 +34,8 @@ non_snake_case)]
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test2_$(NUM_UUID)() -> bool {
-    !!((((true) && (true)) && (true)): bool)
+    let prusti_result: bool = ((true) && (true)) && (true);
+    prusti_result
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -44,7 +45,8 @@ non_snake_case)]
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test3_$(NUM_UUID)() -> bool {
-    !!(((true) && (((true) && (true)))): bool)
+    let prusti_result: bool = (true) && (((true) && (true)));
+    prusti_result
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -54,7 +56,8 @@ non_snake_case)]
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test4_$(NUM_UUID)() -> bool {
-    !!(((((true) && (true))) && (true)): bool)
+    let prusti_result: bool = (((true) && (true))) && (true);
+    prusti_result
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -64,7 +67,8 @@ non_snake_case)]
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test5_$(NUM_UUID)() -> bool {
-    !!(((((true) && (true))) && (((true) && (true)))): bool)
+    let prusti_result: bool = (((true) && (true))) && (((true) && (true)));
+    prusti_result
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]

diff --git a/prusti-tests/tests/parse/ui/assert_on_expiry.stdout b/prusti-tests/tests/parse/ui/assert_on_expiry.stdout
@@ -9,7 +9,6 @@
 
 
 
-#![feature(type_ascription)]
 #![feature(stmt_expr_attributes)]
 #![feature(register_tool)]
 #![register_tool(prusti)]
@@ -24,15 +23,17 @@ non_snake_case)]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pledge_item_test1_$(NUM_UUID)(a: bool,
     result: ()) -> bool {
-    !!((true): bool)
+    let prusti_result: bool = true;
+    prusti_result
 }
 #[allow(unused_must_use, unused_parens, unused_variables, dead_code,
 non_snake_case)]
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pledge_item_test1_$(NUM_UUID)(a: bool,
     result: ()) -> bool {
-    !!((a): bool)
+    let prusti_result: bool = a;
+    prusti_result
 }
 #[prusti::assert_pledge_spec_id_ref_lhs = "$(NUM_UUID)"]
 #[prusti::assert_pledge_spec_id_ref_rhs = "$(NUM_UUID)"]
@@ -44,15 +45,17 @@ non_snake_case)]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pledge_item_test2_$(NUM_UUID)(a: bool,
     result: ()) -> bool {
-    !!((true): bool)
+    let prusti_result: bool = true;
+    prusti_result
 }
 #[allow(unused_must_use, unused_parens, unused_variables, dead_code,
 non_snake_case)]
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pledge_item_test2_$(NUM_UUID)(a: bool,
     result: ()) -> bool {
-    !!((a): bool)
+    let prusti_result: bool = a;
+    prusti_result
 }
 #[prusti::assert_pledge_spec_id_ref_lhs = "$(NUM_UUID)"]
 #[prusti::assert_pledge_spec_id_ref_rhs = "$(NUM_UUID)"]
@@ -64,15 +67,17 @@ non_snake_case)]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pledge_item_test3_$(NUM_UUID)(x: u32,
     result: u32) -> bool {
-    !!((true): bool)
+    let prusti_result: bool = true;
+    prusti_result
 }
 #[allow(unused_must_use, unused_parens, unused_variables, dead_code,
 non_snake_case)]
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pledge_item_test3_$(NUM_UUID)(x: u32,
     result: u32) -> bool {
-    !!((result == match x { 1 => 1, 2 => 2, _ => 0, }): bool)
+    let prusti_result: bool = result == match x { 1 => 1, 2 => 2, _ => 0, };
+    prusti_result
 }
 #[prusti::assert_pledge_spec_id_ref_lhs = "$(NUM_UUID)"]
 #[prusti::assert_pledge_spec_id_ref_rhs = "$(NUM_UUID)"]