--- layout: fc_discuss_archives title: Message 30 from Frama-C-discuss on May 2015 ---
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