--- layout: fc_discuss_archives title: Message 25 from Frama-C-discuss on July 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Compiling Frama-C and why



Hi,

Le 10/07/2012 17:14, Jens Gerlach a ?crit :
>
> Hier sind einige Notizen zur Installation von
> Frama-C/WP, Frama-C/Jessie (why2 und why3)
> f?r Linux.
>
> Erst einmal folgende Sachen installieren:
>
> 	sudo apt-get install ocaml ocaml-native-compilers graphviz \
>               liblablgtksourceview2-ocaml-dev liblablgtk2-gnome-ocaml-dev
>
> Ausserdem habe ich folgende Pakete ueber Synaptic installiert:
> 	alt-ergo, cvc3, ocamlgraph, coq

So far so good, although I'm not the synpatic package are very 
up-to-date, I would recommend to install up-to-date version of provers

> Mit Nitrogen beginnen und Frama-C/WP installieren lassen.
>
> 	cd frama-c-Nitrogen-20111001/
> 	./configure
> 	make
> 	sudo make install
>
> Upgrade zu WP 0.5 (es reicht vermutlich auch, wenn man das nur am Ende macht)
>
> 	cd wp-0.5-Nitrogen-20111001
> 	autoconf
> 	./configure
> 	make depend
> 	make
> 	sudo make install
>
> Frama-C/Jessie ueber why-2.30 installieren
>
> 	cd why-2.30/
> 	./configure
> 	make
> 	sudo make install
>
> Noch einmal Frama-C installieren.
>
> 	cd frama-c-Nitrogen-20111001/
> 	./configure
> 	make
> 	sudo make install

I'm very surprised that the Jessie plugin will still work if you 
reinstall Frama-C a second time. A dynamic load error should occur...


> Why3 installieren
>
> 	cd why3-0.71/
> 	./configure
> 	make
> 	sudo make install


Ach das ist nicht gut ! especially the next release of Why2 will require 
Why3 to be installed before.

The right order should be

1) compile and install why3, configure it (why-config) and hopefully 
check the installation on examples/hello_proof.why

2) compile and install Frama-C. If WP is included and complains about 
why missing, it is probably not a problem (see Virgile answer)

3) compile Why2.30 that include the Jessie plugin, that requires both 
Why3 and Frama-C installed

Hopefully the future version of WP plugin will use only Why3 anyway, so 
that should work without problem.

If I am wrong, then a bug should be reported.

- Claude

-- 
Claude March?                          | tel: +33 1 72 92 59 69
INRIA Saclay - ?le-de-France           |
Universit? Paris-sud, Bat. 650         | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex                    |