--- layout: fc_discuss_archives title: Message 49 from Frama-C-discuss on December 2013 ---
Hello Jens, Le lun. 16 d?c. 2013 11:01:03 CET, "Gerlach, Jens" <jens.gerlach at fokus.fraunhofer.de> a ?crit : > /*@ > requires \valid(a); > assigns \nothing; > ensures \result == *a; > */ > int foo(int* 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 No, it won't satisfy the contract. As soon as a is freed, *a can be anything. On the other hand, it would satisfy ensures \result == \old(*a); Another possibility of "strange" behavior would be something like /*@ requires \valid(a); assigns \nothing; ensures \result == a; */ int* foo(int* a) { int tmp = a; free(a); return tmp; } but then, the contract is missing a frees a; clause (which defaults implicitely to frees \nothing; allocates \nothing; meaning that the function should not (de)allocate anything, as is the case for most C functions). Best regards, -- E tutto per oggi, a la prossima volta. Virgile