Contracts: macro allowing for contraction of specific variables about kani HOT 3 CLOSED

It seems as though deleting

fn visit_receiver(&mut self, _: &'ast syn::Receiver) {
    self.0.insert(Ident::new("self", proc_macro2::Span::call_site()));
}

From the initialize.rs file has no impact on the current tests. This means we are not properly testing consuming the self parameter in a function properly.

This is related to this change as self falls into the same category of arguments that need to be unsafely copied, but adds a layer of complication as self is a reserved keyword and cannot be reassigned.

from kani.

The following two test cases seem to fail kani's checks. Copy is derived in both situations, so it would make sense for the struct to be available in the ensures statement. However, since we are doing an untracked dereference, I suspect that rust memory checker thinks that the memory is no longer needed after the function and frees it, so self_renamed and x_renamed no longer point at valid pieces of data after the function.

// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT
// kani-flags: -Zfunction-contracts

#[derive(Clone,Copy)]
struct DestructSelf;

impl DestructSelf {
    #[kani::requires(self.five()==5)]
    #[kani::ensures(|_| self.five()==5)]
    fn eat(self : DestructSelf){
    }
    fn five(self : &DestructSelf) -> u32{
        5
    }
}

#[kani::proof_for_contract(DestructSelf::eat)]
fn eat_harness() {
    let x = DestructSelf;
    x.eat()
}

// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT
// kani-flags: -Zfunction-contracts

#[derive(Clone,Copy)]
struct Five;

impl Five {
    fn five(self : &Five) -> u32{
        5
    }
}

#[kani::ensures(|result : &Five| x.five() == result.five())]
fn id(x : Five) -> Five {
    x
}

#[kani::proof_for_contract(id)]
fn eat_harness() {
    let x = Five;
    id(x);
}

from kani.

Changed the variable that the old implementation was using so that it uses the variable tracked by rust and not the one that is untracked. This means this is still an issue for the ensures statement as seen in the past two test cases, but no longer for old statements.

from kani.