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



hi all,
   I am trying to add Simplify-1.5.4 to why3 prover list. 
   I copied Simplify-1.5.4.linux to /usr/sbin/ directory, and run the commands as it follows:

cuix at berkhoff:~/Downloads/why3-0.81$ why3config --add-prover simplify  /usr/sbin/Simplify-1.5.4.linux 
Found prover Simplify version 1.5.4 (it is an old version that is less tested than the current one).
Save config to /home/cuix/.why3.conf

cuix at berkhoff:~/Downloads/why3-0.81$ why3config --detect-provers
Found prover Alt-Ergo version 0.93 (it is an old version that is less tested than the current one).
Found prover CVC3 version 2.4.1, Ok.
Found prover Coq version 8.3pl4, Ok.
3 provers detected and 0 provers detected with unsupported version
Save config to /home/cuix/.why3.conf

   Simplify1.5.4 is not detected by why3 afterwards. Simplify1.5.4 is only shipped as binary. I might missed some commands though.   Any suggestions on fixing this problem?

   thanks!

xiaolei 

 		 	   		  
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131107/b8f15687/attachment.html>