--- layout: fc_discuss_archives title: Message 49 from Frama-C-discuss on December 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] New Version of "ACSL by Example" for Frama-C Fluorine



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