2021-03-01 23:43 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000195Frama-CPlug-in > Evapublic2014-02-12 16:56
Assigned Topascal 
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




pascal (reporter)

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)

Ok merci pour la précision !


pascal (reporter)

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
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
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
2013-12-19 01:13 pascal Source_changeset_attached => framac master eeaa7425
2014-02-12 16:56 pascal Source_changeset_attached => framac stable/neon eeaa7425
2018-01-12 14:26 signoles Category Plug-in > value analysis => Plug-in > Eva
+Issue History