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] three newbie questions

Hello,

Boris Hollas a ?crit :
>> Question 3.
>> ------------------
>> Finally, I have installed CVC3 and frama-c recognizes it's there (at
>> lest the GUI does) but all the calls seem to break. Is this just me or
>> is some special switch needed for this one. 

Did you run the tool "why-config" when you installed CVC3? Did it 
success in configuring this ATP?

> 
> The same is true for Simplify. It seems that Alt-Ergo is the only prover
> that is useful for Jessie. I dont't know if this is a bug in Boron.

That's not true. Many users discharge proof obligations using either 
Simplify, Z3, CVC3 or Alt-Ergo. Gappa is also useful for verifying 
floating-points code.

By the way, for many examples, using several ATPs is the only way to 
automatically discharge the whole generated proof obligations.

--
Julien