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] Using Frama-C as Caduceus

As a first step, to recover a file closer to the Caduceus one, you should
select the unbound model for integers, and disable separation analysis.

#pragma JessieIntegerModel(exact)
#pragma SeparationPolicy(None)

- Claude

Claude Marche wrote:
> Hopefully, the jessie plugin of Frama-C provides some improvement over 
> Caduceus. Clearly, there is no chance that you get exactly the same
> PVS file.
>
> Now, I understand that you think the PVS file obtained via 
> Frama-C/Jessie/Why is significantly more complex than the one you got 
> from Caduceus/Why. Indeed, we are willing to improve Frama-C/Jessie 
> output if you request for precise feature wishes.
>
> - Claude
>
> ??????? ?????? wrote:
>   
>> Hello everyone!
>>
>> I moved from Caduceus to Frama-C recently, and haven't yet learned all 
>> the possibilities of Frama-C. My question may sound silly, but I 
>> really can't make Frama-C work like I need.
>>
>> Imagine that I have simple example (with error in loop invariant): 
>> http://pastebin.org/55876 I ran it through Caduceus and got Why-code 
>> (http://pastebin.org/55878). Then I can make pretty simple PVS theory 
>> (http://pastebin.org/55898) and work with PVS lemmas.
>>
>> And now with Frama-C. I rewrote the comments in ACSL (which resulted 
>> in http://pastebin.org/55879) and ran it through Frama-C. To be exact, 
>> I used "frama-c -jessie -jessie-atp goals", which, as I understood, is 
>> somehow an equivalent to "caduceus" command. And that's what I get at 
>> .why file: http://pastebin.org/55882 That's different and will result 
>> in different PVS theory (http://pastebin.org/55901).
>>
>> So, is there any way of getting "Caduceus-like" Why-code and 
>> corresponding PVS theory using Frama-C?
>>
>> Thanks in advance.
>>
>> Dmitry.
>> ------------------------------------------------------------------------
>>
>> _______________________________________________
>> 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           | mobile: +33 6 33 14 57 93 
Parc Orsay Universit?                  | fax: +33 1 74 85 42 29   
4, rue Jacques Monod - B?timent N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |