|Anonymous | Login | Signup for a new account||2017-09-25 00:51 CEST|
|Main | My View | View Issues | Change Log | Roadmap | Repositories|
|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0002300||Frama-C||Documentation > ACSL||public||2017-05-11 13:24||2017-07-18 11:13|
|Status||closed||Resolution||no change required|
|Platform||Silicon/Phosphorus||OS||xubuntu 16.04.1||OS Version|
|Target Version||Fixed in Version|
|Summary||0002300: suggest to clarify semantics of statement contract in ACSL implementation manual|
|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.
|Tags||No tags attached.|
|Attached Files||contractTest.c [^] (93 bytes) 2017-05-11 13:24 [Show Content]|
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.
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.
|2017-05-11 13:24||Jochen||New Issue|
|2017-05-11 13:24||Jochen||Status||new => assigned|
|2017-05-11 13:24||Jochen||Assigned To||=> patrick|
|2017-05-11 13:24||Jochen||File Added: contractTest.c|
|2017-06-28 09:08||patrick||Note Added: 0006415|
|2017-06-28 10:03||patrick||Note Added: 0006416|
|2017-06-28 10:03||patrick||Status||assigned => closed|
|2017-06-28 10:03||patrick||Resolution||open => no change required|
|2017-07-18 11:13||yakobowski||Relationship added||related to 0002317|
|Copyright © 2000 - 2017 MantisBT Team|