diff --git a/tests/expected/function-contract/valid_ptr.expected b/tests/expected/function-contract/valid_ptr.expected index 0f8100c7ceeb..38f31a63d5ca 100644 --- a/tests/expected/function-contract/valid_ptr.expected +++ b/tests/expected/function-contract/valid_ptr.expected @@ -1,3 +1,8 @@ +Checking harness post_condition::harness... +Failed Checks: Kani does not support reasoning about pointer to unallocated memory +Failed Checks: |result| kani::mem::can_dereference(result.0) +VERIFICATION:- FAILED + Checking harness pre_condition::harness_invalid_ptr... Failed Checks: assertion failed: unsafe { read_ptr(ptr) } == -20 Failed Checks: Kani does not support reasoning about pointer to unallocated memory @@ -10,4 +15,4 @@ VERIFICATION:- SUCCESSFUL Checking harness pre_condition::harness_head_ptr... VERIFICATION:- SUCCESSFUL -Complete - 2 successfully verified harnesses, 1 failures, 3 total +Complete - 2 successfully verified harnesses, 2 failures, 4 total diff --git a/tests/expected/function-contract/valid_ptr.rs b/tests/expected/function-contract/valid_ptr.rs index 9537ecc30daa..d66c433cd01e 100644 --- a/tests/expected/function-contract/valid_ptr.rs +++ b/tests/expected/function-contract/valid_ptr.rs @@ -3,8 +3,6 @@ // kani-flags: -Zfunction-contracts -Zmem-predicates //! Test that it is sound to use memory predicates inside a contract pre-condition. -//! We cannot validate post-condition yet. This can be done once we fix: -//! mod pre_condition { /// This contract should succeed only if the input is a valid pointer. @@ -34,12 +32,10 @@ mod pre_condition { } } -/// TODO: Enable once we fix: -#[cfg(not_supported)] mod post_condition { /// This contract should fail since we are creating a dangling pointer. - #[kani::ensures(kani::mem::can_dereference(result.0))] + #[kani::ensures(|result| kani::mem::can_dereference(result.0))] unsafe fn new_invalid_ptr() -> PtrWrapper { let var = 'c'; PtrWrapper(&var as *const _)