--- layout: fc_discuss_archives title: Message 73 from Frama-C-discuss on November 2009 ---
[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                    |