Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000472Frama-CPlug-in > Evapublic2010-05-07 12:352014-02-12 16:55
Reporteryakobowski 
Assigned Topascal 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Boron-20100401 
Target VersionFixed in VersionFrama-C Carbon-20101201-beta1 
Summary0000472: Comparing a function pointer will NULL might raise incorrect warning
DescriptionIn the code below, the value analysis flags the comparison of fun with the NULL pointer as requiring a comparability assertion, while a comparison with the NULL pointer is always legal. void f(void); void g(void); extern int j; int main (void) { void (*fun)(void); int* p; if(j) fun = f; else fun = g; if (fun == 0) return 0; else return 1; } (The problem does not appear if 'fun' is a pointer to only one function, or when comparing non-functional pointers.)
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0000823)
pascal (reporter)
2010-05-10 23:49

"imprecise", not "incorrect".
(0000910)
signoles (manager)
2010-06-04 22:24

Fixed by PC yesterday.

- Issue History
Date Modified Username Field Change
2010-05-07 12:35 yakobowski New Issue
2010-05-07 12:35 yakobowski Status new => assigned
2010-05-07 12:35 yakobowski Assigned To => pascal
2010-05-10 23:49 pascal Note Added: 0000823
2010-06-03 19:39 svn Checkin
2010-06-04 22:24 signoles Note Added: 0000910
2010-06-04 22:24 signoles Status assigned => resolved
2010-06-04 22:24 signoles Fixed in Version => Frama-C Carbon
2010-06-04 22:24 signoles Resolution open => fixed
2010-12-17 19:36 signoles Status resolved => closed
2018-01-12 14:26 signoles Category Plug-in > value analysis => Plug-in > Eva


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker