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

> Just a guess : if you write 2.0 and 1.0 instead of 2 and 1 does it work?
> If yes, then it is an issue with conversion from integer to real.

No it is not.
The generated lemma for Why3 is:

(* ---------------------------------------------------------- *)
(* --- Global Definitions                                 --- *)
(* ---------------------------------------------------------- *)
theory Axiomatic
  
use import bool.Bool
use import int.Int
use import int.ComputerDivision
use import real.RealInfix
use import Qed.Qed
use import int.Abs as IAbs
use import map.Map

lemma Q_POS: forall x : real. (2.0e0 *. x) <=. (1.0e0 +. (x *. x))

end

None of CVC4, Z3 and Alt-Ergo is able to prove it — but in Coq it is.
	L.