Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002300Frama-CDocumentation > ACSLpublic2017-05-11 13:242017-07-18 11:13
ReporterJochen 
Assigned Topatrick 
PrioritynormalSeveritytextReproducibilityN/A
StatusclosedResolutionno change required 
PlatformSilicon/PhosphorusOSxubuntu 16.04.1OS Version
Product Version 
Target VersionFixed in Version 
Summary0002300: suggest to clarify semantics of statement contract in ACSL implementation manual
DescriptionWe 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.
TagsNo tags attached.
Attached Filesc file icon contractTest.c [^] (93 bytes) 2017-05-11 13:24 [Show Content]

- Relationships
related to 0002317assignedcorrenson Statement contracts and WP 

-  Notes
(0006415)
patrick (developer)
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 (developer)
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.

- Issue History
Date Modified Username Field Change
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
Powered by Mantis Bugtracker