Frama-C Bug Tracking System - Frama-C
View Issue Details
0001647Frama-CPlug-in > wppublic2014-02-17 15:582015-03-17 22:17
Anne 
correnson 
normalminorhave not tried
closedfixed 
 
Frama-C Sodium 
0001647: compatibility between \null in ACSL and NULL in C in wp
I have tried to prove properties involving NULL pointers, and I had problem to write the ACSL part. Here is and example: /*@ ensures e1: \result == \null; ensures e2: \result == 0; ensures e3: \result == (int *) \null; ensures e4: \result == (int *) 0; ensures e5: \result == (int *)((void *)0); */ int * f (void) { return NULL; } None of the properties are proved with the default memory model. I finally manage to prove them with: -wp-model Typed+cast Since NULL is used very often in programs, even with a clean typing, maybe something could be done for this special case ? Just a suggestion... ;-)
No tags attached.
Issue History
2014-02-17 15:58AnneNew Issue
2014-02-17 15:58AnneStatusnew => assigned
2014-02-17 15:58AnneAssigned To => correnson
2014-06-02 13:58corrensonNote Added: 0005177
2014-06-02 13:58corrensonStatusassigned => resolved
2014-06-02 13:58corrensonResolutionopen => fixed
2015-03-17 22:17signolesFixed in Version => Frama-C Sodium
2015-03-17 22:17signolesStatusresolved => closed

Notes
(0005177)
correnson   
2014-06-02 13:58   
Fix committed to master branch.