bless, add surrounding error context for postconditions too

Author: Aurel300

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
                 }

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)]

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)]

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)"]