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] RE : Frama-C : Value Analysis : SWITCH vs IF

>the assert status computed by Value Analysis is "Unknown".
>Replacing "*min = Frama_C_float_interval(-100.0,100.0);" 
>with "*min = nd() ? -100.0 : 100.0;" (-slevel > 2)
>allows to validate the assert (i.e., replacing the whole interval with an "enumerate" of states yields a "Valid" status).

The substitution that you are proposing means that only
4 possible couples of values are taken into account for *x and *min:
(-1000.,-100.), (+1000.,-100.), (-1000.,+100.), (+1000.,+100.)
Of course that's easier and it just happens that the value analysis
is able to give a precise answer in this case, but since the
property that you wanted to verify was not only for these four
couples of values, it's useless.

If I may insist on this capital point of methodology:
When you write "nd() ? -100. : 100.", you are making the
analyzer lose precision "on purpose". You are not interested
in these only two values, but you expect the analyzer to
make approximations and you expect the set of values
actually propagated to contain all the values you are 
really interested in (that's the interval [-100.,100]).

It is a very bad idea to do this. We spend our time 
improving the analysis, which means in each new version,
avoiding the gross approximations that were taking place
in the previous versions. In other words, we are actively
trying to break your verification projects (if they
employ such tricks) and render them meaningless
with each new version. And we will continue to do so.
Believe me.

A few functions to introduce non-determinism are provided.
Use them as if they were opaque. These functions are
guaranteed to continue to have the same effects in future
versions, even if precision improves (we'll adapt the
definitions of the functions as necessary).

Do not write x = y = Frama_C_interval(0, 10);
if you mean that x and y should vary independently in this
interval, just because
you believe that the value analysis will treat it the same
as:
x = Frama_C_interval(0, 10);
y = Frama_C_interval(0, 10);

It may already not do so in the Lithium version, and even if it
does for your particular program, it may stop to do so
in the next version.

>With the code above (only using Frama_C_float_interval),
>Value Analysis will not consider "*y >= *min" as Valid at
>the return control point, even if it is located 
>after the aforementionned assert.
>This is due to the fact that one can reduce the state with intervals of values,
>but not with relations between variables, as Virgile mentionned in one of his 
>previous mails (that is to say, not before embedding APRON library or equivalent), isn't it?

You are completely right.

>Then, with the current version of the tool, do you see any means
>to make Value Analysis take into account the assert in calling functions to g()?

I have seen a neat little plug-in appear in the development version
which seems to recognize that an assertion is syntactically the
same as another assertion in a program point where the values
of the variables involved are guaranteed to be unchanged
(and therefore the two assertions, however complicated, can be
recognized as equivalent). If the
author of this plug-in recognizes emself, ey may explain what 
can expected from it.

Apart from that, and until the "APRON Frama-C plug-in", there are
the Hoare logic plug-ins.

Pascal