Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001316Frama-CPlug-in > wppublic2012-11-22 21:462014-02-12 16:58
Reportersduprat 
Assigned Tocorrenson 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Oxygen-20120901 
Target VersionFixed in VersionFrama-C Fluorine-20130401 
Summary0001316: false property proved intTyped (if confirmed)
DescriptionIn the attached exemple, the property OUT_ko3 of f2b is proved while it seems to be not a true property.
The problem is in Typed and not in Store.

The problem is also in SVN 20767.
Additional Information//frama-c -wp rp2.c -wp-byreference -wp-model Store --> OK
//frama-c -wp rp2.c -wp-byreference -wp-model Typed --> f1b/OUT_ko3 is proved
TagsNo tags attached.
Attached Filesc file icon rp2.c [^] (591 bytes) 2012-11-22 21:46 [Show Content]

- Relationships

-  Notes
(0004599)
correnson (manager)
2014-02-12 16:58

Fix committed to stable/neon branch.

- Issue History
Date Modified Username Field Change
2012-11-22 21:46 sduprat New Issue
2012-11-22 21:46 sduprat Status new => assigned
2012-11-22 21:46 sduprat Assigned To => correnson
2012-11-22 21:46 sduprat File Added: rp2.c
2012-12-07 13:18 svn Checkin
2012-12-07 13:18 svn Status assigned => resolved
2012-12-07 13:18 svn Resolution open => fixed
2013-04-19 11:05 signoles Fixed in Version => Frama-C Fluorine
2013-04-19 11:05 signoles Status resolved => closed
2014-02-12 16:58 correnson Note Added: 0004599
2014-02-12 16:58 correnson Status closed => resolved


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker