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

  • Subject: [Frama-c-discuss] Assign clauses with ghost variables
  • From: frank at dordowsky.de (Frank Dordowsky)
  • Date: Sun, 31 May 2015 14:04:08 +0200 (CEST)
  • In-reply-to: <mailman.5768.1432882366.22323.frama-c-discuss@lists.gforge.inria.fr>
  • References: <mailman.5768.1432882366.22323.frama-c-discuss@lists.gforge.inria.fr>
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