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



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