Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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                    |