--- layout: fc_discuss_archives title: Message 82 from Frama-C-discuss on October 2013 ---
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