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] Frama C path sensitiveness

Hello David,

> It seems that the "n1 < n2" expression is a bit too complicated for
> the value analysis plugin.
> [...]
> I tried to add an "//@ assert n1 < n2 || n1 >= n2;"

The situation is a little bit like adding

  //@ assert x1 - x0 >= 0.125;

in this example:

http://blog.frama-c.com/index.php?post/2011/03/26/Helping-the-value-analysis-2

It doesn't work because the relation between two variables that you are
offering is not in the general pattern of the information that the value
analysis represents. It generally is able to represent precisely more
simple properties such as "x >= 12" or "x <= 17" or the conjunction
of properties that it can represent (such as the conjunction of the
above). If you are writing assertions for the purpose of helping it,
you should offer them in a format that matches its internal representation
for memory states.

Pascal