--- layout: fc_discuss_archives title: Message 79 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



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>