0002300: suggest to clarify semantics of statement contract in ACSL implementation manual

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0002300

Frama-C

Documentation > ACSL

public

2017-05-11 13:24

2017-07-18 11:13

Reporter

Jochen

Assigned To

patrick

Priority

normal

Severity

text

Reproducibility

N/A

Status

closed

Resolution

no change required

Platform

Silicon/Phosphorus

xubuntu 16.04.1

OS Version

Product 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] [Hide Content]

void foo(void) {
	int x;
	//@ assigns x; ensures x >= 5;
	x = 5;
	//@assert bar: x == 5;
}

Relationships

related to

0002317

assigned

correnson

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