--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on May 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



My mistake. I coalesced two different things when replying to Maurice :

- the validity of the lemma /*@ lemma sq_double: \forall real x; x*x - .2 *
x + 0.01 >= 0.; */. It is indeed valid in ACSL, should be proven by WP
whatever the model (since, as Loïc mentioned, it involves only real) , and
(as all lemmas) is completely ignored by Value;

- the validity status of the assert in double x1 = x*x - .2 * x + 0.01; /*@
assert x1 >= 0; */, which is invalid in ACSL, but can be proven by the
Float model of WP.

On Wed, May 4, 2016 at 2:07 PM, Claude Marché <Claude.Marche at inria.fr>
wrote:

>
> Sorry to interfere, but I don't understand the meaning of "wrong in WP"
>
> According to ACSL manual, this lemma is a statement expressed purely in
> mathematical real arithmetic, and as such it is valid. It is indeed
> proved automatically by Z3 4.4.1.
>
> If you want to state a similar property talking about floating-point
> arithmetic, it should be stated differently, typically using a program
>
> void f(double x) {
>   double y = x*x - .2 * x + 0.01;
>   //@ assert y >= 0.0;
> }
>
> But I guess it probably wrong because of rounding, even with a
> precondition like \abs(x) <= 1.0
>
> My two cents,
>
> - Claude
>
> Le 04/05/2016 13:54, Loïc Correnson a écrit :
> >> /*@ lemma sq_double: \forall real x; x*x - .2 * x + 0.01 >= 0.; */
> >
> > This lemma is definitely wrong in WP with Real model (not float there).
> > At least, it is not provable in the forthcoming release of Frama-C.
> > Is there a bug in some existing release?
> >       L.
> >
> >
> > _______________________________________________
> > Frama-c-discuss mailing list
> > Frama-c-discuss at lists.gforge.inria.fr
> > http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss
> >
>
> --
> Claude Marché                          | tel: +33 1 69 15 66 08
> INRIA Saclay - ÃŽle-de-France           |
> Université Paris-sud, Bat. 650         | http://www.lri.fr/~marche/
> F-91405 ORSAY Cedex                    |
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss
>



-- 
Boris
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20160504/62b6d84f/attachment-0001.html>