Frama-C Bug Tracking System - Frama-C
View Issue Details
0002300Frama-CDocumentation > ACSLpublic2017-05-11 13:242017-07-18 11:13
Jochen 
patrick 
normaltextN/A
closedno change required 
Silicon/Phosphorusxubuntu 16.04.1
 
 
0002300: suggest to clarify semantics of statement contract in ACSL implementation manual
We were wondering about the semantical difference between assertions and a statement contract. Therefore, we ran "frama-c -wp contractTest.c" on the attached program (Frama-c version Phosphorus-20170501-beta1). The assertion "bar" couldn't be proven (without the statement contract, it could). This supports our hypothesis that a statement contract completely overrides the standard Hoare-calculus semantics. However, this isn't explicitly stated in the ACSL Implementation manual (version Silicon-20161101), where statement contracts are mentioned on p.12 and 36, and mainly in their own section (2.4.4) on p.44-45. We therefore wonder if the observed "override behavior" is just special to the WP plugin, or if it is part of the ACSL language definition and obligatory for all plug-ins. An appropriate sentence in section 2.4.4 could clarify this question.
No tags attached.
related to 0002317assigned correnson Statement contracts and WP 
c contractTest.c (93) 2017-05-11 13:24
https://bts.frama-c.com/file_download.php?file_id=1175&type=bug
Issue History
2017-05-11 13:24JochenNew Issue
2017-05-11 13:24JochenStatusnew => assigned
2017-05-11 13:24JochenAssigned To => patrick
2017-05-11 13:24JochenFile Added: contractTest.c
2017-06-28 09:08patrickNote Added: 0006415
2017-06-28 10:03patrickNote Added: 0006416
2017-06-28 10:03patrickStatusassigned => closed
2017-06-28 10:03patrickResolutionopen => no change required
2017-07-18 11:13yakobowskiRelationship addedrelated to 0002317

Notes
(0006415)
patrick   
2017-06-28 09:08   
This has nothing to do with the ACSL manual. The ASCL manual gives the semantics of the properties, and states nothing on how tools have to uses properties to prove others properties. For exemple, ACSL does not say that tools have to use a cut strategy for assert properties. Yes, the observed "override behavior" is just special to the WP plugin.
(0006416)
patrick   
2017-06-28 10:03   
The semantics of statement contracts in ACSL implementation manual seems clear enough to state about the veracity of such contracts. Proof strategies are out of scope the ACSL manual.