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] Behavior specification with ghost variables

There is a way to use behavior specifications together with ghost 
variables by removing the assume clause and placing the assume
expression into a condition within the ensures clause, as shown
in the example below:

// file: ifbvr.h

//@ ghost int inp;

/*@
   @ ensures ! ((inp >= 0) && (inp < 0));
   @ behavior Higher:
   @  ensures inp >= 0 ==> \result == 'p';
   @ behavior Lower:
   @  ensures inp < 0 ==> \result == 'n';
   @ complete behaviors;
   @*/
char foo ();

The top ensures clause replaces the disjoint clause, i.e. it is a
manually established disjoint. In my example it is trivial, but it may
get very large and complicated if there are more than two behavior
specifications.

I also tried model variables because they are advocated in the ACSL
specification 1.7 as means to "...provide abstract specifications to
functions whose concrete implementation must remain private".
Unfortunately, it seems that model variables are not yet implemented in 
Fluorine.

Frank