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- andGUI-mode
- Subject: [Frama-c-discuss] Jessie-Plugin inconsistence between batch- andGUI-mode
- From: Pascal.CUOQ at cea.fr (CUOQ Pascal)
- Date: Mon, 18 May 2009 17:12:32 +0200
- References: <42050C88D59E144CA358159FF0E6018B067373@TITAN.first.fraunhofer.de>
>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) Did you use the binary distribution or compile Frama-C yourself? I remember putting the then-current distribution of alt-ergo in the MacOS X binary distribution so that you'd have at least one automatic prover to experiment with. >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). I didn't know this work-around, so thanks for mentioning it. >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 can confirm that this behavior exists, and I even had located the line in the sources of Why where something strange was happening, but I didn't have time to investigate more and have forgotten the details now. I will try to look into it again in June. If you are already working from the source distribution, and willing to look into it yourself, the problem was that the prover processes were not being spawned properly from the Why GUI for some reason that remained to be determined. Pascal
- Follow-Ups:
- [Frama-c-discuss] Jessie-Plugin inconsistence between batch-andGUI-mode
- From: kerstin.hartig at first.fraunhofer.de (Kerstin Hartig)
- [Frama-c-discuss] Jessie-Plugin inconsistence between batch-andGUI-mode
- References:
- [Frama-c-discuss] Jessie-Plugin inconsistence between batch- and GUI-mode
- From: kerstin.hartig at first.fraunhofer.de (Kerstin Hartig)
- [Frama-c-discuss] Jessie-Plugin inconsistence between batch- and GUI-mode
- Prev by Date: [Frama-c-discuss] Jessie-Plugin inconsistence between batch- and GUI-mode
- Next by Date: [Frama-c-discuss] Jessie-Plugin inconsistence between batch-and GUI-mode
- Previous by thread: [Frama-c-discuss] Jessie-Plugin inconsistence between batch-and GUI-mode
- Next by thread: [Frama-c-discuss] Jessie-Plugin inconsistence between batch-andGUI-mode
- Index(es):