--- layout: fc_discuss_archives title: Message 18 from Frama-C-discuss on April 2016 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] hint assertions and understanding cooperation between wp and value plugin



Thank you very much Loïc and Boris for your answers! This improved my
understanding of wp and value cooperation.

The need of float model for this was a bit fuzzy for me, so following your
remarks, I checked my assumptions with frama-c:

/*@ lemma sq_double: \forall double x; x*x >= 0.; */

is verifiable and value analysis shows that x*x >= 0 
with -val-subdivide-non-linear 1094

So, in this case, I understand that the proof had the meaning I wanted!
But, then this makes me realize that something like:

#include <__fc_builtin.h>

/*@ lemma sq_double: \forall real x; x*x - .2 * x + 0.01 >= 0.; */
int main()
{
  double x = Frama_C_double_interval(-1., 1.);
  double x1 = x*x - .2 * x + 0.01;
  /*@ assert x1 >= 0; */
}

is ok in the real model with:
frama-c -val t.c -wp -wp-prover z3

and hopefully cannot be verified with:
frama-c -val t.c -wp -wp-prover z3 -wp-model float

On the other side, (x - .1)*(x - .1) >= 0 is verifiable with -wp
-wp-model float but I did not manage to verify it with the value plugin
alone and -val-subdivide-non-linear (I stopped the computation after
99999)