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.
|ID0002300||Frama-C||Documentation > ACSL||public||2017-05-11||2017-07-18|
|Reporter||Jochen||Assigned To||patrick||Resolution||no change required|
|Platform||Silicon/Phosphorus||OS||xubuntu 16.04.1||OS Version||-|
|Product Version||-||Target Version||-||Fixed in Version||-|
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.