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] Jessie-Plugin inconsistence between batch- and GUI-mode

  • Subject: [Frama-c-discuss] Jessie-Plugin inconsistence between batch- and GUI-mode
  • From: kerstin.hartig at first.fraunhofer.de (Kerstin Hartig)
  • Date: Mon, 18 May 2009 16:57:32 +0200
Hello everyone,

I am facing some problems running Jessie and I as I didn't find any
advices for this problem in the archive I hope maybe someone here has
the answer and can help me to solve it.

I have installed Frama-C on MacOS X, I additionally installed some
provers  (alt-ergo, cvc3 and yices) and ran why-config. (everything was
fine)
I've got a piece of code that I want the provers to run on.


If I try to run it in batch mode:
frama-c -jessie-analysis -jessie-atp alt-ergo file.c
everything seems to work fine, alt-ergo finds 14 valid proof obligations
(0 invalid/unknown/timeout/failure).


If I try to run it in gui-mode:
frama-c -jessie-analysis -jessie-gui file.c
the results of alt-ergo in the GWhy-Interface are not consistent with
the batch-mode results, actually there are no results. Clicking on the
prover just makes it run fast through the PO's, but no results. (I could
post a screenshot of this if required)
I tried the different provers and different source files (also the
tutorial). I always get the same problem. 

Does anyone have any suggestions how to solve this?

Thanks,

Kerstin

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090518/91dc480d/attachment.htm