--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on October 2014 ---
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 -------------- next part -------------- /*@ axiomatic SumAxiomatic { logic integer Sum{L}(unsigned int* a, integer i, integer j) reads a[i], a[j-1]; axiom Sum0: \forall unsigned int* a, int i, j; i > j ==> Sum(a, i, j) == 0; axiom Sum1: \forall unsigned int* a, int i, j, k; 0 <= i < j <= k ==> Sum(a, i, k) == Sum(a, i, j) + Sum(a, j, k); axiom Sum2: \forall unsigned int* a, int i, j; i == j ==> Sum(a, i, j) == a[i]; } */ /*@ requires Sum(a, 0, length) == 10; */ void testSum (unsigned int *a, unsigned int length){ } /* Function used to test Sum */ void functionTest () { unsigned int a[] = {5U, 2U, 3U}; testSum (a, 3U); }