suggest to clarify semantics of statement contract in ACSL implementation manual
ID0002300: This issue was created automatically from Mantis Issue 2300. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002300 | Frama-C | Documentation > ACSL | public | 2017-05-11 | 2017-07-18 |
| Reporter | Jochen | Assigned To | patrick | Resolution | no change required |
| Priority | normal | Severity | text | Reproducibility | N/A |
| Platform | Silicon/Phosphorus | OS | xubuntu 16.04.1 | OS Version | - |
| Product Version | - | Target Version | - | Fixed in Version | - |
Description :
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.