Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] ACSL, globals and ghosts
  • From: virgile.prevosto at m4x.org (Virgile Prevosto)
  • Date: Fri, 9 Aug 2013 13:08:23 +0200
  • In-reply-to: <20130809093949.GA5295@damazan>
  • References: <20130809093949.GA5295@damazan>
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