--- layout: fc_discuss_archives title: Message 40 from Frama-C-discuss on July 2010 ---
[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