--- layout: fc_discuss_archives title: Message 64 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 Virgile,

I have just tried it, but it did not work. It showed the same error message.

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 10:26 AM, Virgile Prevosto
<virgile.prevosto at m4x.org>wrote:

> Hello,
>
> 2013/11/8 Nanci Naomi <nnarai at gmail.com>:
>
> > 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
>
> Rename the file to Simplify or simplify. If I'm not mistaken, why3
> does not search for an executable whose name begins with Simplify, but
> is exactly Simplify,
>
> Best regards,
> --
> E tutto per oggi, a la prossima volta
> Virgile
>
> _______________________________________________
> 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/6c735615/attachment.html>