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

>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