--- layout: fc_discuss_archives title: Message 66 from Frama-C-discuss on November 2013 ---
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>