--- layout: fc_discuss_archives title: Message 103 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 also installed Simplify under Nanci Naomi's instructions:

http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2013-November/004083.html

"why3config --debug autodetect --add-prover simplify /usr/local/bin/simplify"

I used it to verify some of those examples in this website:
http://proval.lri.fr/gallery/jessieplugin.en.html

It seems simplify works fine for me.

What kind of code you try to prove? What happened if you  increase the
value of timeout  to a bigger one?

Regards,

-david

On 15 November 2013 01:52, Xiao-lei Cui <x_cui at hotmail.com> wrote:
> Hi David,
> I have alt-ergo prover installed (version 0.93). It is fast and efficient.
> I also installed Simplify-1.5.4 recently, but it is timed out for almost
> every proof obligation. Eventhough I set the timeout limit to 10 seconds,
> still it cannot prove anything.
>
> Not sure what went wrong:)
>
> cheers,
>
> xiaolei
>
>
>
>> From: abiao.yang at gmail.com
>> Date: Mon, 11 Nov 2013 10:03:12 +0000
>
>> To: frama-c-discuss at lists.gforge.inria.fr
>> Subject: Re: [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
>>
>> _______________________________________________
>> 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
>
> _______________________________________________
> 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