Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000372Frama-CPlug-in > value analysispublic2010-01-13 18:392010-04-13 15:33
Reportergmelquio 
Assigned Tovirgile 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Boron-20100401 
Summary0000372: Wrong postconditions are "valid according to value analysis"
Description/*@ ensures \result == 1; */
int main() {
  return 0;
}

When clicking on the "ensures" clause, Frama-C GUI (r7298) reports:

This is an ensures clause.
Status: Valid according to value analysis
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0000621)
pascal (reporter)
2010-01-13 20:11

Version 7304 gives "Unknown"

commandline: bin/viewer.opt -val t.c

Are you sure you did not launch the last released version of the GUI by accident (for instance by typing "frama-c-gui" instead of bin/viewer.opt"?)

(side note: the value analysis does not support "\result" yet so it should always answer "Unknown" for properties that involve it)
(0000622)
gmelquio (reporter)
2010-01-13 20:21

I did launch the GUI, and I confirm it was not by accident. (Why would it be?) That being said, I also confirm that Virgile's commit has fixed the bug.
(0000623)
gmelquio (reporter)
2010-01-13 20:23

Nice. Posting a comment on a "closed" report causes it to reopen. And I can't find a way to close it myself. I so hate Mantis...
(0000624)
pascal (reporter)
2010-01-13 20:52

So Virgile fixed the bug without a changelog entry, and without closing this bug. Mmh... I should report him.
(0000626)
virgile (developer)
2010-01-14 08:58

Well, sorry for not having marked as resolved a bug which was opened 20 minutes _after_ the commit which fixed it and the accompanying e-mail saying so.

- Issue History
Date Modified Username Field Change
2010-01-13 18:39 gmelquio New Issue
2010-01-13 18:39 gmelquio Status new => assigned
2010-01-13 18:39 gmelquio Assigned To => pascal
2010-01-13 20:11 pascal Note Added: 0000621
2010-01-13 20:12 pascal Status assigned => closed
2010-01-13 20:12 pascal Resolution open => unable to reproduce
2010-01-13 20:21 gmelquio Note Added: 0000622
2010-01-13 20:21 gmelquio Status closed => feedback
2010-01-13 20:21 gmelquio Resolution unable to reproduce => reopened
2010-01-13 20:23 gmelquio Note Added: 0000623
2010-01-13 20:52 pascal Note Added: 0000624
2010-01-13 20:52 pascal Status feedback => resolved
2010-01-13 20:52 pascal Resolution reopened => fixed
2010-01-14 08:58 virgile Assigned To pascal => virgile
2010-01-14 08:58 virgile Note Added: 0000626
2010-01-14 08:58 virgile Status resolved => feedback
2010-01-14 08:58 virgile Resolution fixed => reopened
2010-01-14 15:43 virgile Status feedback => resolved
2010-01-14 15:43 virgile Resolution reopened => fixed
2010-04-13 15:30 signoles Status resolved => new
2010-04-13 15:31 signoles Status new => closed
2010-04-13 15:33 signoles Fixed in Version => Frama-C Boron


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker