--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on October 2014 ---
Hello, Your axiomatization of Sum is probably inadequate. It should be clear in your mind if Sum(a,i,j) includes also a[j] or not. Your axioms do not seem to be coherent with that respect. I attach a very similar example coming from the test suite of Jessie (available in subdir tests/c of Why distribution). The two lemmas sum3 and sum_footprint need some induction reasoning to be proved, so in the current state of technology in Frama-C + either Jessie or WP plugins, an interactive prover like Coq is needed to prove them. But you can safely admit them for the rest of the code. Hope this helps, - Claude Le 02/10/2014 18:26, Sebastian a ?crit : > Hi, > Thank you very much for your previous reply. > I followed your instructions and I tried to implement the axiomatic Sum. > I am using "Frama-C Neon-20140301" with Alt-Ergo prover on Ubuntu 14.04. > I have tried to test it with a simple example but my axiomatic Sum > doesn't work and I am not able to find the error. > I have made a "functionTest" function that calls "testSum" function with > array elements that satisfy the requirements of "testSum" requires > clause, but the prover was not able to prove it. > I attached the axiomatic Sum definition, the "testSum" function and the > "functionTest" function. > Could you please suggest how I can proceed with finding a solution to > this problem? > > Thank you very much. > Best regards, > Sebastian > > > > Il 29/09/14 14:12, Lo?c Correnson ha scritto: >> Hi, >> \sum and \lambda are unsupported with WP. >> Instead, you can axiomatize your sum or use an inductive predicate. >> >> See >> http://www.fokus.fraunhofer.de/de/sqc/_download_sqc/ACSL-by-Example.pdf >> ? 3.8.1 is a good hint. >> L. >> >> >> >> Le 29 sept. 2014 ? 10:00, Sebastian <sdavrieux at gmail.com> a ?crit : >> >>> Good morning, >>> I'm trying to do the average without overflow, however I'm not >>> able to check an assert that contains \sum annotation. >>> So I decided to make a simpler function that only uses \sum, but it >>> doesn't work. What can I do to solve the problem? >>> >>> Best regards, >>> Sebastian >>> <testSum.c>_______________________________________________ >>> Frama-c-discuss mailing list >>> Frama-c-discuss at lists.gforge.inria.fr >>> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss >> _______________________________________________ >> Frama-c-discuss mailing list >> Frama-c-discuss at lists.gforge.inria.fr >> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | Universit? Paris-sud, Bat. 650 | http://www.lri.fr/~marche/ F-91405 ORSAY Cedex | -------------- section suivante -------------- Une pi?ce jointe autre que texte a ?t? nettoy?e... Nom: sum_array.c Type: text/x-csrc Taille: 3796 octets Desc: non disponible URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20141003/4c89ea7a/attachment.c>