--- layout: fc_discuss_archives title: Message 42 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



On Thu, 2010-07-22 at 09:57 +0200, Julien Signoles wrote:

> 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.

I have a program that generates ~200 VC. Most of them are proved by
Alt-Ergo, but none of them by Simplify. I see the "tool problem" icon on
each VC. I ran why-config and it detected Simplify. I was able to use
Simplify with previous versions of Frama-C/Jessie. Maybe there's a bug
in the toolchain or the makefile. I use Boron on Ubuntu 10.


    prover      version              info   invocation
------------------------------------------------------
  Alt-Ergo         0.91   (not supported)   alt-ergo 
  Simplify        1.5.4                     simplify 
 
-- 
Regards,
Boris