Comparing a function pointer will NULL might raise incorrect warning (#1694) · Issues · pub / frama-c

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.)

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information