--- layout: fc_discuss_archives title: Message 40 from Frama-C-discuss on May 2015 ---
Responding to Patrick > The use of the nonfree ACSL importer plug-in is the industrial solution > to that scoping problem. > It solves most of the real industrial needs since industrials use naming > rules. > Sorry, I could not locate this ACSL importer plugin on Frama-C website (also not on the external plug-ins site). Is it internal to some company? > In your example, an alternative based on the merge of several contracts > done by Frama-C tool could help ; > but that functionality is undocumented : > Just add > //@assigns the_state; > in your C source file between line > static int the_state = 0; > and > void set_state(int val) { > > Then, Frama-C tool will generate the clause > //@assigns the_state, gState; > for the contract of the function set_state. > Adding the assigns clause in the body indeed works. But I like to make matter a bit more complicated (as it is in practice): the update to the internal state is guarded as shown in the following extension of my example: ------ /*@ @ behavior Change: @ assumes gState == 0; @ assigns gState; @ ensures val == gState; @ behavior Keep: @ assumes gState != 0; @ assigns \nothing; @ ensures gState == \old(gState); @ complete behaviors; @ disjoint behaviors; @*/ void set_state(int val); ----- The implementation is corresponding: ------ void set_state(int val) { //@ assert the_state == gState; if ( the_state == 0 ) { the_state = val; //@ ghost gState = the_state; } } ------- Now the simple assings clause in front of the function definition is no longer sufficient because the state variable the_state is not always modified. The solution I have found is to repeat the complete specification in the body by replacing the ghost state gState with the real state the_state, i.e. adding the following ACSL annotation in front of the body: ------- /*@ @ behavior Change: @ assumes the_state == 0; @ assigns the_state; @ ensures val == the_state; @ behavior Keep: @ assumes the_state != 0; @ assigns \nothing; @ ensures the_state == \old(the_state); @ complete behaviors; @ disjoint behaviors; @*/ ------- However, this is stil not sufficient, in order to prove the completeness of the behaviors, I had to add the following axiom: ----- /*@ axiomatic equivalence { @ axiom force_equal: \forall int the_state, gState; the_state == gState; @ } @*/ ----- The whole approach of repeating the specification is not very elegant, especially in real world specifications that are much more extensive. On the other hand, this could be done by a tool if the tool knows which ghost variable corresponds to what real state variable. Or is there a better solution? Frank