--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on October 2012 ---
Le lundi 08 octobre 2012 ? 11:05 +0200, Boris Hollas a ?crit : > Hello, > > the code below doesn't verify with Jessie because 0.8 * x > 0.0 can't be > verified. > > #pragma JessieFloatModel(math) > > //@ requires 1 <= x < 10; > void foo(int x) { > double y = 1.0 / (0.8 * x); > } > > > If I add > //@ lemma pos: \forall integer x; x > 0 ==> 0.8 * x > 0.0; > then this lemma can't be verified. This happens with Alt-Ergo and > Simplify and both the why2 and the why3-backend. I don't understand what you think the issue is. Sure, alt-ergo and simplify might no be powerful enough to prove the goal, but how does that make it a problem with jessie and float division? In fact, cvc3, z3, and gappa, succeed in proving your program. Best regards, Guillaume