Strange behaviour of programs with contract

[jesper-amilon]

This contract verifies as safe, but it seems it should not, since the assertion in main() does not follow from the post-condition for foo(). If you change the contract to "ensures x >= 0", it seems to verify.
int x;
/*@
ensures x > 0;
*/
void foo(){
x =2;
}

void main() {
foo();
assert(x == 2);
}

[zafer-esen]

TriCera shows that the post-condition holds when verifying foo, but uses the method body in main rather than the weaker postcondition, which allows the verification of the assertion. Essentially, the ensures clause is currently equivalent to an assert statement at the end of its method body.

The expected behaviour would be to use the provided contracts rather than the method body at call sites. This would also be a step in the direction of modular verification in TriCera.

[jesper-amilon]

Ideally maybe the user could specify with a comman-line flag if tricera should verify modularly or not when seeing a contract.