Failed Checks: Check that ptr is freeable

[thanhnguyen-aws]

I tried this code:

struct Foo {
    vec: Vec<u8>
}

#[kani::requires (e <10)]
#[kani::modifies(f)]
fn foo_push (f: &mut Foo, e: u8) {
    f.vec.push(e);
}


#[kani::proof_for_contract(foo_push)]
fn proof_foo_push_contract () {
    const FOO_SIZE: usize = 2;
    let bytes: [u8; FOO_SIZE] = kani::any();
    let mut f = Foo { vec: bytes.to_vec() };
    let e : u8 = kani::any();
    foo_push(&mut f, e);
}

#[kani::proof]
#[kani::unwind(5)]
fn proof_foo_push_no_contract () {
    const FOO_SIZE: usize = 2;
    let bytes: [u8; FOO_SIZE] = kani::any();
    let mut f = Foo { vec: bytes.to_vec() };
    let e : u8 = kani::any();
    kani::assume(e < 10);
    foo_push(&mut f, e);
} 

using the following command line invocation:

kani src/example.rs -Zfunction-contracts

with Kani version: 0.57.0

I expected to see this happen: the same results for both harnesses proof_foo_push_contract and proof_foo_push_no_contract.

Instead, this happened:

1. proof_foo_push_contract takes a lot of time and returns "Failed Checks: Check that ptr is freeable"
2. proof_foo_push_no_contract runs very fast and returns "VERIFICATION:- SUCCESSFUL"