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

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