Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000612Frama-CDocumentation > ACSLpublic2010-10-18 17:482014-02-12 16:55
ReporterJochen 
Assigned Tovirgile 
PrioritynormalSeveritytextReproducibilityN/A
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Boron-20100401 
Target VersionFrama-C Carbon-20101201-beta1Fixed in VersionFrama-C Carbon-20101201-beta1 
Summary0000612: Mention that invariant does not hold after for-loop
DescriptionThe ACSL-1.4 reference, available from http://frama-c.com/acsl.html, [^] explains on p.35-36 where the invariant of a for-loop shall hold as follows: ``The predicate I holds ... right after the initialization expression ...; ­for a for (init; c; step) s loop, I must be preserved by the side-effects of c followed by s followed by step''.
While this is possibly the most compact explanation, it is based on the transformation of "for (init;c;step) s" into "init; while (1) { int C=c; if(!C) break; s; step; }", which seems to be rather unusual. As a consequence, the for-loop invariant does not hold after normal termination, if c has side-effects (cf. attached demonstration program).
This unexpected fact should be mentioned in the ACSL reference.
TagsNo tags attached.
Attached Filesc file icon ftest.c [^] (1,103 bytes) 2010-10-18 17:48 [Show Content]

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2010-10-18 17:48 Jochen New Issue
2010-10-18 17:48 Jochen Status new => assigned
2010-10-18 17:48 Jochen Assigned To => signoles
2010-10-18 17:48 Jochen File Added: ftest.c
2010-10-18 18:01 signoles Assigned To signoles => virgile
2010-10-26 13:12 virgile Target Version => Frama-C Carbon
2010-12-02 16:54 svn Checkin
2010-12-02 16:54 svn Status assigned => resolved
2010-12-02 16:54 svn Resolution open => fixed
2010-12-10 15:45 signoles Fixed in Version => Frama-C Carbon-20101201-beta1
2010-12-17 19:35 signoles Status resolved => closed
2016-06-21 14:11 signoles Category Documentation => Documentation > ACSL


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker