--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on October 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Problem with Jessie and float division



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