--- layout: fc_discuss_archives title: Message 40 from Frama-C-discuss on May 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Assign clauses with ghost variables



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