--- layout: fc_discuss_archives title: Message 58 from Frama-C-discuss on August 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] installation on Ubuntu



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++;
  }
}