Frama-C Bug Tracking System - Frama-C
View Issue Details
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 <stdlib.h>
 3. struct my_struct {
 4. void * my_field;
 5. };
 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

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 <stdlib.h>

struct my_struct {
   int * my_field;
   int *m2;

void main(struct my_struct * l) {
  if (l!=NULL) {
    if (l->my_field!=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
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
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:59svn
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
2013-12-19 01:13pascalSource_changeset_attached => framac master eeaa7425
2014-02-12 16:56pascalSource_changeset_attached => framac stable/neon eeaa7425
2018-01-12 14:26signolesCategoryPlug-in > value analysis => Plug-in > Eva