Skip to content

Commit d49abc7

Browse files
Aurel300Aurel300
committed
bless, add surrounding error context for postconditions too
1 parent 8188d32 commit d49abc7

31 files changed

+615
-446
lines changed

‎prusti-interface/src/environment/loops.rs‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -123,6 +123,7 @@ impl<'b, 'tcx> Visitor<'tcx> for AccessCollector<'b, 'tcx> {
123123
NonMutatingUse(mir::visit::NonMutatingUseContext::Copy) => PlaceAccessKind::Read,
124124
NonMutatingUse(mir::visit::NonMutatingUseContext::Move) => PlaceAccessKind::Move,
125125
NonMutatingUse(mir::visit::NonMutatingUseContext::Inspect) => PlaceAccessKind::Read,
126+
NonMutatingUse(mir::visit::NonMutatingUseContext::PlaceMention) => PlaceAccessKind::Read,
126127
NonMutatingUse(mir::visit::NonMutatingUseContext::SharedBorrow) => {
127128
PlaceAccessKind::SharedBorrow
128129
}

‎prusti-tests/tests/compiletest.rs‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -178,7 +178,7 @@ fn test_runner(_tests: &[&()]) {
178178

179179
// Filter the tests to run
180180
let filter = env::args().nth(1);
181-
181+
/*
182182
// Test the parsing of specifications. This doesn't run the verifier.
183183
println!("[parse]");
184184
run_no_verification("parse", &filter);
@@ -191,7 +191,7 @@ fn test_runner(_tests: &[&()]) {
191191
println!("[verify]");
192192
run_verification_no_overflow("verify", &filter);
193193
save_verification_cache();
194-
194+
*/
195195
// Test the verifier with overflow checks enabled.
196196
println!("[verify_overflow]");
197197
run_verification_overflow("verify_overflow", &filter);

‎prusti-tests/tests/parse/ui/after_expiry.stdout‎

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,6 @@
88

99

1010

11-
#![feature(type_ascription)]
1211
#![feature(stmt_expr_attributes)]
1312
#![feature(register_tool)]
1413
#![register_tool(prusti)]
@@ -23,7 +22,8 @@ non_snake_case)]
2322
#[prusti::spec_id = "$(NUM_UUID)"]
2423
fn prusti_pledge_item_test1_$(NUM_UUID)(a: bool,
2524
result: ()) -> bool {
26-
!!((a): bool)
25+
let prusti_result: bool = a;
26+
prusti_result
2727
}
2828
#[prusti::pledge_spec_id_ref = "$(NUM_UUID)"]
2929
#[prusti::specs_version = $(SPECS_VERSION)]
@@ -34,7 +34,8 @@ non_snake_case)]
3434
#[prusti::spec_id = "$(NUM_UUID)"]
3535
fn prusti_pledge_item_test2_$(NUM_UUID)(a: bool,
3636
result: ()) -> bool {
37-
!!((a): bool)
37+
let prusti_result: bool = a;
38+
prusti_result
3839
}
3940
#[prusti::pledge_spec_id_ref = "$(NUM_UUID)"]
4041
#[prusti::specs_version = $(SPECS_VERSION)]
@@ -45,7 +46,8 @@ non_snake_case)]
4546
#[prusti::spec_id = "$(NUM_UUID)"]
4647
fn prusti_pledge_item_test3_$(NUM_UUID)(x: u32,
4748
result: u32) -> bool {
48-
!!((result == match x { 1 => 1, 2 => 2, _ => 0, }): bool)
49+
let prusti_result: bool = result == match x { 1 => 1, 2 => 2, _ => 0, };
50+
prusti_result
4951
}
5052
#[prusti::pledge_spec_id_ref = "$(NUM_UUID)"]
5153
#[prusti::specs_version = $(SPECS_VERSION)]

‎prusti-tests/tests/parse/ui/and.stdout‎

Lines changed: 10 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,6 @@
1010

1111

1212

13-
#![feature(type_ascription)]
1413
#![feature(stmt_expr_attributes)]
1514
#![feature(register_tool)]
1615
#![register_tool(prusti)]
@@ -24,7 +23,8 @@ non_snake_case)]
2423
#[prusti::spec_only]
2524
#[prusti::spec_id = "$(NUM_UUID)"]
2625
fn prusti_pre_item_test1_$(NUM_UUID)() -> bool {
27-
!!(((true) && (true)): bool)
26+
let prusti_result: bool = (true) && (true);
27+
prusti_result
2828
}
2929
#[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
3030
#[prusti::specs_version = $(SPECS_VERSION)]
@@ -34,7 +34,8 @@ non_snake_case)]
3434
#[prusti::spec_only]
3535
#[prusti::spec_id = "$(NUM_UUID)"]
3636
fn prusti_pre_item_test2_$(NUM_UUID)() -> bool {
37-
!!((((true) && (true)) && (true)): bool)
37+
let prusti_result: bool = ((true) && (true)) && (true);
38+
prusti_result
3839
}
3940
#[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
4041
#[prusti::specs_version = $(SPECS_VERSION)]
@@ -44,7 +45,8 @@ non_snake_case)]
4445
#[prusti::spec_only]
4546
#[prusti::spec_id = "$(NUM_UUID)"]
4647
fn prusti_pre_item_test3_$(NUM_UUID)() -> bool {
47-
!!(((true) && (((true) && (true)))): bool)
48+
let prusti_result: bool = (true) && (((true) && (true)));
49+
prusti_result
4850
}
4951
#[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
5052
#[prusti::specs_version = $(SPECS_VERSION)]
@@ -54,7 +56,8 @@ non_snake_case)]
5456
#[prusti::spec_only]
5557
#[prusti::spec_id = "$(NUM_UUID)"]
5658
fn prusti_pre_item_test4_$(NUM_UUID)() -> bool {
57-
!!(((((true) && (true))) && (true)): bool)
59+
let prusti_result: bool = (((true) && (true))) && (true);
60+
prusti_result
5861
}
5962
#[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
6063
#[prusti::specs_version = $(SPECS_VERSION)]
@@ -64,7 +67,8 @@ non_snake_case)]
6467
#[prusti::spec_only]
6568
#[prusti::spec_id = "$(NUM_UUID)"]
6669
fn prusti_pre_item_test5_$(NUM_UUID)() -> bool {
67-
!!(((((true) && (true))) && (((true) && (true)))): bool)
70+
let prusti_result: bool = (((true) && (true))) && (((true) && (true)));
71+
prusti_result
6872
}
6973
#[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
7074
#[prusti::specs_version = $(SPECS_VERSION)]

‎prusti-tests/tests/parse/ui/assert_on_expiry.stdout‎

Lines changed: 12 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,6 @@
99

1010

1111

12-
#![feature(type_ascription)]
1312
#![feature(stmt_expr_attributes)]
1413
#![feature(register_tool)]
1514
#![register_tool(prusti)]
@@ -24,15 +23,17 @@ non_snake_case)]
2423
#[prusti::spec_id = "$(NUM_UUID)"]
2524
fn prusti_pledge_item_test1_$(NUM_UUID)(a: bool,
2625
result: ()) -> bool {
27-
!!((true): bool)
26+
let prusti_result: bool = true;
27+
prusti_result
2828
}
2929
#[allow(unused_must_use, unused_parens, unused_variables, dead_code,
3030
non_snake_case)]
3131
#[prusti::spec_only]
3232
#[prusti::spec_id = "$(NUM_UUID)"]
3333
fn prusti_pledge_item_test1_$(NUM_UUID)(a: bool,
3434
result: ()) -> bool {
35-
!!((a): bool)
35+
let prusti_result: bool = a;
36+
prusti_result
3637
}
3738
#[prusti::assert_pledge_spec_id_ref_lhs = "$(NUM_UUID)"]
3839
#[prusti::assert_pledge_spec_id_ref_rhs = "$(NUM_UUID)"]
@@ -44,15 +45,17 @@ non_snake_case)]
4445
#[prusti::spec_id = "$(NUM_UUID)"]
4546
fn prusti_pledge_item_test2_$(NUM_UUID)(a: bool,
4647
result: ()) -> bool {
47-
!!((true): bool)
48+
let prusti_result: bool = true;
49+
prusti_result
4850
}
4951
#[allow(unused_must_use, unused_parens, unused_variables, dead_code,
5052
non_snake_case)]
5153
#[prusti::spec_only]
5254
#[prusti::spec_id = "$(NUM_UUID)"]
5355
fn prusti_pledge_item_test2_$(NUM_UUID)(a: bool,
5456
result: ()) -> bool {
55-
!!((a): bool)
57+
let prusti_result: bool = a;
58+
prusti_result
5659
}
5760
#[prusti::assert_pledge_spec_id_ref_lhs = "$(NUM_UUID)"]
5861
#[prusti::assert_pledge_spec_id_ref_rhs = "$(NUM_UUID)"]
@@ -64,15 +67,17 @@ non_snake_case)]
6467
#[prusti::spec_id = "$(NUM_UUID)"]
6568
fn prusti_pledge_item_test3_$(NUM_UUID)(x: u32,
6669
result: u32) -> bool {
67-
!!((true): bool)
70+
let prusti_result: bool = true;
71+
prusti_result
6872
}
6973
#[allow(unused_must_use, unused_parens, unused_variables, dead_code,
7074
non_snake_case)]
7175
#[prusti::spec_only]
7276
#[prusti::spec_id = "$(NUM_UUID)"]
7377
fn prusti_pledge_item_test3_$(NUM_UUID)(x: u32,
7478
result: u32) -> bool {
75-
!!((result == match x { 1 => 1, 2 => 2, _ => 0, }): bool)
79+
let prusti_result: bool = result == match x { 1 => 1, 2 => 2, _ => 0, };
80+
prusti_result
7681
}
7782
#[prusti::assert_pledge_spec_id_ref_lhs = "$(NUM_UUID)"]
7883
#[prusti::assert_pledge_spec_id_ref_rhs = "$(NUM_UUID)"]

0 commit comments

Comments
 (0)