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