diff --git a/prusti-interface/src/environment/loops.rs b/prusti-interface/src/environment/loops.rs index 1b3e214aee3..c7f34bde6a5 100644 --- 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 index c1dafc5a37b..2a04af2362c 100644 --- 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 index d941c81ba15..d4541662198 100644 --- 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 index e587bf8d92e..6c638fe1785 100644 --- 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 index dd95f8bd8ca..0ffdf3d80e0 100644 --- 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,7 +23,8 @@ 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)] @@ -32,7 +32,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::assert_pledge_spec_id_ref_lhs = "$(NUM_UUID)"] #[prusti::assert_pledge_spec_id_ref_rhs = "$(NUM_UUID)"] @@ -44,7 +45,8 @@ 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)] @@ -52,7 +54,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::assert_pledge_spec_id_ref_lhs = "$(NUM_UUID)"] #[prusti::assert_pledge_spec_id_ref_rhs = "$(NUM_UUID)"] @@ -64,7 +67,8 @@ 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)] @@ -72,7 +76,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::assert_pledge_spec_id_ref_lhs = "$(NUM_UUID)"] #[prusti::assert_pledge_spec_id_ref_rhs = "$(NUM_UUID)"] diff --git a/prusti-tests/tests/parse/ui/composite.stdout b/prusti-tests/tests/parse/ui/composite.stdout index e135aebb9b1..8c0238fa2cc 100644 --- a/prusti-tests/tests/parse/ui/composite.stdout +++ b/prusti-tests/tests/parse/ui/composite.stdout @@ -29,7 +29,6 @@ -#![feature(type_ascription)] #![feature(stmt_expr_attributes)] #![feature(register_tool)] #![register_tool(prusti)] @@ -43,7 +42,8 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test1_$(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)] @@ -53,8 +53,9 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test2_$(NUM_UUID)() -> bool { - !!(((((true) && ((!(true) || (true)))) && (((true) || (true)))) && - (true)): bool) + let prusti_result: bool = + (((true) && ((!(true) || (true)))) && (((true) || (true)))) && (true); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -64,7 +65,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)] @@ -74,7 +76,8 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test4_$(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)] @@ -84,8 +87,10 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test5_$(NUM_UUID)() -> bool { - !!((((!(true) || (true))) && - ((!(true) || ((true) && (((true) || (true))))))): bool) + let prusti_result: bool = + ((!(true) || (true))) && + ((!(true) || ((true) && (((true) || (true)))))); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -95,8 +100,10 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test6_$(NUM_UUID)() -> bool { - !!((!(((true) && (true))) || - (!(true) || (!(true) || (!(true) || (true))))): bool) + let prusti_result: bool = + !(((true) && (true))) || + (!(true) || (!(true) || (!(true) || (true)))); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -106,8 +113,10 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test7_$(NUM_UUID)() -> bool { - !!((!(((true) && (true))) || - (!(((true) && (true))) || (((true) && (true))))): bool) + let prusti_result: bool = + !(((true) && (true))) || + (!(((true) && (true))) || (((true) && (true)))); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -117,7 +126,8 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test8_$(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)] @@ -127,8 +137,10 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test9_$(NUM_UUID)() -> bool { - !!((!(((true) || (true))) || - (((true) || (((true) && (((true) || (true)))))))): bool) + let prusti_result: bool = + !(((true) || (true))) || + (((true) || (((true) && (((true) || (true))))))); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -138,10 +150,11 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test10_$(NUM_UUID)() -> bool { - !!(((true) && - (::prusti_contracts::forall((), - #[prusti::spec_only] |a: i32| -> bool - { ((a == 5): bool) }))): bool) + let prusti_result: bool = + (true) && + (::prusti_contracts::forall((), + #[prusti::spec_only] |a: i32| -> bool { a == 5 })); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -151,9 +164,10 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test12_$(NUM_UUID)() -> bool { - !!((::prusti_contracts::forall((), - #[prusti::spec_only] |a: i32| -> bool - { ((a == 5): bool) })): bool) + let prusti_result: bool = + ::prusti_contracts::forall((), + #[prusti::spec_only] |a: i32| -> bool { a == 5 }); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -163,10 +177,12 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test13_$(NUM_UUID)() -> bool { - !!((!(true) || - (!(::prusti_contracts::forall((), - #[prusti::spec_only] |a: i32, b: i32| -> bool - { ((a == 5): bool) })) || (true))): bool) + let prusti_result: bool = + !(true) || + (!(::prusti_contracts::forall((), + #[prusti::spec_only] |a: i32, b: i32| -> bool { a == 5 })) + || (true)); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -176,10 +192,11 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test14_$(NUM_UUID)() -> bool { - !!((!(true) || - (::prusti_contracts::forall((), - #[prusti::spec_only] |a: i32| -> bool - { ((a == 5): bool) }))): bool) + let prusti_result: bool = + !(true) || + (::prusti_contracts::forall((), + #[prusti::spec_only] |a: i32| -> bool { a == 5 })); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -189,9 +206,11 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test15_$(NUM_UUID)() -> bool { - !!((!(::prusti_contracts::forall((), - #[prusti::spec_only] |a: i32| -> bool { ((a == 5): bool) })) - || (true)): bool) + let prusti_result: bool = + !(::prusti_contracts::forall((), + #[prusti::spec_only] |a: i32| -> bool { a == 5 })) || + (true); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -201,13 +220,13 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test16_$(NUM_UUID)() -> bool { - !!((!(::prusti_contracts::forall((), - #[prusti::spec_only] |b: i32| -> bool - { ((b == 10): bool) })) || - (!(true) || - (::prusti_contracts::forall((), - #[prusti::spec_only] |a: u32, b: u32| -> bool - { ((a == 5): bool) })))): bool) + let prusti_result: bool = + !(::prusti_contracts::forall((), + #[prusti::spec_only] |b: i32| -> bool { b == 10 })) || + (!(true) || + (::prusti_contracts::forall((), + #[prusti::spec_only] |a: u32, b: u32| -> bool { a == 5 }))); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -217,10 +236,11 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test17_$(NUM_UUID)() -> bool { - !!(((true) && - (::prusti_contracts::exists((), - #[prusti::spec_only] |a: i32| -> bool - { ((a == 5): bool) }))): bool) + let prusti_result: bool = + (true) && + (::prusti_contracts::exists((), + #[prusti::spec_only] |a: i32| -> bool { a == 5 })); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -230,9 +250,10 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test19_$(NUM_UUID)() -> bool { - !!((::prusti_contracts::exists((), - #[prusti::spec_only] |a: i32| -> bool - { ((a == 5): bool) })): bool) + let prusti_result: bool = + ::prusti_contracts::exists((), + #[prusti::spec_only] |a: i32| -> bool { a == 5 }); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -242,10 +263,12 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test20_$(NUM_UUID)() -> bool { - !!((!(true) || - (!(::prusti_contracts::exists((), - #[prusti::spec_only] |a: i32, b: i32| -> bool - { ((a == 5): bool) })) || (true))): bool) + let prusti_result: bool = + !(true) || + (!(::prusti_contracts::exists((), + #[prusti::spec_only] |a: i32, b: i32| -> bool { a == 5 })) + || (true)); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -255,10 +278,11 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test21_$(NUM_UUID)() -> bool { - !!((!(true) || - (::prusti_contracts::exists((), - #[prusti::spec_only] |a: i32| -> bool - { ((a == 5): bool) }))): bool) + let prusti_result: bool = + !(true) || + (::prusti_contracts::exists((), + #[prusti::spec_only] |a: i32| -> bool { a == 5 })); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -268,9 +292,11 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test22_$(NUM_UUID)() -> bool { - !!((!(::prusti_contracts::exists((), - #[prusti::spec_only] |a: i32| -> bool { ((a == 5): bool) })) - || (true)): bool) + let prusti_result: bool = + !(::prusti_contracts::exists((), + #[prusti::spec_only] |a: i32| -> bool { a == 5 })) || + (true); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -280,13 +306,13 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test23_$(NUM_UUID)() -> bool { - !!((!(::prusti_contracts::exists((), - #[prusti::spec_only] |b: i32| -> bool - { ((b == 10): bool) })) || - (!(true) || - (::prusti_contracts::exists((), - #[prusti::spec_only] |a: u32, b: u32| -> bool - { ((a == 5): bool) })))): bool) + let prusti_result: bool = + !(::prusti_contracts::exists((), + #[prusti::spec_only] |b: i32| -> bool { b == 10 })) || + (!(true) || + (::prusti_contracts::exists((), + #[prusti::spec_only] |a: u32, b: u32| -> bool { a == 5 }))); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -296,7 +322,8 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test24_$(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)] @@ -306,12 +333,12 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test25_$(NUM_UUID)() -> bool { - !!(((::prusti_contracts::forall((), - #[prusti::spec_only] |a: i32| -> bool { ((a == 5): bool) })) - || - (::prusti_contracts::forall((), - #[prusti::spec_only] |a: i32| -> bool - { ((a == 5): bool) }))): bool) + let prusti_result: bool = + (::prusti_contracts::forall((), + #[prusti::spec_only] |a: i32| -> bool { a == 5 })) || + (::prusti_contracts::forall((), + #[prusti::spec_only] |a: i32| -> bool { a == 5 })); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -321,12 +348,12 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test26_$(NUM_UUID)() -> bool { - !!(((::prusti_contracts::exists((), - #[prusti::spec_only] |a: i32| -> bool { ((a == 5): bool) })) - || - (::prusti_contracts::exists((), - #[prusti::spec_only] |a: i32| -> bool - { ((a == 5): bool) }))): bool) + let prusti_result: bool = + (::prusti_contracts::exists((), + #[prusti::spec_only] |a: i32| -> bool { a == 5 })) || + (::prusti_contracts::exists((), + #[prusti::spec_only] |a: i32| -> bool { a == 5 })); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] diff --git a/prusti-tests/tests/parse/ui/empty.stdout b/prusti-tests/tests/parse/ui/empty.stdout index 4676c524737..77f14acdd73 100644 --- a/prusti-tests/tests/parse/ui/empty.stdout +++ b/prusti-tests/tests/parse/ui/empty.stdout @@ -1,6 +1,5 @@ // compile-flags: -Pprint_desugared_specs=true -Pno_verify=true -Phide_uuids=true -#![feature(type_ascription)] #![feature(stmt_expr_attributes)] #![feature(register_tool)] #![register_tool(prusti)] diff --git a/prusti-tests/tests/parse/ui/exists.stdout b/prusti-tests/tests/parse/ui/exists.stdout index a3a7150c4b5..be7b7034c8a 100644 --- a/prusti-tests/tests/parse/ui/exists.stdout +++ b/prusti-tests/tests/parse/ui/exists.stdout @@ -11,7 +11,6 @@ -#![feature(type_ascription)] #![feature(stmt_expr_attributes)] #![feature(register_tool)] #![register_tool(prusti)] @@ -25,9 +24,10 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test1_$(NUM_UUID)() -> bool { - !!((::prusti_contracts::exists((), - #[prusti::spec_only] |a: i32| -> bool - { (((a + a == a + a)): bool) })): bool) + let prusti_result: bool = + ::prusti_contracts::exists((), + #[prusti::spec_only] |a: i32| -> bool { (a + a == a + a) }); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -37,11 +37,11 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test2_$(NUM_UUID)() -> bool { - !!((::prusti_contracts::exists((), - #[prusti::spec_only] |a: i32, b: i32| -> bool - { - ((((a + b == a + b) && (true)) == (a + b == a + b)): bool) - })): bool) + let prusti_result: bool = + ::prusti_contracts::exists((), + #[prusti::spec_only] |a: i32, b: i32| -> bool + { ((a + b == a + b) && (true)) == (a + b == a + b) }); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -51,9 +51,11 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test3_$(NUM_UUID)() -> bool { - !!((::prusti_contracts::exists((), - #[prusti::spec_only] |a: i32, b: i32| -> bool - { ((!(a + b == a + b) || (a + b == a + b)): bool) })): bool) + let prusti_result: bool = + ::prusti_contracts::exists((), + #[prusti::spec_only] |a: i32, b: i32| -> bool + { !(a + b == a + b) || (a + b == a + b) }); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -63,10 +65,11 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test4_$(NUM_UUID)() -> bool { - !!((::prusti_contracts::exists(((#[prusti::spec_only] |a: i32| (1), - #[prusti::spec_only] |a: i32| ((2 == 2) && (true))),), - #[prusti::spec_only] |a: i32| -> bool - { ((a + a == a + a): bool) })): bool) + let prusti_result: bool = + ::prusti_contracts::exists(((#[prusti::spec_only] |a: i32| (1), + #[prusti::spec_only] |a: i32| ((2 == 2) && (true))),), + #[prusti::spec_only] |a: i32| -> bool { a + a == a + a }); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -76,11 +79,12 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test5_$(NUM_UUID)() -> bool { - !!((::prusti_contracts::exists(((#[prusti::spec_only] |a: i32, b: i32| - (1), #[prusti::spec_only] |a: i32, b: i32| (2)), - (#[prusti::spec_only] |a: i32, b: i32| (1),)), - #[prusti::spec_only] |a: i32, b: i32| -> bool - { ((a + b == a + b): bool) })): bool) + let prusti_result: bool = + ::prusti_contracts::exists(((#[prusti::spec_only] |a: i32, b: i32| + (1), #[prusti::spec_only] |a: i32, b: i32| (2)), + (#[prusti::spec_only] |a: i32, b: i32| (1),)), + #[prusti::spec_only] |a: i32, b: i32| -> bool { a + b == a + b }); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -90,14 +94,16 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test6_$(NUM_UUID)() -> bool { - !!((::prusti_contracts::exists(((#[prusti::spec_only] |a: i32, b: i32| - (1), #[prusti::spec_only] |a: i32, b: i32| (2), - #[prusti::spec_only] |a: i32, b: i32| (3)), - (#[prusti::spec_only] |a: i32, b: i32| (1), - #[prusti::spec_only] |a: i32, b: i32| (2)), - (#[prusti::spec_only] |a: i32, b: i32| (1),)), - #[prusti::spec_only] |a: i32, b: i32| -> bool - { ((!(a + b == a + b) || (a + b == a + b)): bool) })): bool) + let prusti_result: bool = + ::prusti_contracts::exists(((#[prusti::spec_only] |a: i32, b: i32| + (1), #[prusti::spec_only] |a: i32, b: i32| (2), + #[prusti::spec_only] |a: i32, b: i32| (3)), + (#[prusti::spec_only] |a: i32, b: i32| (1), + #[prusti::spec_only] |a: i32, b: i32| (2)), + (#[prusti::spec_only] |a: i32, b: i32| (1),)), + #[prusti::spec_only] |a: i32, b: i32| -> bool + { !(a + b == a + b) || (a + b == a + b) }); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] diff --git a/prusti-tests/tests/parse/ui/expression.stdout b/prusti-tests/tests/parse/ui/expression.stdout index a675007c16a..3737677aaa9 100644 --- a/prusti-tests/tests/parse/ui/expression.stdout +++ b/prusti-tests/tests/parse/ui/expression.stdout @@ -7,7 +7,6 @@ -#![feature(type_ascription)] #![feature(stmt_expr_attributes)] #![feature(register_tool)] #![register_tool(prusti)] @@ -21,7 +20,8 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test1_$(NUM_UUID)() -> bool { - !!(((1 == 1) && (1 != 2)): bool) + let prusti_result: bool = (1 == 1) && (1 != 2); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -32,7 +32,8 @@ non_snake_case)] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_post_item_test2_$(NUM_UUID)(result: ()) -> bool { - !!(((1 == 1) || (1 == 2)): bool) + let prusti_result: bool = (1 == 1) || (1 == 2); + prusti_result } #[prusti::post_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] diff --git a/prusti-tests/tests/parse/ui/forall.stdout b/prusti-tests/tests/parse/ui/forall.stdout index 96f3c59b5b1..b2b9a4f66e7 100644 --- a/prusti-tests/tests/parse/ui/forall.stdout +++ b/prusti-tests/tests/parse/ui/forall.stdout @@ -11,7 +11,6 @@ -#![feature(type_ascription)] #![feature(stmt_expr_attributes)] #![feature(register_tool)] #![register_tool(prusti)] @@ -25,9 +24,10 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test1_$(NUM_UUID)() -> bool { - !!((::prusti_contracts::forall((), - #[prusti::spec_only] |a: i32| -> bool - { (((a + a == a + a)): bool) })): bool) + let prusti_result: bool = + ::prusti_contracts::forall((), + #[prusti::spec_only] |a: i32| -> bool { (a + a == a + a) }); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -37,11 +37,11 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test2_$(NUM_UUID)() -> bool { - !!((::prusti_contracts::forall((), - #[prusti::spec_only] |a: i32, b: i32| -> bool - { - ((((a + b == a + b) && (true)) == (a + b == a + b)): bool) - })): bool) + let prusti_result: bool = + ::prusti_contracts::forall((), + #[prusti::spec_only] |a: i32, b: i32| -> bool + { ((a + b == a + b) && (true)) == (a + b == a + b) }); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -51,9 +51,11 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test3_$(NUM_UUID)() -> bool { - !!((::prusti_contracts::forall((), - #[prusti::spec_only] |a: i32, b: i32| -> bool - { ((!(a + b == a + b) || (a + b == a + b)): bool) })): bool) + let prusti_result: bool = + ::prusti_contracts::forall((), + #[prusti::spec_only] |a: i32, b: i32| -> bool + { !(a + b == a + b) || (a + b == a + b) }); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -63,10 +65,11 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test4_$(NUM_UUID)() -> bool { - !!((::prusti_contracts::forall(((#[prusti::spec_only] |a: i32| (1), - #[prusti::spec_only] |a: i32| ((2 == 2) && (true))),), - #[prusti::spec_only] |a: i32| -> bool - { ((a + a == a + a): bool) })): bool) + let prusti_result: bool = + ::prusti_contracts::forall(((#[prusti::spec_only] |a: i32| (1), + #[prusti::spec_only] |a: i32| ((2 == 2) && (true))),), + #[prusti::spec_only] |a: i32| -> bool { a + a == a + a }); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -76,11 +79,12 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test5_$(NUM_UUID)() -> bool { - !!((::prusti_contracts::forall(((#[prusti::spec_only] |a: i32, b: i32| - (1), #[prusti::spec_only] |a: i32, b: i32| (2)), - (#[prusti::spec_only] |a: i32, b: i32| (1),)), - #[prusti::spec_only] |a: i32, b: i32| -> bool - { ((a + b == a + b): bool) })): bool) + let prusti_result: bool = + ::prusti_contracts::forall(((#[prusti::spec_only] |a: i32, b: i32| + (1), #[prusti::spec_only] |a: i32, b: i32| (2)), + (#[prusti::spec_only] |a: i32, b: i32| (1),)), + #[prusti::spec_only] |a: i32, b: i32| -> bool { a + b == a + b }); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -90,14 +94,16 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test6_$(NUM_UUID)() -> bool { - !!((::prusti_contracts::forall(((#[prusti::spec_only] |a: i32, b: i32| - (1), #[prusti::spec_only] |a: i32, b: i32| (2), - #[prusti::spec_only] |a: i32, b: i32| (3)), - (#[prusti::spec_only] |a: i32, b: i32| (1), - #[prusti::spec_only] |a: i32, b: i32| (2)), - (#[prusti::spec_only] |a: i32, b: i32| (1),)), - #[prusti::spec_only] |a: i32, b: i32| -> bool - { ((!(a + b == a + b) || (a + b == a + b)): bool) })): bool) + let prusti_result: bool = + ::prusti_contracts::forall(((#[prusti::spec_only] |a: i32, b: i32| + (1), #[prusti::spec_only] |a: i32, b: i32| (2), + #[prusti::spec_only] |a: i32, b: i32| (3)), + (#[prusti::spec_only] |a: i32, b: i32| (1), + #[prusti::spec_only] |a: i32, b: i32| (2)), + (#[prusti::spec_only] |a: i32, b: i32| (1),)), + #[prusti::spec_only] |a: i32, b: i32| -> bool + { !(a + b == a + b) || (a + b == a + b) }); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] diff --git a/prusti-tests/tests/parse/ui/implies.stdout b/prusti-tests/tests/parse/ui/implies.stdout index 89bdf502e21..736afa8a39f 100644 --- a/prusti-tests/tests/parse/ui/implies.stdout +++ b/prusti-tests/tests/parse/ui/implies.stdout @@ -15,7 +15,6 @@ -#![feature(type_ascription)] #![feature(stmt_expr_attributes)] #![feature(register_tool)] #![register_tool(prusti)] @@ -29,7 +28,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)] @@ -39,7 +39,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)] @@ -49,7 +50,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)] @@ -59,7 +61,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)] @@ -69,7 +72,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)] @@ -79,7 +83,8 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test21_$(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)] @@ -89,7 +94,8 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test22_$(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)] @@ -99,7 +105,8 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test23_$(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)] @@ -109,7 +116,8 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test24_$(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)] @@ -119,7 +127,8 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test25_$(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/parenthesis.stderr b/prusti-tests/tests/parse/ui/parenthesis.stderr index a783c287344..54a1d67f983 100644 --- a/prusti-tests/tests/parse/ui/parenthesis.stderr +++ b/prusti-tests/tests/parse/ui/parenthesis.stderr @@ -2,7 +2,10 @@ error[E0308]: mismatched types --> $DIR/parenthesis.rs:8:15 | 8 | #[requires( ( 12345))] - | ^^^^^^^^^^^ expected `bool`, found integer + | ^^^^^^^^^^^ + | | + | expected `bool`, found integer + | expected due to this error[E0308]: mismatched types --> $DIR/parenthesis.rs:11:20 diff --git a/prusti-tests/tests/parse/ui/predicates-visibility.stdout b/prusti-tests/tests/parse/ui/predicates-visibility.stdout index 3ebd48713fd..f1a453b2e48 100644 --- a/prusti-tests/tests/parse/ui/predicates-visibility.stdout +++ b/prusti-tests/tests/parse/ui/predicates-visibility.stdout @@ -8,7 +8,6 @@ -#![feature(type_ascription)] #![feature(stmt_expr_attributes)] #![feature(register_tool)] #![register_tool(prusti)] @@ -26,17 +25,21 @@ mod foo { #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pred_item_pred1_$(NUM_UUID)(a: bool) -> bool { - (({ - ::prusti_contracts::forall((), - #[prusti::spec_only] |b: bool| -> bool { ((a == b): bool) }) - }): bool) + let prusti_result: bool = + { + ::prusti_contracts::forall((), + #[prusti::spec_only] |b: bool| -> bool { a == b }) + }; + prusti_result } #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::pred_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] pub fn pred1(a: bool) -> bool { - ::core::panicking::panic_fmt(format_args!("not implemented: {0}", - format_args!("predicate"))) + { + ::core::panicking::panic_fmt(format_args!("not implemented: {0}", + format_args!("predicate"))); + } } } #[allow(unused_must_use, unused_parens, unused_variables, dead_code, @@ -44,7 +47,8 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test_pub_pred_$(NUM_UUID)() -> bool { - !!((foo::pred1(true)): bool) + let prusti_result: bool = foo::pred1(true); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] diff --git a/prusti-tests/tests/parse/ui/predicates.stdout b/prusti-tests/tests/parse/ui/predicates.stdout index bd47d01ae3c..aea6d0a2371 100644 --- a/prusti-tests/tests/parse/ui/predicates.stdout +++ b/prusti-tests/tests/parse/ui/predicates.stdout @@ -12,7 +12,6 @@ -#![feature(type_ascription)] #![feature(stmt_expr_attributes)] #![feature(register_tool)] #![register_tool(prusti)] @@ -27,24 +26,29 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pred_item_pred1_$(NUM_UUID)(a: bool) -> bool { - (({ - ::prusti_contracts::forall((), - #[prusti::spec_only] |b: bool| -> bool { ((a == b): bool) }) - }): bool) + let prusti_result: bool = + { + ::prusti_contracts::forall((), + #[prusti::spec_only] |b: bool| -> bool { a == b }) + }; + prusti_result } #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::pred_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] fn pred1(a: bool) -> bool { - ::core::panicking::panic_fmt(format_args!("not implemented: {0}", - format_args!("predicate"))) + { + ::core::panicking::panic_fmt(format_args!("not implemented: {0}", + format_args!("predicate"))); + } } #[allow(unused_must_use, unused_parens, unused_variables, dead_code, non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_use_pred1_$(NUM_UUID)() -> bool { - !!((pred1(true)): bool) + let prusti_result: bool = pred1(true); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -54,24 +58,29 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pred_item_pred2_$(NUM_UUID)(a: bool) -> bool { - (({ - ::prusti_contracts::exists((), - #[prusti::spec_only] |b: bool| -> bool { ((a == b): bool) }) - }): bool) + let prusti_result: bool = + { + ::prusti_contracts::exists((), + #[prusti::spec_only] |b: bool| -> bool { a == b }) + }; + prusti_result } #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::pred_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] fn pred2(a: bool) -> bool { - ::core::panicking::panic_fmt(format_args!("not implemented: {0}", - format_args!("predicate"))) + { + ::core::panicking::panic_fmt(format_args!("not implemented: {0}", + format_args!("predicate"))); + } } #[allow(unused_must_use, unused_parens, unused_variables, dead_code, non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_use_pred2_$(NUM_UUID)() -> bool { - !!((pred2(true)): bool) + let prusti_result: bool = pred2(true); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -82,18 +91,22 @@ non_snake_case)] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pred_item_forall_implication_$(NUM_UUID)() -> bool { - (({ - ::prusti_contracts::forall((), - #[prusti::spec_only] |x: usize| -> bool - { ((!((x != 0)) || (x * 2 != 0)): bool) }) - }): bool) + let prusti_result: bool = + { + ::prusti_contracts::forall((), + #[prusti::spec_only] |x: usize| -> bool + { !((x != 0)) || (x * 2 != 0) }) + }; + prusti_result } #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::pred_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] fn forall_implication() -> bool { - ::core::panicking::panic_fmt(format_args!("not implemented: {0}", - format_args!("predicate"))) + { + ::core::panicking::panic_fmt(format_args!("not implemented: {0}", + format_args!("predicate"))); + } } #[allow(unused_must_use, unused_parens, unused_variables, dead_code, non_snake_case)] @@ -101,18 +114,22 @@ non_snake_case)] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pred_item_exists_implication_$(NUM_UUID)() -> bool { - (({ - ::prusti_contracts::exists((), - #[prusti::spec_only] |x: usize| -> bool - { ((!((x != 0)) || (x * 2 != 0)): bool) }) - }): bool) + let prusti_result: bool = + { + ::prusti_contracts::exists((), + #[prusti::spec_only] |x: usize| -> bool + { !((x != 0)) || (x * 2 != 0) }) + }; + prusti_result } #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::pred_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] fn exists_implication() -> bool { - ::core::panicking::panic_fmt(format_args!("not implemented: {0}", - format_args!("predicate"))) + { + ::core::panicking::panic_fmt(format_args!("not implemented: {0}", + format_args!("predicate"))); + } } fn main() {} ProcedureSpecification { source: DefId(0:7 ~ predicates[$(CRATE_ID)]::pred1), kind: Inherent(Predicate(Some(DefId(0:5 ~ predicates[$(CRATE_ID)]::prusti_pred_item_pred1_$(NUM_UUID))))), pres: Empty, posts: Empty, pledges: Empty, trusted: Inherent(false), terminates: Inherent(None), purity: Inherent(None) } diff --git a/prusti-tests/tests/parse/ui/simple_and.stderr b/prusti-tests/tests/parse/ui/simple_and.stderr index 43847c58c76..d68d12687ab 100644 --- a/prusti-tests/tests/parse/ui/simple_and.stderr +++ b/prusti-tests/tests/parse/ui/simple_and.stderr @@ -2,25 +2,37 @@ error[E0308]: mismatched types --> $DIR/simple_and.rs:5:12 | 5 | #[requires(12345)] - | ^^^^^ expected `bool`, found integer + | ^^^^^ + | | + | expected `bool`, found integer + | expected due to this error[E0308]: mismatched types --> $DIR/simple_and.rs:8:17 | 8 | #[requires (12345)] - | ^^^^^ expected `bool`, found integer + | ^^^^^ + | | + | expected `bool`, found integer + | expected due to this error[E0308]: mismatched types --> $DIR/simple_and.rs:17:5 | 17 | 12345) ] - | ^^^^^ expected `bool`, found integer + | ^^^^^ + | | + | expected `bool`, found integer + | expected due to this error[E0308]: mismatched types --> $DIR/simple_and.rs:22:5 | 22 | 12345) - | ^^^^^ expected `bool`, found integer + | ^^^^^ + | | + | expected `bool`, found integer + | expected due to this error[E0308]: mismatched types --> $DIR/simple_and.rs:26:20 diff --git a/prusti-tests/tests/parse/ui/trait-bounds.stdout b/prusti-tests/tests/parse/ui/trait-bounds.stdout index dffbf72abcd..2bd0f271c5b 100644 --- a/prusti-tests/tests/parse/ui/trait-bounds.stdout +++ b/prusti-tests/tests/parse/ui/trait-bounds.stdout @@ -8,7 +8,6 @@ -#![feature(type_ascription)] #![feature(stmt_expr_attributes)] #![feature(register_tool)] #![register_tool(prusti)] @@ -35,7 +34,8 @@ impl<'a, T: PartialEq, const L : usize> #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_post_item_bar_$(NUM_UUID)(_self: Foo<'a, T, L>, result: &'a [T; L]) -> bool { - !!((result == _self.0): bool) + let prusti_result: bool = result == _self.0; + prusti_result } #[prusti::extern_spec = "inherent_impl"] #[allow(unused, dead_code)] diff --git a/prusti-tests/tests/parse/ui/traits.stdout b/prusti-tests/tests/parse/ui/traits.stdout index 48b8cc30964..fb4a259b168 100644 --- a/prusti-tests/tests/parse/ui/traits.stdout +++ b/prusti-tests/tests/parse/ui/traits.stdout @@ -25,7 +25,6 @@ -#![feature(type_ascription)] #![feature(stmt_expr_attributes)] #![feature(register_tool)] #![register_tool(prusti)] @@ -40,7 +39,8 @@ trait Test1 { #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test1_$(NUM_UUID)() -> bool { - !!((true): bool) + let prusti_result: bool = true; + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -51,7 +51,8 @@ trait Test1 { #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_post_item_test2_$(NUM_UUID)(result: ()) -> bool { - !!((true): bool) + let prusti_result: bool = true; + prusti_result } #[prusti::post_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -61,7 +62,8 @@ trait Test1 { #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test3_$(NUM_UUID)() -> bool { - !!((true): bool) + let prusti_result: bool = true; + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -72,7 +74,8 @@ trait Test1 { #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_post_item_test4_$(NUM_UUID)(result: ()) -> bool { - !!((true): bool) + let prusti_result: bool = true; + prusti_result } #[prusti::post_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -84,7 +87,8 @@ trait Test2 { #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test1_$(NUM_UUID)() -> bool { - !!((true): bool) + let prusti_result: bool = true; + prusti_result } #[allow(unused_must_use, unused_parens, unused_variables, dead_code, non_snake_case)] @@ -92,7 +96,8 @@ trait Test2 { #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_post_item_test1_$(NUM_UUID)(result: ()) -> bool { - !!((true): bool) + let prusti_result: bool = true; + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::post_spec_id_ref = "$(NUM_UUID)"] @@ -103,7 +108,8 @@ trait Test2 { #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test2_$(NUM_UUID)() -> bool { - !!((true): bool) + let prusti_result: bool = true; + prusti_result } #[allow(unused_must_use, unused_parens, unused_variables, dead_code, non_snake_case)] @@ -111,7 +117,8 @@ trait Test2 { #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_post_item_test2_$(NUM_UUID)(result: ()) -> bool { - !!((true): bool) + let prusti_result: bool = true; + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::post_spec_id_ref = "$(NUM_UUID)"] @@ -124,7 +131,8 @@ trait Test3 { #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test1_$(NUM_UUID)(&self) -> bool { - !!((true): bool) + let prusti_result: bool = true; + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -135,7 +143,8 @@ trait Test3 { #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_post_item_test2_$(NUM_UUID)(&self, result: ()) -> bool { - !!((true): bool) + let prusti_result: bool = true; + prusti_result } #[prusti::post_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -145,7 +154,8 @@ trait Test3 { #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test3_$(NUM_UUID)(&self) -> bool { - !!((true): bool) + let prusti_result: bool = true; + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -156,7 +166,8 @@ trait Test3 { #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_post_item_test4_$(NUM_UUID)(&self, result: ()) -> bool { - !!((true): bool) + let prusti_result: bool = true; + prusti_result } #[prusti::post_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -168,7 +179,8 @@ trait Test4 { #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test1_$(NUM_UUID)(&self) -> bool { - !!((true): bool) + let prusti_result: bool = true; + prusti_result } #[allow(unused_must_use, unused_parens, unused_variables, dead_code, non_snake_case)] @@ -176,7 +188,8 @@ trait Test4 { #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_post_item_test1_$(NUM_UUID)(&self, result: ()) -> bool { - !!((true): bool) + let prusti_result: bool = true; + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::post_spec_id_ref = "$(NUM_UUID)"] @@ -187,7 +200,8 @@ trait Test4 { #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test2_$(NUM_UUID)(&self) -> bool { - !!((true): bool) + let prusti_result: bool = true; + prusti_result } #[allow(unused_must_use, unused_parens, unused_variables, dead_code, non_snake_case)] @@ -195,7 +209,8 @@ trait Test4 { #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_post_item_test2_$(NUM_UUID)(&self, result: ()) -> bool { - !!((true): bool) + let prusti_result: bool = true; + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::post_spec_id_ref = "$(NUM_UUID)"] diff --git a/prusti-tests/tests/parse/ui/true.stdout b/prusti-tests/tests/parse/ui/true.stdout index 38d8e2be6c2..21f2c83de9a 100644 --- a/prusti-tests/tests/parse/ui/true.stdout +++ b/prusti-tests/tests/parse/ui/true.stdout @@ -9,7 +9,6 @@ -#![feature(type_ascription)] #![feature(stmt_expr_attributes)] #![feature(register_tool)] #![register_tool(prusti)] @@ -23,7 +22,8 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test1_$(NUM_UUID)() -> bool { - !!((true): bool) + let prusti_result: bool = true; + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -34,7 +34,8 @@ non_snake_case)] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_post_item_test2_$(NUM_UUID)(result: ()) -> bool { - !!((true): bool) + let prusti_result: bool = true; + prusti_result } #[prusti::post_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -61,7 +62,8 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test4_$(NUM_UUID)() -> bool { - !!((true): bool) + let prusti_result: bool = true; + prusti_result } #[allow(unused_must_use, unused_parens, unused_variables, dead_code, non_snake_case)] @@ -69,7 +71,8 @@ non_snake_case)] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_post_item_test4_$(NUM_UUID)(result: ()) -> bool { - !!((true): bool) + let prusti_result: bool = true; + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::post_spec_id_ref = "$(NUM_UUID)"] diff --git a/prusti-tests/tests/parse/ui/trusted.stdout b/prusti-tests/tests/parse/ui/trusted.stdout index ee4abe3abf6..c50084f549e 100644 --- a/prusti-tests/tests/parse/ui/trusted.stdout +++ b/prusti-tests/tests/parse/ui/trusted.stdout @@ -7,7 +7,6 @@ -#![feature(type_ascription)] #![feature(stmt_expr_attributes)] #![feature(register_tool)] #![register_tool(prusti)] diff --git a/prusti-tests/tests/typecheck/ui/forall_encode_typeck.stdout b/prusti-tests/tests/typecheck/ui/forall_encode_typeck.stdout index 9c1730f139e..dfcfc0f4f02 100644 --- a/prusti-tests/tests/typecheck/ui/forall_encode_typeck.stdout +++ b/prusti-tests/tests/typecheck/ui/forall_encode_typeck.stdout @@ -7,7 +7,6 @@ -#![feature(type_ascription)] #![feature(stmt_expr_attributes)] #![feature(register_tool)] #![register_tool(prusti)] @@ -21,11 +20,12 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test1_$(NUM_UUID)() -> bool { - !!((::prusti_contracts::forall(((#[prusti::spec_only] |a: i32, b: u32| - (a == a), #[prusti::spec_only] |a: i32, b: u32| (a == a)), - (#[prusti::spec_only] |a: i32, b: u32| (true),)), - #[prusti::spec_only] |a: i32, b: u32| -> bool - { ((a == a): bool) })): bool) + let prusti_result: bool = + ::prusti_contracts::forall(((#[prusti::spec_only] |a: i32, b: u32| + (a == a), #[prusti::spec_only] |a: i32, b: u32| (a == a)), + (#[prusti::spec_only] |a: i32, b: u32| (true),)), + #[prusti::spec_only] |a: i32, b: u32| -> bool { a == a }); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -35,11 +35,12 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test2_$(NUM_UUID)() -> bool { - !!((::prusti_contracts::exists(((#[prusti::spec_only] |a: i32, b: u32| - (a == a), #[prusti::spec_only] |a: i32, b: u32| (a == a)), - (#[prusti::spec_only] |a: i32, b: u32| (true),)), - #[prusti::spec_only] |a: i32, b: u32| -> bool - { ((a == a): bool) })): bool) + let prusti_result: bool = + ::prusti_contracts::exists(((#[prusti::spec_only] |a: i32, b: u32| + (a == a), #[prusti::spec_only] |a: i32, b: u32| (a == a)), + (#[prusti::spec_only] |a: i32, b: u32| (true),)), + #[prusti::spec_only] |a: i32, b: u32| -> bool { a == a }); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] diff --git a/prusti-tests/tests/typecheck/ui/forall_triggers.stdout b/prusti-tests/tests/typecheck/ui/forall_triggers.stdout index e24630b4595..ac6ac3c3288 100644 --- a/prusti-tests/tests/typecheck/ui/forall_triggers.stdout +++ b/prusti-tests/tests/typecheck/ui/forall_triggers.stdout @@ -13,7 +13,6 @@ -#![feature(type_ascription)] #![feature(stmt_expr_attributes)] #![feature(register_tool)] #![register_tool(prusti)] @@ -27,10 +26,11 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test1_$(NUM_UUID)() -> bool { - !!((::prusti_contracts::forall(((#[prusti::spec_only] |a: i32| - (a == a),),), - #[prusti::spec_only] |a: i32| -> bool { ((true): bool) })): - bool) + let prusti_result: bool = + ::prusti_contracts::forall(((#[prusti::spec_only] |a: i32| + (a == a),),), + #[prusti::spec_only] |a: i32| -> bool { true }); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -40,14 +40,15 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test2_$(NUM_UUID)() -> bool { - !!((::prusti_contracts::forall(((#[prusti::spec_only] |a: i32| - ((a == a) && (true)),),), - #[prusti::spec_only] |a: i32| -> bool - { - ((::prusti_contracts::forall((), - #[prusti::spec_only] |b: i32| -> bool { ((true): bool) })): - bool) - })): bool) + let prusti_result: bool = + ::prusti_contracts::forall(((#[prusti::spec_only] |a: i32| + ((a == a) && (true)),),), + #[prusti::spec_only] |a: i32| -> bool + { + ::prusti_contracts::forall((), + #[prusti::spec_only] |b: i32| -> bool { true }) + }); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -57,15 +58,16 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test3_$(NUM_UUID)() -> bool { - !!((::prusti_contracts::forall(((#[prusti::spec_only] |a: i32| - (a == a),),), - #[prusti::spec_only] |a: i32| -> bool - { - ((::prusti_contracts::forall(((#[prusti::spec_only] |b: i32| - (a == a),),), - #[prusti::spec_only] |b: i32| -> bool { ((true): bool) })): - bool) - })): bool) + let prusti_result: bool = + ::prusti_contracts::forall(((#[prusti::spec_only] |a: i32| + (a == a),),), + #[prusti::spec_only] |a: i32| -> bool + { + ::prusti_contracts::forall(((#[prusti::spec_only] |b: i32| + (a == a),),), + #[prusti::spec_only] |b: i32| -> bool { true }) + }); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -75,15 +77,16 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test4_$(NUM_UUID)() -> bool { - !!((::prusti_contracts::forall(((#[prusti::spec_only] |a: i32| - ((a == a) && (true)),),), - #[prusti::spec_only] |a: i32| -> bool - { - ((::prusti_contracts::forall(((#[prusti::spec_only] |b: i32| - (a == b),),), - #[prusti::spec_only] |b: i32| -> bool { ((true): bool) })): - bool) - })): bool) + let prusti_result: bool = + ::prusti_contracts::forall(((#[prusti::spec_only] |a: i32| + ((a == a) && (true)),),), + #[prusti::spec_only] |a: i32| -> bool + { + ::prusti_contracts::forall(((#[prusti::spec_only] |b: i32| + (a == b),),), + #[prusti::spec_only] |b: i32| -> bool { true }) + }); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -93,10 +96,11 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test5_$(NUM_UUID)() -> bool { - !!((::prusti_contracts::exists(((#[prusti::spec_only] |a: i32| - (a == a),),), - #[prusti::spec_only] |a: i32| -> bool { ((true): bool) })): - bool) + let prusti_result: bool = + ::prusti_contracts::exists(((#[prusti::spec_only] |a: i32| + (a == a),),), + #[prusti::spec_only] |a: i32| -> bool { true }); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -106,14 +110,15 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test6_$(NUM_UUID)() -> bool { - !!((::prusti_contracts::exists(((#[prusti::spec_only] |a: i32| - ((a == a) && (true)),),), - #[prusti::spec_only] |a: i32| -> bool - { - ((::prusti_contracts::exists((), - #[prusti::spec_only] |b: i32| -> bool { ((true): bool) })): - bool) - })): bool) + let prusti_result: bool = + ::prusti_contracts::exists(((#[prusti::spec_only] |a: i32| + ((a == a) && (true)),),), + #[prusti::spec_only] |a: i32| -> bool + { + ::prusti_contracts::exists((), + #[prusti::spec_only] |b: i32| -> bool { true }) + }); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -123,15 +128,16 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test7_$(NUM_UUID)() -> bool { - !!((::prusti_contracts::exists(((#[prusti::spec_only] |a: i32| - (a == a),),), - #[prusti::spec_only] |a: i32| -> bool - { - ((::prusti_contracts::exists(((#[prusti::spec_only] |b: i32| - (a == a),),), - #[prusti::spec_only] |b: i32| -> bool { ((true): bool) })): - bool) - })): bool) + let prusti_result: bool = + ::prusti_contracts::exists(((#[prusti::spec_only] |a: i32| + (a == a),),), + #[prusti::spec_only] |a: i32| -> bool + { + ::prusti_contracts::exists(((#[prusti::spec_only] |b: i32| + (a == a),),), + #[prusti::spec_only] |b: i32| -> bool { true }) + }); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -141,15 +147,16 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test8_$(NUM_UUID)() -> bool { - !!((::prusti_contracts::exists(((#[prusti::spec_only] |a: i32| - ((a == a) && (true)),),), - #[prusti::spec_only] |a: i32| -> bool - { - ((::prusti_contracts::exists(((#[prusti::spec_only] |b: i32| - (a == b),),), - #[prusti::spec_only] |b: i32| -> bool { ((true): bool) })): - bool) - })): bool) + let prusti_result: bool = + ::prusti_contracts::exists(((#[prusti::spec_only] |a: i32| + ((a == a) && (true)),),), + #[prusti::spec_only] |a: i32| -> bool + { + ::prusti_contracts::exists(((#[prusti::spec_only] |b: i32| + (a == b),),), + #[prusti::spec_only] |b: i32| -> bool { true }) + }); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] diff --git a/prusti-tests/tests/typecheck/ui/nested_forall.stdout b/prusti-tests/tests/typecheck/ui/nested_forall.stdout index 54d10eb6239..4f9fc90254e 100644 --- a/prusti-tests/tests/typecheck/ui/nested_forall.stdout +++ b/prusti-tests/tests/typecheck/ui/nested_forall.stdout @@ -12,7 +12,6 @@ -#![feature(type_ascription)] #![feature(stmt_expr_attributes)] #![feature(register_tool)] #![register_tool(prusti)] @@ -26,13 +25,14 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test1_$(NUM_UUID)() -> bool { - !!((::prusti_contracts::forall((), - #[prusti::spec_only] |a: i32| -> bool - { - ((::prusti_contracts::forall((), - #[prusti::spec_only] |a: i32| -> bool - { ((a == a): bool) })): bool) - })): bool) + let prusti_result: bool = + ::prusti_contracts::forall((), + #[prusti::spec_only] |a: i32| -> bool + { + ::prusti_contracts::forall((), + #[prusti::spec_only] |a: i32| -> bool { a == a }) + }); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -42,13 +42,15 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test2_$(NUM_UUID)() -> bool { - !!((::prusti_contracts::forall((), - #[prusti::spec_only] |a: i32| -> bool - { - ((::prusti_contracts::forall((), - #[prusti::spec_only] |b: i32| -> bool - { ((!(a == a) || (b == b)): bool) })): bool) - })): bool) + let prusti_result: bool = + ::prusti_contracts::forall((), + #[prusti::spec_only] |a: i32| -> bool + { + ::prusti_contracts::forall((), + #[prusti::spec_only] |b: i32| -> bool + { !(a == a) || (b == b) }) + }); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -58,17 +60,19 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test3_$(NUM_UUID)() -> bool { - !!((::prusti_contracts::forall((), - #[prusti::spec_only] |a: i32| -> bool - { - ((::prusti_contracts::forall((), - #[prusti::spec_only] |b: i32| -> bool - { - ((::prusti_contracts::forall((), - #[prusti::spec_only] |c: i32| -> bool - { (((a == a) && (b == b)): bool) })): bool) - })): bool) - })): bool) + let prusti_result: bool = + ::prusti_contracts::forall((), + #[prusti::spec_only] |a: i32| -> bool + { + ::prusti_contracts::forall((), + #[prusti::spec_only] |b: i32| -> bool + { + ::prusti_contracts::forall((), + #[prusti::spec_only] |c: i32| -> bool + { (a == a) && (b == b) }) + }) + }); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -78,13 +82,14 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test4_$(NUM_UUID)() -> bool { - !!((::prusti_contracts::exists((), - #[prusti::spec_only] |a: i32| -> bool - { - ((::prusti_contracts::exists((), - #[prusti::spec_only] |a: i32| -> bool - { ((a == a): bool) })): bool) - })): bool) + let prusti_result: bool = + ::prusti_contracts::exists((), + #[prusti::spec_only] |a: i32| -> bool + { + ::prusti_contracts::exists((), + #[prusti::spec_only] |a: i32| -> bool { a == a }) + }); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -94,13 +99,15 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test5_$(NUM_UUID)() -> bool { - !!((::prusti_contracts::exists((), - #[prusti::spec_only] |a: i32| -> bool - { - ((::prusti_contracts::exists((), - #[prusti::spec_only] |b: i32| -> bool - { ((!(a == a) || (b == b)): bool) })): bool) - })): bool) + let prusti_result: bool = + ::prusti_contracts::exists((), + #[prusti::spec_only] |a: i32| -> bool + { + ::prusti_contracts::exists((), + #[prusti::spec_only] |b: i32| -> bool + { !(a == a) || (b == b) }) + }); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -110,17 +117,19 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test6_$(NUM_UUID)() -> bool { - !!((::prusti_contracts::exists((), - #[prusti::spec_only] |a: i32| -> bool - { - ((::prusti_contracts::exists((), - #[prusti::spec_only] |b: i32| -> bool - { - ((::prusti_contracts::exists((), - #[prusti::spec_only] |c: i32| -> bool - { (((a == a) && (b == b)): bool) })): bool) - })): bool) - })): bool) + let prusti_result: bool = + ::prusti_contracts::exists((), + #[prusti::spec_only] |a: i32| -> bool + { + ::prusti_contracts::exists((), + #[prusti::spec_only] |b: i32| -> bool + { + ::prusti_contracts::exists((), + #[prusti::spec_only] |c: i32| -> bool + { (a == a) && (b == b) }) + }) + }); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] diff --git a/prusti-tests/tests/verify/ui/calls.stdout b/prusti-tests/tests/verify/ui/calls.stdout index 6b3c7be3f31..7b51abd5015 100644 --- a/prusti-tests/tests/verify/ui/calls.stdout +++ b/prusti-tests/tests/verify/ui/calls.stdout @@ -15,7 +15,6 @@ -#![feature(type_ascription)] #![feature(stmt_expr_attributes)] #![feature(register_tool)] #![register_tool(prusti)] @@ -30,7 +29,8 @@ non_snake_case)] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_post_item_max_$(NUM_UUID)(a: i32, b: i32, result: i32) -> bool { - !!(((result == a) || (result == b)): bool) + let prusti_result: bool = (result == a) || (result == b); + prusti_result } #[allow(unused_must_use, unused_parens, unused_variables, dead_code, non_snake_case)] @@ -38,7 +38,8 @@ non_snake_case)] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_post_item_max_$(NUM_UUID)(a: i32, b: i32, result: i32) -> bool { - !!(((result >= a) && (result >= b)): bool) + let prusti_result: bool = (result >= a) && (result >= b); + prusti_result } #[prusti::post_spec_id_ref = "$(NUM_UUID)"] #[prusti::post_spec_id_ref = "$(NUM_UUID)"] @@ -62,8 +63,9 @@ non_snake_case)] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_post_item_test_max3_$(NUM_UUID)(result: i32) -> bool { - !!((((true) && ((!(true) || (result == 3)))) && (((true) || (false)))): - bool) + let prusti_result: bool = + ((true) && ((!(true) || (result == 3)))) && (((true) || (false))); + prusti_result } #[prusti::post_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] diff --git a/prusti-tests/tests/verify/ui/collect.stdout b/prusti-tests/tests/verify/ui/collect.stdout index 2a3e4baddac..ead43b41e13 100644 --- a/prusti-tests/tests/verify/ui/collect.stdout +++ b/prusti-tests/tests/verify/ui/collect.stdout @@ -9,7 +9,6 @@ -#![feature(type_ascription)] #![feature(stmt_expr_attributes)] #![feature(register_tool)] #![register_tool(prusti)] @@ -23,7 +22,8 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test1_$(NUM_UUID)() -> bool { - !!((true): bool) + let prusti_result: bool = true; + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -34,7 +34,8 @@ non_snake_case)] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_post_item_test2_$(NUM_UUID)(result: ()) -> bool { - !!((true): bool) + let prusti_result: bool = true; + prusti_result } #[prusti::post_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -63,7 +64,8 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test4_$(NUM_UUID)() -> bool { - !!((true): bool) + let prusti_result: bool = true; + prusti_result } #[allow(unused_must_use, unused_parens, unused_variables, dead_code, non_snake_case)] @@ -71,7 +73,8 @@ non_snake_case)] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_post_item_test4_$(NUM_UUID)(result: ()) -> bool { - !!((true): bool) + let prusti_result: bool = true; + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::post_spec_id_ref = "$(NUM_UUID)"] diff --git a/prusti-tests/tests/verify/ui/false.stdout b/prusti-tests/tests/verify/ui/false.stdout index 85324948ecc..4fb5c13e414 100644 --- a/prusti-tests/tests/verify/ui/false.stdout +++ b/prusti-tests/tests/verify/ui/false.stdout @@ -7,7 +7,6 @@ -#![feature(type_ascription)] #![feature(stmt_expr_attributes)] #![feature(register_tool)] #![register_tool(prusti)] @@ -22,7 +21,8 @@ non_snake_case)] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_post_item_test1_$(NUM_UUID)(result: ()) -> bool { - !!((false): bool) + let prusti_result: bool = false; + prusti_result } #[prusti::post_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] diff --git a/prusti-tests/tests/verify/ui/forall_verify.stdout b/prusti-tests/tests/verify/ui/forall_verify.stdout index 29f01018e3e..917f179fcd2 100644 --- a/prusti-tests/tests/verify/ui/forall_verify.stdout +++ b/prusti-tests/tests/verify/ui/forall_verify.stdout @@ -16,7 +16,6 @@ // have checked the emitted Viper code (including the positions) and // could not see any relevant differences. -#![feature(type_ascription)] #![feature(stmt_expr_attributes)] #![feature(register_tool)] #![register_tool(prusti)] @@ -34,9 +33,10 @@ non_snake_case)] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_post_item_test1_$(NUM_UUID)(result: ()) -> bool { - !!((::prusti_contracts::forall((), - #[prusti::spec_only] |x: i32| -> bool { ((true): bool) })): - bool) + let prusti_result: bool = + ::prusti_contracts::forall((), + #[prusti::spec_only] |x: i32| -> bool { true }); + prusti_result } #[prusti::post_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -47,9 +47,10 @@ non_snake_case)] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_post_item_test2_$(NUM_UUID)(result: ()) -> bool { - !!((::prusti_contracts::forall((), - #[prusti::spec_only] |x: i32| -> bool - { ((identity(x) == x): bool) })): bool) + let prusti_result: bool = + ::prusti_contracts::forall((), + #[prusti::spec_only] |x: i32| -> bool { identity(x) == x }); + prusti_result } #[prusti::post_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -60,9 +61,10 @@ non_snake_case)] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_post_item_test3_$(NUM_UUID)(result: ()) -> bool { - !!((::prusti_contracts::forall((), - #[prusti::spec_only] |x: i32| -> bool - { ((identity(x) == x + 1): bool) })): bool) + let prusti_result: bool = + ::prusti_contracts::forall((), + #[prusti::spec_only] |x: i32| -> bool { identity(x) == x + 1 }); + prusti_result } #[prusti::post_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -73,9 +75,10 @@ non_snake_case)] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_post_item_test4_$(NUM_UUID)(result: ()) -> bool { - !!((::prusti_contracts::exists((), - #[prusti::spec_only] |x: i32| -> bool { ((true): bool) })): - bool) + let prusti_result: bool = + ::prusti_contracts::exists((), + #[prusti::spec_only] |x: i32| -> bool { true }); + prusti_result } #[prusti::post_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -86,7 +89,8 @@ non_snake_case)] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_post_item_test5_$(NUM_UUID)(result: ()) -> bool { - !!((identity(1) == 1): bool) + let prusti_result: bool = identity(1) == 1; + prusti_result } #[allow(unused_must_use, unused_parens, unused_variables, dead_code, non_snake_case)] @@ -94,9 +98,10 @@ non_snake_case)] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_post_item_test5_$(NUM_UUID)(result: ()) -> bool { - !!((::prusti_contracts::exists((), - #[prusti::spec_only] |x: i32| -> bool - { ((identity(x) == x): bool) })): bool) + let prusti_result: bool = + ::prusti_contracts::exists((), + #[prusti::spec_only] |x: i32| -> bool { identity(x) == x }); + prusti_result } #[prusti::post_spec_id_ref = "$(NUM_UUID)"] #[prusti::post_spec_id_ref = "$(NUM_UUID)"] @@ -108,9 +113,10 @@ non_snake_case)] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_post_item_test6_$(NUM_UUID)(result: ()) -> bool { - !!((::prusti_contracts::exists((), - #[prusti::spec_only] |x: i32| -> bool - { ((identity(x) == x + 1): bool) })): bool) + let prusti_result: bool = + ::prusti_contracts::exists((), + #[prusti::spec_only] |x: i32| -> bool { identity(x) == x + 1 }); + prusti_result } #[prusti::post_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] diff --git a/prusti-tests/tests/verify/ui/pledges.stdout b/prusti-tests/tests/verify/ui/pledges.stdout index b8567ce292a..2bf20a2ccb7 100644 --- a/prusti-tests/tests/verify/ui/pledges.stdout +++ b/prusti-tests/tests/verify/ui/pledges.stdout @@ -11,7 +11,6 @@ -#![feature(type_ascription)] #![feature(stmt_expr_attributes)] #![feature(register_tool)] #![register_tool(prusti)] @@ -52,7 +51,8 @@ non_snake_case)] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pledge_item_reborrow_$(NUM_UUID)<'a>(x: &'a mut T, result: &'a mut u32) -> bool { - !!((before_expiry(*result) == x.f): bool) + let prusti_result: bool = before_expiry(*result) == x.f; + prusti_result } #[prusti::pledge_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] diff --git a/prusti-tests/tests/verify/ui/predicate.stdout b/prusti-tests/tests/verify/ui/predicate.stdout index 36ab9225986..1164fc9e071 100644 --- a/prusti-tests/tests/verify/ui/predicate.stdout +++ b/prusti-tests/tests/verify/ui/predicate.stdout @@ -18,7 +18,6 @@ // somewhere down the call stack is false // Provide an existential witness. -#![feature(type_ascription)] #![feature(stmt_expr_attributes)] #![feature(register_tool)] #![register_tool(prusti)] @@ -35,34 +34,42 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pred_item_true_p1_$(NUM_UUID)() -> bool { - (({ - ::prusti_contracts::forall((), - #[prusti::spec_only] |x: i32| -> bool { ((true): bool) }) - }): bool) + let prusti_result: bool = + { + ::prusti_contracts::forall((), + #[prusti::spec_only] |x: i32| -> bool { true }) + }; + prusti_result } #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::pred_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] fn true_p1() -> bool { - ::core::panicking::panic_fmt(format_args!("not implemented: {0}", - format_args!("predicate"))) + { + ::core::panicking::panic_fmt(format_args!("not implemented: {0}", + format_args!("predicate"))); + } } #[allow(unused_must_use, unused_parens, unused_variables, dead_code, non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pred_item_true_p2_$(NUM_UUID)() -> bool { - (({ - ::prusti_contracts::exists((), - #[prusti::spec_only] |x: i32| -> bool { ((true): bool) }) - }): bool) + let prusti_result: bool = + { + ::prusti_contracts::exists((), + #[prusti::spec_only] |x: i32| -> bool { true }) + }; + prusti_result } #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::pred_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] fn true_p2() -> bool { - ::core::panicking::panic_fmt(format_args!("not implemented: {0}", - format_args!("predicate"))) + { + ::core::panicking::panic_fmt(format_args!("not implemented: {0}", + format_args!("predicate"))); + } } #[allow(unused_must_use, unused_parens, unused_variables, dead_code, non_snake_case)] @@ -70,18 +77,21 @@ non_snake_case)] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pred_item_forall_identity_$(NUM_UUID)() -> bool { - (({ - ::prusti_contracts::forall((), - #[prusti::spec_only] |x: i32| -> bool - { ((identity(x) == x): bool) }) - }): bool) + let prusti_result: bool = + { + ::prusti_contracts::forall((), + #[prusti::spec_only] |x: i32| -> bool { identity(x) == x }) + }; + prusti_result } #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::pred_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] fn forall_identity() -> bool { - ::core::panicking::panic_fmt(format_args!("not implemented: {0}", - format_args!("predicate"))) + { + ::core::panicking::panic_fmt(format_args!("not implemented: {0}", + format_args!("predicate"))); + } } #[allow(unused_must_use, unused_parens, unused_variables, dead_code, non_snake_case)] @@ -89,19 +99,22 @@ non_snake_case)] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pred_item_exists_identity_$(NUM_UUID)() -> bool { - (({ - ::prusti_contracts::exists(((#[prusti::spec_only] |x: i32| - (identity(x)),),), - #[prusti::spec_only] |x: i32| -> bool - { ((identity(x) == x): bool) }) - }): bool) + let prusti_result: bool = + { + ::prusti_contracts::exists(((#[prusti::spec_only] |x: i32| + (identity(x)),),), + #[prusti::spec_only] |x: i32| -> bool { identity(x) == x }) + }; + prusti_result } #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::pred_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] fn exists_identity() -> bool { - ::core::panicking::panic_fmt(format_args!("not implemented: {0}", - format_args!("predicate"))) + { + ::core::panicking::panic_fmt(format_args!("not implemented: {0}", + format_args!("predicate"))); + } } #[allow(unused_must_use, unused_parens, unused_variables, dead_code, non_snake_case)] @@ -109,7 +122,8 @@ non_snake_case)] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test_identity_1_$(NUM_UUID)() -> bool { - !!((true_p1()): bool) + let prusti_result: bool = true_p1(); + prusti_result } #[allow(unused_must_use, unused_parens, unused_variables, dead_code, non_snake_case)] @@ -117,7 +131,8 @@ non_snake_case)] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test_identity_1_$(NUM_UUID)() -> bool { - !!((forall_identity()): bool) + let prusti_result: bool = forall_identity(); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] @@ -129,7 +144,8 @@ non_snake_case)] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test_identity_2_$(NUM_UUID)() -> bool { - !!((true_p2()): bool) + let prusti_result: bool = true_p2(); + prusti_result } #[allow(unused_must_use, unused_parens, unused_variables, dead_code, non_snake_case)] @@ -137,7 +153,8 @@ non_snake_case)] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test_identity_2_$(NUM_UUID)() -> bool { - !!((exists_identity()): bool) + let prusti_result: bool = exists_identity(); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] @@ -148,14 +165,17 @@ non_snake_case)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pred_item_false_p_$(NUM_UUID)() -> bool { - (({ false }): bool) + let prusti_result: bool = { false }; + prusti_result } #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::pred_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] fn false_p() -> bool { - ::core::panicking::panic_fmt(format_args!("not implemented: {0}", - format_args!("predicate"))) + { + ::core::panicking::panic_fmt(format_args!("not implemented: {0}", + format_args!("predicate"))); + } } #[allow(unused_must_use, unused_parens, unused_variables, dead_code, non_snake_case)] @@ -163,7 +183,8 @@ non_snake_case)] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_precond_or_correctly_$(NUM_UUID)() -> bool { - !!(((false_p()) || (true)): bool) + let prusti_result: bool = (false_p()) || (true); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] diff --git a/prusti-tests/tests/verify/ui/pure.stdout b/prusti-tests/tests/verify/ui/pure.stdout index 9a3c5be52ce..ed73cc72f2f 100644 --- a/prusti-tests/tests/verify/ui/pure.stdout +++ b/prusti-tests/tests/verify/ui/pure.stdout @@ -20,7 +20,6 @@ -#![feature(type_ascription)] #![feature(stmt_expr_attributes)] #![feature(register_tool)] #![register_tool(prusti)] @@ -43,7 +42,8 @@ non_snake_case)] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_post_item_test_identity2_$(NUM_UUID)(result: ()) -> bool { - !!((6 == identity(6)): bool) + let prusti_result: bool = 6 == identity(6); + prusti_result } #[prusti::post_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -69,8 +69,9 @@ non_snake_case)] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_post_item_test_max3_$(NUM_UUID)(result: i32) -> bool { - !!((((true) && ((!(true) || (result == 3)))) && (((true) || (false)))): - bool) + let prusti_result: bool = + ((true) && ((!(true) || (result == 3)))) && (((true) || (false))); + prusti_result } #[prusti::post_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] @@ -81,7 +82,8 @@ non_snake_case)] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test_max4_$(NUM_UUID)(a: i32, b: i32) -> bool { - !!((a > b): bool) + let prusti_result: bool = a > b; + prusti_result } #[allow(unused_must_use, unused_parens, unused_variables, dead_code, non_snake_case)] @@ -89,7 +91,8 @@ non_snake_case)] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_post_item_test_max4_$(NUM_UUID)(a: i32, b: i32, result: i32) -> bool { - !!((result == max(a, b)): bool) + let prusti_result: bool = result == max(a, b); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::post_spec_id_ref = "$(NUM_UUID)"] @@ -101,7 +104,8 @@ non_snake_case)] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_pre_item_test_max5_$(NUM_UUID)(a: i32, b: i32) -> bool { - !!((a < b): bool) + let prusti_result: bool = a < b; + prusti_result } #[allow(unused_must_use, unused_parens, unused_variables, dead_code, non_snake_case)] @@ -109,7 +113,8 @@ non_snake_case)] #[prusti::spec_id = "$(NUM_UUID)"] fn prusti_post_item_test_max5_$(NUM_UUID)(a: i32, b: i32, result: i32) -> bool { - !!((result == max(a, b)): bool) + let prusti_result: bool = result == max(a, b); + prusti_result } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::post_spec_id_ref = "$(NUM_UUID)"] diff --git a/prusti-viper/src/encoder/mir/pure/pure_functions/encoder_high.rs b/prusti-viper/src/encoder/mir/pure/pure_functions/encoder_high.rs index 9eecbe6c60b..44060d88e92 100644 --- a/prusti-viper/src/encoder/mir/pure/pure_functions/encoder_high.rs +++ b/prusti-viper/src/encoder/mir/pure/pure_functions/encoder_high.rs @@ -371,11 +371,12 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureEncoder<'p, 'v, 'tcx> { self.parent_def_id, assertion_substs, )?; - self.encoder.error_manager().set_error( - encoded_assertion.position().into(), + let original_position = encoded_assertion.position(); + conjuncts.push(self.encoder.set_surrounding_error_context_for_expression( + encoded_assertion, + original_position, ErrorCtxt::PureFunctionDefinition, - ); - conjuncts.push(encoded_assertion); + )); } let post = conjuncts.into_iter().conjoin(); diff --git a/prusti-viper/src/encoder/mir/pure/pure_functions/encoder_poly.rs b/prusti-viper/src/encoder/mir/pure/pure_functions/encoder_poly.rs index fc87248b06b..fc413de09a1 100644 --- a/prusti-viper/src/encoder/mir/pure/pure_functions/encoder_poly.rs +++ b/prusti-viper/src/encoder/mir/pure/pure_functions/encoder_poly.rs @@ -522,10 +522,11 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureFunctionEncoder<'p, 'v, 'tcx> { self.parent_def_id, assertion_substs, )?; - self.encoder - .error_manager() - .set_error(encoded_postcond.pos(), ErrorCtxt::PureFunctionDefinition); - func_spec.push(encoded_postcond); + let new_pos = self.encoder.error_manager().set_surrounding_error_context( + encoded_postcond.pos(), + ErrorCtxt::PureFunctionDefinition, + ); + func_spec.push(encoded_postcond.set_pos(new_pos)); } let post = func_spec.into_iter().conjoin();