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

[Frama-c-discuss] Problems with Nitrogen/Fluorine



Hello,

2013/10/22 Alessio Iotti <alle.iot at gmail.com>:
> Thank you for the response. I modified the program, i used the Jessie plugin
> instead of the WP plugin and it works.
> However "ACSL By Example" refers to Frama-C Nitrogen 20111001 used with the
> WP plugin, as i tried originally.
> Which can be the causes of this discrepancy between my version (in
> attachment) and the one on the paper?
>

I don't have a Nitrogen version at hand, but if I launch Fluorine's WP
on your second version of the file, in which the Count2 axiom is
correctly parenthesized, as mentioned by Guillaume and as it is the
case in the ACSL by example document, everything gets discharged.  On
your original version, though, a proof obligation is missing, since
Count2 is wrong (&& binds more tightly than ==>, so that A ==> B && C
==> D reads as A ==> (B&&C) ==> D).

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile