Comparing a function pointer will NULL might raise incorrect warning
ID0000472: This issue was created automatically from Mantis Issue 472. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000472 | Frama-C | Plug-in > Eva | public | 2010-05-07 | 2014-02-12 |
| Reporter | yakobowski | Assigned To | pascal | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Boron-20100401 | Target Version | - | Fixed in Version | Frama-C Carbon-20101201-beta1 |
Description :
In 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.)