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] Jessie + simplify broken?

  • Subject: [Frama-c-discuss] Jessie + simplify broken?
  • From: Claude.Marche at inria.fr (Claude Marche)
  • Date: Mon, 11 Oct 2010 17:19:53 +0200
  • In-reply-to: <2130910004.130939.1286806628226.JavaMail.root@zmbs1.inria.fr>
  • References: <2130910004.130939.1286806628226.JavaMail.root@zmbs1.inria.fr>
On 10/11/2010 04:17 PM, Boris Hollas wrote:
> Hi,
>
> I just tried to verify some of my programs with Jessie and simplify.
> Although why found simplify, all VCs fail. I see the "tool problem"
> icon.
>
> I compiled everything from the Boron 20100401 distribution on Ubuntu 10
> and installed simplify separately. Does why need special switches
> for ./configure?
>
>
>      prover      version              info   invocation
> ------------------------------------------------------
>    Alt-Ergo         0.92   (not supported)   alt-ergo
>    Simplify        1.5.4                     simplify
>          Z3                      not found
>       Yices                      not found
>        CVC3                      not found
>        CVCL                      not found
>       Gappa                      not found
>         Coq                      not found
>         PVS                      not found
> ------------------------------------------------------
>
>    

The prover Simplify should work. Please also consider adding more of 
them: for me Z3 and CVC3 regularly prove VCs that cannot be proved with 
Alt-Ergo or Simplify

When the "tools" icon shows up for a prover, please select Proof/Debug 
mode in the menu
and replay the same proof by double-clicking on it. Debug info should 
print on the standard error, so that you can figure out what is the problem.

Apart from that, I confirm that the time limit setting of Gwhy should be 
stored permanently between sessions, so you have a specific problem with 
that, e.g. the ~/.gwhyrc, or the equivalent under MSWindows, is not 
writeable.




- Claude

-- 
Claude March?                          | tel: +33 1 72 92 59 69
INRIA Saclay - ?le-de-France           | mobile: +33 6 33 14 57 93
Parc Orsay Universit?                  | fax: +33 1 74 85 42 29
4, rue Jacques Monod - B?timent N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |