Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Using Frama-C as Caduceus

  • Subject: [Frama-c-discuss] Using Frama-C as Caduceus
  • From: diman.soap at gmail.com (Дмитрий Ручкин)
  • Date: Sun, 22 Nov 2009 00:41:11 +0300
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