diff --git a/tests/expected/function-contract/valid_ptr.expected b/tests/expected/function-contract/valid_ptr.expected index 4014a0723029..3d836112e5c5 100644 --- a/tests/expected/function-contract/valid_ptr.expected +++ b/tests/expected/function-contract/valid_ptr.expected @@ -1,3 +1,8 @@ +Checking 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... VERIFICATION:- SUCCESSFUL (encountered one or more panics as expected) @@ -7,4 +12,4 @@ VERIFICATION:- SUCCESSFUL Checking harness pre_condition::harness_head_ptr... VERIFICATION:- SUCCESSFUL -Complete - 3 successfully verified harnesses, 0 failures, 3 total +Complete - 3 successfully verified harnesses, 1 failures, 4 total diff --git a/tests/expected/function-contract/valid_ptr.rs b/tests/expected/function-contract/valid_ptr.rs index abfa037dcc48..3188765d645e 100644 --- a/tests/expected/function-contract/valid_ptr.rs +++ b/tests/expected/function-contract/valid_ptr.rs @@ -36,7 +36,7 @@ mod pre_condition { 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 _)