--- layout: fc_discuss_archives title: Message 58 from Frama-C-discuss on August 2013 ---
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++; } }