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

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
>>
>