--- layout: fc_discuss_archives title: Message 37 from Frama-C-discuss on February 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] [Why-discuss] Generate Coq file using Frama-c / Why



Hello,

> Anyway, I will try to follow the instructions from Pascal.

If you mean "install a version of Why where Coq V8 has been detected,  
compiled with 64-bit OCaml 3.11.2 for Snow Leopard, your best bet to  
avoid interference between the two is to overwrite the Why provided in  
the Frama-C binary package.

Compile with:
export PATH=/usr/local/Frama-C_Be/bin:$PATH
./configure --prefix=/usr/local/Frama-C_Be/
make
sudo make install

Note that there is an OCaml compiler in the Frama-C package, but it  
was compiled for Leopard and I don't recommend using it. It is better  
to use a Snow Leopard OCaml compiler.

Pascal