Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000195Frama-CPlug-in > Evapublic2009-07-16 22:352014-02-12 16:56
Assigned Topascal 
PlatformOSOS Version
Product VersionFrama-C Beryllium-20090601-beta1 
Target VersionFixed in VersionFrama-C Beryllium-20090901 
Summary0000195: wrongly synthesized assert
DescriptionLet'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.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
pascal (reporter)
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.
derepas (reporter)
2009-07-17 11:14

Ok merci pour la précision !
pascal (reporter)
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).

- Issue History
Date Modified Username Field Change
2009-07-16 22:35 derepas New Issue
2009-07-16 22:35 derepas Status new => assigned
2009-07-16 22:35 derepas Assigned To => pascal
2009-07-17 10:20 pascal Note Added: 0000271
2009-07-17 11:14 derepas Note Added: 0000272
2009-07-17 18:32 pascal Note Added: 0000278
2009-07-17 18:59 svn Checkin
2009-07-17 18:59 svn Status assigned => resolved
2009-07-17 18:59 svn Resolution open => fixed
2009-09-02 10:54 signoles Status resolved => closed
2009-09-02 10:57 signoles Fixed in Version => Frama-C Beryllium
2018-01-12 14:26 signoles Category Plug-in > value analysis => Plug-in > Eva

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker