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



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