Fix syntax and expected output

model-checking · Jan 22, 2025 · cf697f7 · cf697f7
1 parent ed261e3
commit cf697f7
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 2 deletions.
diff --git 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
@@ -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<char> {
         let var = 'c';
         PtrWrapper(&var as *const _)