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