--- layout: fc_discuss_archives title: Message 72 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



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                    |