--- layout: fc_discuss_archives title: Message 48 from Frama-C-discuss on December 2013 ---
Hello Pascal and Lo?c, thanks for discussing the additional ensures clauses of swap. The main reason I added them is related to an incertitude I have about \valid and free. Imagine I have a function foo with the following contract that is verified by WP. /*@ requires \valid(a); assigns \nothing; ensures \result == *a; */ int foo(int* a) { return *a; } But what if someone provides the following implementation int foo(int* a) { int tmp = *a; free(a); return tmp; } Wouldn?t this implementation also satisfy the contract BUT invalidating the pointer a? Adding the clause ?ensures \valid(a);? would in my opinion exclude the second implementation. Jens