--- layout: fc_discuss_archives title: Message 66 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 Guillaume,

We added the option as suggested to the command:
why3config --debug autodetect --add-prover simplify /usr/local/bin/simplify

And it showed the following error message:
Run : (/usr/local/bin/simplify -version) > /tmp/outeedda4 2>&1
command '/usr/local/bin/simplify -version' failed
Error: File /usr/local/bin/simplify does not correspond to the prover id
simplify

When running the command:
/usr/local/bin/simplify -version

it showed the message:
sh: /usr/local/bin/simplify: Bad CPU type in executable

I think that the binary file is corrupted.
Is there other version to MAC OS?

In the linux, the binary file works.

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:49 AM, Guillaume Melquiond <
guillaume.melquiond at inria.fr> wrote:

> On 08/11/2013 13:26, Virgile Prevosto 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,
>>
>
> With option "--add-prover", why3 does not care about the name of the
> executable; it only checks that the program has the expected version
> string. (Just to be sure, I renamed one of my provers 'toto' and it worked
> fine.)
>
> You can pass option "--debug autodetect" in addition to "--add-prover" in
> order to see which part of the detection failed.
>
> Best regards,
>
> Guillaume
>
>
> _______________________________________________
> 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/d95715cb/attachment-0001.html>