Frama-C Bug Tracking System - Frama-C
View Issue Details
0000195Frama-CPlug-in > Evapublic2009-07-16 22:352014-02-12 16:56
Frama-C Beryllium-20090601-beta1 
Frama-C Beryllium-20090901 
0000195: wrongly synthesized assert
Let's consider the following program: 1. #include 2. 3. struct my_struct { 4. void * my_field; 5. }; 6. 7. void main(struct my_struct * l) { 8. if (l!=NULL) { 9. if (l->my_field!=NULL) { 10. l->my_field=NULL; 11. } 12. } 13. } Then I launch frama-c-gui and value analysis on entry point 'main'. The following assert is synthesized between line 8 and 9: //@ assert \valid(&l->my_field); Even though l->my_field could be NULL and the program be ok.
No tags attached.
Issue History
2009-07-16 22:35derepasNew Issue
2009-07-16 22:35derepasStatusnew => assigned
2009-07-16 22:35derepasAssigned To => pascal
2009-07-17 10:20pascalNote Added: 0000271
2009-07-17 11:14derepasNote Added: 0000272
2009-07-17 18:32pascalNote Added: 0000278
2009-07-17 18:59svnCheckin
2009-07-17 18:59svnStatusassigned => resolved
2009-07-17 18:59svnResolutionopen => fixed
2009-09-02 10:54signolesStatusresolved => closed
2009-09-02 10:57signolesFixed in Version => Frama-C Beryllium
2018-01-12 14:26signolesCategoryPlug-in > value analysis => Plug-in > Eva

2009-07-17 10:20   
Strictly speaking, this is a feature wish: the only guarantee is that there are no false negatives. False positives happen, and this is one. The problem here comes from the "void*" type for the struct field. If it was of type "pointer to t", the analyzer would allocate a byte array of size (context-width * sizeof(t)) for the pointed area. Unfortunately, there is no meaningful size to use for void, therefore the analyzer is unable to build a precise context in this way and has to resort to building an imprecise context. In the imprecise context the value of l->my_field is a so-called "garbled mix" and it is impossible to represent the fact that inside the innermost then branch, l->my_field is not NULL. Workarounds: instanciate the "void*" field in the actual pointer type that you intend, or, if you are using "void*" to treat the type as abstract, replace it by "char*". It should not matter because you are not dereferencing it because it is abstract.
2009-07-17 11:14   
Ok merci pour la précision !
2009-07-17 18:32   
After discussing the behavior of the analyzer and looking at it again I now think that it is doing the right thing and I need to clarify what. The example (slightly modified): #include struct my_struct { int * my_field; int *m2; }; void main(struct my_struct * l) { if (l!=NULL) { if (l->my_field!=NULL) { l->m2=NULL; } } } The commandline: bin/toplevel.opt -val t.c The alarms: t.c:9: Warning: pointer comparison: assert \pointer_comparable(l, (void *)0); l is an argument of the entry point. Although the analyzer gives it the value {{ &NULL ; &star_l ;}}, star_l is a special variable that gives you, when you access it, the warnings about being potentially invalid at the same time that what happens if it is in fact valid is propagated. This message warns, rightly, that the pointer comparison can be unspecified in some cases. t.c:10: Warning: out of bounds read. assert \valid(&l->my_field); The program attempts to read four bytes (a pointer) from l->my_field. Because you could have passed any pointer l to the function, reading these four bytes could produce undefined results. Having compared l to NULL does not protect against all the possibilities of invalid pointer, which is why the analyzer gives star_l the special status mentioned above. t.c:10: Warning: pointer comparison: assert \pointer_comparable(l->my_field, (void *)0); It could be unspecified to compare the pointer thus obtained to NULL. t.c:11: Warning: out of bounds write. assert \valid(&l->m2); The special status of star_l makes the analyzer warn about the possibility that it is not allowed to write in l->m2. ___________ If you do not want the special status (and the warnings) for variable star_l, you can use the option -context-valid-pointers. This also removes the possibility of the pointers being NULL. It might be interesting to set these two options separately but it is not possible at the moment (it wouldn't be difficult to add if it was desired though).