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] hint assertions and understanding cooperation between wp and value plugin

  • Subject: [Frama-c-discuss] hint assertions and understanding cooperation between wp and value plugin
  • From: Maurice.Bremond at inria.fr (Maurice Bremond)
  • Date: Mon, 25 Apr 2016 12:52:42 +0200
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)