2021-02-27 10:40 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000077Frama-CPlug-in > Evapublic2014-02-12 16:56
Reporterpascal 
Assigned Topascal 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Beryllium-20090601-beta1 
Summary0000077: if((int)(&a+2)) fails to warn about being unspecified
Descriptionsee summary.
This is related to bug 76, which is fixed and partially fixes
this problem too: at least the condition is correctly
analyzed as being 0 or 1. But the policy is to emit an alarm
(that is complicated to express, but that's another issue)
and to consider the condition to be 1 modulo the verification
of the alarm.
TagsNo tags attached.
Attached Files

-Relationships
+Relationships

-Notes
There are no notes attached to this issue.
+Notes

-Issue History
Date Modified Username Field Change
2009-05-05 22:00 pascal New Issue
2009-05-05 22:00 pascal Status new => assigned
2009-05-05 22:00 pascal Assigned To => pascal
2009-05-06 15:50 svn
2009-05-06 15:50 svn Status assigned => resolved
2009-05-06 15:50 svn Resolution open => fixed
2009-06-23 18:02 signoles Status resolved => closed
2009-06-23 18:03 signoles Fixed in Version => Frama-C Beryllium beta-1
2013-12-19 01:13 pascal Source_changeset_attached => framac master 102d243c
2014-02-12 16:56 pascal Source_changeset_attached => framac stable/neon 102d243c
2018-01-12 14:26 signoles Category Plug-in > value analysis => Plug-in > Eva
+Issue History