Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000399Frama-CPlug-in > jessiepublic2010-02-06 12:182010-04-19 16:14
Reporterdpariente 
Assigned Tocmarche 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Boron-20100401 
Summary0000399: Statement contract and "hiding" of statement
DescriptionHello,

On the following annotated code:

int main(int x)
{ int y=0;
 //@ assigns y; ensures y==3;
 y=x;
 //@ assert y>0;
}

analyzed by: frama-c -jessie foo.c
assert y>0 is not discharged (no matter the preceding statement contract is valid or not).

Indeed, statement contract (assigns y; ensures y==3;) doesn't seem to be taken into account as it does not appear in .jc file.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0000675)
cmarche (developer)
2010-02-10 15:31


Fixed in Why CVS.

A small issue remains: localization of the requires clause of statement contracts
is wrong: this is a problem within Why itself: bad handling of localization of "any" black boxes.

(0000778)
signoles (manager)
2010-04-19 16:14

Fix in Why 2.24 (require Frama-C Boron-20100401).

- Issue History
Date Modified Username Field Change
2010-02-06 12:18 dpariente New Issue
2010-02-06 12:18 dpariente Status new => assigned
2010-02-06 12:18 dpariente Assigned To => cmarche
2010-02-10 15:31 cmarche Note Added: 0000675
2010-02-10 15:31 cmarche Status assigned => resolved
2010-02-10 15:31 cmarche Resolution open => fixed
2010-02-10 15:31 cmarche Additional Information Updated
2010-04-19 16:13 signoles Status resolved => closed
2010-04-19 16:13 signoles Fixed in Version => Frama-C Boron
2010-04-19 16:14 signoles Note Added: 0000778


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker