Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Pointer comparable warnings and NULL test for parameter

Hello,

here is first the short answer to your question: if you want to test
that function f() works well when passed either NULL or a valid
pointer to an int containing any value, describe these hypotheses
thus:

int u();

int main() {
  int x = u();
  int *p = u() ? NULL : &x;
  f(p);
}

This may seem like a lot of work, but it is only about the same work
as you would need to write a unit test for f(). The difference is that
in this main() you have described all the circumstances in which you
expect f() to work, instead of just one case.

Now, perhaps your function f() expects instead a valid pointer to the
beginning of an array of two ints, and it is not designed to receive
NULL (a perfectly valid design decision as long as it is documented.
Most C standard library functions work this way, not testing for NULL
because it is the caller's responsibility not to pass it). Also the
function f() should only write to the passed array and not read from
it. You can capture these conditions so:

int main() {
  int t[2]; // uninitialized
  f(t);
}

To summarize the short answer: to work precisely, the analyzer needs a
description of the function's expectations. You already know one
language in which these descriptions can be written: you can write
them in C. They look like unit tests but they are much, much more
powerful, and thus less boring.

If you provide the sort of information described above to the
analyzer, it should not warn about invalid pointer comparisons.

On Wed, Mar 20, 2013 at 9:49 AM,  <benoit.gerard at dga.defense.gouv.fr> wrote:
> When trying to analyse a function using value I get \pointer_comparable
> warnings for each test on pointer parameters (== NULL).
> I did not manage to understand why it does so: the only clue I found is a
> post on the blog that considers more advanced situations than just comparing
> a pointer to NULL.

This (http://blog.frama-c.com/index.php?post/2011/06/04/Valid-compare-pointers
) is the right clue but there is not nearly enough information to
understand what is happening here. The issue the analyzer sees is
indeed that it looks like function f() may compare an invalid pointer
to NULL.

Just like &x - 1234 == NULL is a dangerous test that can be true or
false depending where variable x is placed in memory, any comparison
between an invalid pointer and NULL is considered dangerous because
non-deterministic. Plus you never know how an optimizing compiler is
going to transform it (http://lwn.net/Articles/278137/ ).

The reason tab is considered a possibly invalid pointer is that it is
a pointer argument to the entry function of the analysis. The memory
blocks reserved as destination for these pointers have a special
status to reflect the fact that the analyzer is not sure exactly
whether they should be considered valid memory and how large they are.

The simplest solution is to give the analyzer more information.
Following the short answer's recommendation, if you want it to
consider NULL, say so explicitly. If you want it to consider pointers
to arrays between 1 and 10 in size, say it (I would recommend doing 10
separate analyses, each with an array of known size). There is no way
the one-size-fits-all initial context generated when the entry point
has pointer as argument can satisfy you, because passing pointers as
arguments in C can mean too many different things.

Pascal