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
- Subject: [Frama-c-discuss] Behavior specification with ghost variables
- From: frank at dordowsky.de (Frank Dordowsky)
- Date: Tue, 29 Apr 2014 21:27:05 +0200 (CEST)
- In-reply-to: <535F434C.7030105@free.fr>
- References: <alpine.LNX.2.03.1404272055440.591@dordowsky.de> <535F434C.7030105@free.fr>
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
- Follow-Ups:
- [Frama-c-discuss] Behavior specification with ghost variables
- From: virgile.prevosto at m4x.org (Virgile Prevosto)
- [Frama-c-discuss] Behavior specification with ghost variables
- References:
- [Frama-c-discuss] Behavior specification with ghost variables
- From: frank at dordowsky.de (Frank Dordowsky)
- [Frama-c-discuss] Behavior specification with ghost variables
- From: anne.pacalet at free.fr (Anne Pacalet)
- [Frama-c-discuss] Behavior specification with ghost variables
- Prev by Date: [Frama-c-discuss] Behavior specification with ghost variables
- Next by Date: [Frama-c-discuss] Behavior specification with ghost variables
- Previous by thread: [Frama-c-discuss] Behavior specification with ghost variables
- Next by thread: [Frama-c-discuss] Behavior specification with ghost variables
- Index(es):