--- layout: fc_discuss_archives title: Message 32 from Frama-C-discuss on October 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Jessie + simplify broken?



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                    |