--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on October 2014 ---
Thank you very much! It works perfectly! Now I'm able to solve Average Problem and it seems to work. Best regards, Sebastian Il 03/10/14 09:51, Claude March? ha scritto: > > > To make this example more visible, I've just add it to Toccata's gallery: > > http://toccata.lri.fr/gallery/sum_array.en.html > > you will see there which prover I used to prove the VCs. You may also > have a look at the Coq proofs of the two lemmas if you want. > > Last but not least, while doing that I realized that my own > axiomatization was not quite adequate either, so please look at the > web page above for a better one. > > Notice that this gallery contains some more examples proved using > Frama-C/Jessie at > > http://toccata.lri.fr/gallery/jessieplugin.en.html > > - Claude > > Le 03/10/2014 08:52, Claude March? a ?crit : >> >> 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 >>> >> >> >> >> _______________________________________________ >> 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 >> >