--- layout: fc_discuss_archives title: Message 68 from Frama-C-discuss on November 2009 ---
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. -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20091122/5c2f4794/attachment.htm