Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Average Problem

  • Subject: [Frama-c-discuss] Average Problem
  • From: Claude.Marche at inria.fr (Claude Marché)
  • Date: Fri, 03 Oct 2014 08:52:14 +0200
  • In-reply-to: <542D7CC1.1060606@gmail.com>
  • References: <54291115.1080500@gmail.com> <542911A4.5010109@gmail.com> <043C3AA7-9E35-4C73-9AB2-07B8D812B84F@cea.fr> <542D7CC1.1060606@gmail.com>
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>