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: anne.pacalet at free.fr (Anne Pacalet)
- Date: Tue, 29 Apr 2014 08:14:36 +0200
- In-reply-to: <alpine.LNX.2.03.1404272055440.591@dordowsky.de>
- References: <alpine.LNX.2.03.1404272055440.591@dordowsky.de>
Le 27/04/2014 20:58, Frank Dordowsky a ?crit : > When I try to prove this with the wp plugin, all assertions are > proven, but not the post conditions of the two ensure clauses in the > behavior clauses. What is the reason for that? I think it is because the 'assumes' properties refer to the pre-state, and we don't know anything about the initial value of 'inp', while your assertions refer to 'inp' at the end of the function. What about a post-condition like : ((inp >= 0 ) && (\result == 'p')) || ((inp < 0 ) && (\result == 'n')); Hope this helps, Anne.
- Follow-Ups:
- [Frama-c-discuss] Behavior specification with ghost variables
- From: frank at dordowsky.de (Frank Dordowsky)
- [Frama-c-discuss] Behavior specification with ghost variables
- From: frank at dordowsky.de (Frank Dordowsky)
- [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
- Prev by Date: [Frama-c-discuss] Error on using pp-annot
- 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):