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] Provers versions

  • Subject: [Frama-c-discuss] Provers versions
  • From: rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)
  • Date: Mon, 30 Sep 2013 16:03:51 -0300
  • In-reply-to: <52467C25.5000400@inria.fr>
  • References: <CAEtoXR0u7Hpu+tf2-95pe=CazhktApzz02vMdJM0Tr3pcNofLA@mail.gmail.com> <52467C25.5000400@inria.fr>
Thank you for your reply.

We did the changes in the wh3.conf file.

Best regards,
Nanci, Rovedy, Luciana


2013/9/28 Claude Marche <Claude.Marche at inria.fr>

>
> Hello,
>
> All versions of provers below were released after the Why 0.81 release,
> so we did not have the opportunity to test them.
>
> In general they are supported in the dev version of Why, and thus will
> be supported in the next release. But there is no unique answer on
> whether they are OK with 0.81 or not, see below.
>
> On 09/27/2013 07:21 PM, Rovedy Aparecida Busquim e Silva wrote:
> > Warning: prover Z3 version 4.3.2 is not known to be supported, use it at
> > your own risk!
>
> This one is OK with 0.81, as far as I know.
>
> > Warning: prover Gappa version 1.0.0 is not known to be supported, use it
> at
> > your own risk!
>
> OK too.
>
> > Warning: prover Coq version 8.4pl2 is not known to be supported, use it
> at
> > your own risk!
>
> should be OK too.
>
> > Warning: prover Alt-Ergo version 0.95.2 is not known to be supported, use
> > it at your own risk!
>
> There is a small unintended change in the -timelimit option of Alt-Ergo
> 0.95.2, that prevents Why3 to stop Alt-Ergo after the user given time
> limit. This can be fixed by editing the [alt-ergo] record of the
> generated why3.conf and replace the '%T' argument of why3cpulimit to '%t'
>
> > Warning: prover Yices version 2.1.0. is not known to be supported, use it
> > at your own risk!
>
> Yices 2 does not support quantifiers AFAIK, so you will not get any
> interesting proofs from Why3. You should stick to the last Yices 1 version
>
> - Claude
>
> _______________________________________________
> 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/20130930/335b1a3b/attachment.html>