--- layout: fc_discuss_archives title: Message 9 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



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.
-- 
Best regards,
Boris