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



Hi, xiao lei,

I suggest you also to install the Alt-Ergo prover.

It seems that the Alt-Ergo prover is really fast...

-david

On 11 November 2013 02:20, Xiao-lei Cui <x_cui at hotmail.com> wrote:
> Hello David,
>    Thanks for the tip.  I copied the simplify-executable to usr/local/bin/
> as you suggested. And renamed that file to "simplify" as Virgile said in
> another thread. It is working well now. It seems why3 cannot recognize
> namings like Simplify-1.5.5.linux.
>
> cuix at berkhoff:~/Downloads/why3-0.81$ why3config --add-prover simplify
> /usr/local/bin/simplify
> cuix at berkhoff:~/Downloads/why3-0.81$ why3config --detect-proversFound 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 Simplify version 1.5.4 (it is an old version that is less
> tested than the current one).
> Found prover Coq version 8.3pl4, Ok.
> 4 provers detected and 0 provers detected with unsupported version
> Save config to /home/cuix/.why3.conf
>
> cheers,
> xiaolei
>
>> From: dmentre at linux-france.org
>> Date: Fri, 8 Nov 2013 08:31:45 +0100
>> To: frama-c-discuss at lists.gforge.inria.fr
>> Subject: Re: [Frama-c-discuss] adding new provers to why3
>
>>
>> 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