--- layout: fc_discuss_archives title: Message 18 from Frama-C-discuss on April 2016 ---
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)