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



On 08.10.2012 11:36, Guillaume Melquiond wrote:
> that make it a problem with jessie and float division? In fact, cvc3,
> z3, and gappa, succeed in proving your program.

Indeed, CVC3 proves the code, even without the lemma, but only if I use 
the why3-backend. However, Z3 runs in a time out.

I don't understand why because Z3 and Simplify generally perform well on 
arithmetics.

I haven't installed gappa. I read 
http://gappa.gforge.inria.fr/doc/ch06s01.html, but I don't know how to 
install it in a way so that why can use it. In what order do gappa, 
jessie, why3 have to be compiled and installed? Does gappa work with 
why3? Is gappa independent of Frama-C?

-- 
Best regards,
Boris