--- layout: fc_discuss_archives title: Message 62 from Frama-C-discuss on November 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] adding new provers to why3



Hello,

We have problem with the MAC OS version of simplify.

The simplify binary file was in the /private/var/root/.opam/4.01.0/bin
directory with the other provers (alt-ergo, cvc3, z3, gappa, yices, coq)

The command why3config --detect-provers shows all the provers, but simplify.

As suggested by David we moved the simplify binary file to /usr/local/bin.
The command why3config --add-prover simplify
/usr/local/bin/Simplify-1.5.4.macosx shows the following error:

Error: File /usr/local/bin/Simplify-1.5.4.macosx does not correspond to the
prover id simplify

How to solve it?

Best regards

Nanci Naomi

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Treat the Earth well.  It was not given to you by your parents,
it was loaned to you by your children. (Kenyan proverb)
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~



On Fri, Nov 8, 2013 at 5:31 AM, David MENTRE <dmentre at linux-france.org>wrote:

> Hello Xiao-lei,
>
> 2013/11/8 Xiao-lei Cui <x_cui at hotmail.com>:
> >    I am trying to add Simplify-1.5.4 to why3 prover list.
> >    I copied Simplify-1.5.4.linux to /usr/sbin/ directory, and run the
> > commands as it follows:
>
> The prover should be in your regular user PATH. I doubt /usr/sbin/ is
> in your PATH (it is a special path for administrators). I would put
> the Simplify binary into /usr/local/bin/. The general habit is to
> never put anything outside /usr/local/.
>
> > cuix at berkhoff:~/Downloads/why3-0.81$ why3config --add-prover simplify
> > /usr/sbin/Simplify-1.5.4.linux
> > Found prover Simplify version 1.5.4 (it is an old version that is less
> > tested than the current one).
> > Save config to /home/cuix/.why3.conf
>
> What print "why3 --list-provers" after that step?
>
> > cuix at berkhoff:~/Downloads/why3-0.81$ why3config --detect-provers
> > Found prover Alt-Ergo version 0.93 (it is an old version that is less
> tested
> > than the current one).
> > Found prover CVC3 version 2.4.1, Ok.
> > Found prover Coq version 8.3pl4, Ok.
> > 3 provers detected and 0 provers detected with unsupported version
> > Save config to /home/cuix/.why3.conf
>
> Option --detect-provers re-initialize your /home/cuix/.why3.conf
> configuration file, therefore I guess your previous --add-prover
> configuration is lost.
>
> Best regards,
> david
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131108/b9ded529/attachment.html>