--- layout: fc_discuss_archives title: Message 81 from Frama-C-discuss on October 2013 ---
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? Kind regards, Alessio Iotti 2013/10/17 Guillaume Melquiond <guillaume.melquiond at inria.fr> > On 17/10/2013 10:13, Alessio Iotti wrote: > >> Dear All, i am moving the first steps with Frama-C, following the >> excellent tutorial "ACSL By Example". >> I have encountered a problem trying to replicate the count algorithm >> experiment. The attached file, >> taken literally from "ACSL By Example", illustrates the problem in >> comments beginning with "/***". >> > > That is somehow fortunate that Fluorine fails at proving it, and that is > kind of scary that Nitrogen (even partly) succeeded, because what you are > trying to prove is plain wrong! > > Axiom count2 should have been written > > \forall int *a, v, integer i ; > (a[i] != v ==> Count(a, v, i, i+1) == 0) && > (a[i] == v ==> Count(a, v, i, i+1) == 1); > > Once changed, all the proof obligations are verified. > > Best regards, > > Guillaume > -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131022/e0a79e5a/attachment.html> -------------- next part -------------- A non-text attachment was scrubbed... Name: count_axiom.c Type: text/x-csrc Size: 1481 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131022/e0a79e5a/attachment.c>