--- layout: fc_discuss_archives title: Message 79 from Frama-C-discuss on August 2013 ---
Since I didn't see anyone mention it, I thought I'd add that Opam<http://opam.ocamlpro.com/>, the OCaml Package Manager is quite handy. If I recall correctly I had some trouble using it to install Frama-C itself, and found it easier to just compile it by hand. But for many of its dependencies and optional add-ons (alt-ergo, why3, coq, lablgtk, etc), it worked like a charm. J.A. On 26 August 2013 13:51, Stephen Siegel <siegel at udel.edu> wrote: > I'm just posting here what I did to install these tools on a fresh Ubuntu > system in case it is helpful to others... > > > To install current Frama-C with Jessie, Why, and Why3 on Ubuntu: > > sudo apt-get install \ > ocaml \ > ocaml-native-compilers \ > libocamlgraph-ocaml-dev \ > libzarith-ocaml-dev \ > otags \ > graphviz \ > liblablgtk2-gnome-ocaml-dev \ > liblablgtksourceview2-ocaml-dev \ > rubber \ > sqlite3 \ > coq \ > alt-ergo > > In /usr/local/lib/ocaml/3.12.1 execute: > sudo ln -s /usr/lib/ocaml/zarith > > Download ltl2ba from > http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/download.php > Unpack, compile with just "make" and move executable ltl2ba into your path > (e.g., /usr/local/bin). > > Download and unpack: > http://frama-c.com/download/frama-c-Fluorine-20130601.tar.gz > http://why3.lri.fr/download/why3-0.81.tar.gz > http://why.lri.fr/download/why-2.33.tar.gz > In the last case, edit configure, replacing each occurrence of 20130401 > with 20130601 > In each case, build and install as usual: > ./configure > make > sudo make install > Configure Why3 by executing why3config. It should be able to find at > least Alt-Ergo. > Test on this example copy.c by executing > frama-c -jessie copy.c > and selecting Alt-Ergo (for example) to discharge all VCs. They should > all check. > > Contents of copy.c: > > /* Array copy: copies elements of one array into another. > * Author: Stephen F. Siegel > * VCs can be discharged by Alt-Ergo or CVC3. > */ > > /*@ > @ requires n>=0 && \valid(a+(0..n-1)) && \valid(b+(0..n-1)) ; > @ ensures \forall integer i ; 0 <= i < n ==> a[i] == b[i] ; > @ assigns b[0..n-1] ; > @*/ > void copy(int n, double a[], double b[]) { > int i = 0; > > /*@ > @ loop invariant 0<=i<=n; > @ loop invariant \forall integer j ; 0<=j<i ==> b[j] == a[j] ; > @ loop variant n - i ; > @*/ > while (i < n) { > b[i] = a[i]; > i++; > } > } > > > > _______________________________________________ > 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/20130830/e03f5b64/attachment.html>