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] a value analysis case studie

Hello St?phane,

I am afraid I only have a partial solution. The crux of the problem is
that state subdivisions that happen in a callee cannot be propagated
to the caller; only the union of the states is returned. Unless you
are willing to write the conditions that lead init2() to succeed in
terms that the value analysis can understand: in this case you can
subdivide along this line inside the body of f1(), before calling
init1(), and you do not need any new feature.

It would be possible to return subdivisions that have been made at the
strategic place in init1() to f1(). If your actual functions are
simple enough, it would work. If they have complicated logic, the
combinatorial explosion that was limited by the current propagation
strategy would prevent you from taking advantage of it.

> But values computed by the tool for index at the exit of init1() is
> [--...--]. And there is no relational properties between the exit status of
> init1() and index (for ex: "\result ==0 => index==0").

The value analysis only uses disjunctions for state subdivision.
The way to write the implication above in a way that is useful to the
value analysis is:

//@ assert (res == 0 && index == 0) || res == -1;

or more generally if you do not know that res can only be 0 or -1:

//@ assert (res == 0 && index == 0) || res <0 || res > 0;

For instance, I annotated your code so:

//@ ensures (\result == 0 && index == 0) || \result == -1;
int init1(void)
{
  ...
}

...
  res = init1();

//@ assert (res == 0 && index == 0) || res == -1;
  if (res == 0)
    return tab[index+n];

With these annotations, the value analysis proves the post-condition
of init1, and takes advantage of the assertion to omit the alarm on
the tab access. The reasoning step that is missing is to deduce the
assertion from the post-condition of init1. But in effect, I have only
used ACSL to force the propagation of subdivided states from init1 to
f1 here.

Perhaps we can take the discussion of the real examples and the
applicability of the new feature I described to them off-list. Or if
you are willing to write the annotations as above, we can discuss
whether deductive techniques can prove the assertion from the
post-condition.

Pascal