Frama-C Bug Tracking System - Frama-C
View Issue Details
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.
Relationships
Attached Files

Notes
(0000823)
pascal   
2010-05-10 23:49   
"imprecise", not "incorrect".
(0000910)
signoles   
2010-06-04 22:24   
Fixed by PC yesterday.

Issue History
Date ModifiedUsernameFieldChange
2010-05-07 12:35yakobowskiNew Issue
2010-05-07 12:35yakobowskiStatusnew => assigned
2010-05-07 12:35yakobowskiAssigned To => pascal
2010-05-10 23:49pascalNote Added: 0000823
2010-06-03 19:39svn
2010-06-04 22:24signolesNote Added: 0000910
2010-06-04 22:24signolesStatusassigned => resolved
2010-06-04 22:24signolesFixed in Version => Frama-C Carbon
2010-06-04 22:24signolesResolutionopen => fixed
2010-12-17 19:36signolesStatusresolved => closed
2013-12-19 01:13pascalSource_changeset_attached => framac master ce6b7d50
2014-02-12 16:55pascalSource_changeset_attached => framac stable/neon ce6b7d50
2018-01-12 14:26signolesCategoryPlug-in > value analysis => Plug-in > Eva