Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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