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

[Frama-c-discuss] Floating point computations with WP and Jessie



> I tried your code with Frama-C Nitrogen + Jessie 2.30 + Why3 0.72 (just 
> with frama-c -jessie <file.c>) and I am able to prove every VCs using 
> Alt-Ergo/CVC3 and or /Z3. I attached the HTML report produced using 
> why3session.

For Jessie, I just discovered that I can prove all VCs with Alt-Ergo +
CVC3 if I use
frama-c -jessie  r_ges.c
but not if I use
frama-c -jessie -jessie-atp=gui.
The latter fails with Alt-Ergo, CVC3, Simplify, Z3.

I use Frama-C Nitrogen + Jessie 2.30 + Why3 0.72. 

WP with any of the above provers fails to verify the call precondition
for r_ges = r_seq(r1,tmp). I haven't tried the latest WP plugin though.
-- 
Best regards,
Boris