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] Assign clauses with ghost variables

Hello David,

2015-05-28 9:52 GMT+02:00 David MENTRE <dmentre at linux-france.org>:
>
> In my humble opinion, there is lack of abstraction of Frama-C in such
> situations. You need to mention every modified variable in contracts, even
> those that you would like to be hidden. For example, I see no way to use
> static variables (variable local to a file, but if used should be mentioned
> in contract therefore seen from outside!).

You're perfectly right, we lack an option of an abstract memory region
(and probably some separation formulas saying that the visible part of
the memory is separated from it). This shows up for static variables
C, but would be much more widespread for private members of C++
classes. I don't have any really satisfying solution for now, but the
following work:

--- static.h
#define INITSTATE (1)
//@ ghost int gState=INITSTATE;

//@ logic int* abstract_region;

/*@
  @  assigns gState, *abstract_region;
  @  ensures val == gState;
  @*/
void set_state(int val);

--- static.c
#include "static.h"
static int the_state = 0;

//@ axiomatic State { axiom internal_state: abstract_region == &the_state; }

void set_state(int val) {
  the_state = val;
//@ ghost gState = the_state;
}

---
Note however that if you use static.h without static.c, you will need
to add \separate(abstract_region,xxx) axioms for basically all your
global variables[1] (a plug-in might help here, but this is still
tedious), otherwise set_state will have the ability to write anywhere
in memory. It would be interesting to investigate how to handle
natively these kinds of abstract regions, but this is not an easy
goal. In the mean time, Patrick's solution seems a more sensible
workaround.

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile
[1] I make absolutely no warranty about whether this is sufficient to
make WP happy