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

[Frama-c-discuss] ACSL, globals and ghosts



Hello Pierre-Lo?c,

2013/8/9 Pierre-Lo?c Garoche <Pierre-Loic.Garoche at onera.fr>:
> How do global variables interact with contracts? When used in ensures, it seems
> that the global variable appear as a typed free variable. No knwoledge at all
> about its value, even when it is just a constant. For example, the following
> ensures is not proved automatically.
>
> int x = 0;
>
> /*@ requires y >= 0;
>   @ ensures \result > x;
>   @*/
> int f(int y) { return y +1; }

Well, we don't have any information about the value of x when entering
function f: it can very well be modified between initialization and
call site. Admittedly, if x was declared const int, it could be said
to be 0, but since this is can easily be defeated by a cast, we chose
not to rely on it in Frama-C.
On the other hand, if you explicitly say that f is the main entry
point of your program, then we know that in the pre-state x is 0, and
the ensures is easily discharged, as you can see with frama-c -wp
-main f file.c

>
> * Additional ghost field in a struct
>
> The manuel mentions ghost fields: If a structure has ghost fields, the sizeof of
> the structure is the same has the structure without ghost fields. Also,
> alignment of fields remains unchanged
>
> However, it doesn't seems accepted by the Fluorine (June release) and it is not
> colored in red in the ACSL implementation document.
>
This is a bug in the implementation notes. Thanks for having reported it.

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile