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