--- layout: fc_discuss_archives title: Message 44 from Frama-C-discuss on May 2009 ---
>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