--- layout: fc_discuss_archives title: Message 41 from Frama-C-discuss on April 2014 ---
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