--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on March 2009 ---
Hello Pascal, On Fri, Feb 27, 2009 at 17:53, Pascal Cuoq <Pascal.Cuoq at cea.fr> wrote: > On Feb 27, 2009, at 2:54 PM, David MENTRE wrote: >> I have successfully compiled Frama-C Lithium on Debian Lenny 5.0 (I >> can give my installation notes if needed). > > We would be happy to have them in order to be able to provide them to > others, or even to fix what is fixable. Please find them in attached file. Sincerely yours, david -------------- next part -------------- Compilation on Debian Lenny 5.0 of Frama-C and some Free provers Note: #: root shell $: regular user shell # aptitude install liblablgtk2-gnome-ocaml-dev \ liblablgtksourceview-ocaml-dev liblablgtk2-ocaml-dev ocaml \ ocaml-native-compilers ocaml-mode \ stow == Alt-Ergo == $ wget http://alt-ergo.lri.fr/http/alt-ergo-0.8.tar.gz $ tar zxf alt-ergo-0.8.tar.gz $ cd alt-ergo-0.8 # aptitude install libocamlgraph-ocaml-dev $ ./configure --prefix=/usr/local/stow/alt-ergo-0.8 $ make $ make install $ mkdir /usr/local/stow/alt-ergo-0.8/bin $ make install $ cd /usr/local/stow/ $ stow alt-ergo-0.8 == CCVC3 == $ wget http://www.cs.nyu.edu/acsys/cvc3/download/1.5/cvc3-1.5.tar.gz $ tar zxf cvc3-1.5.tar.gz $ cd cvc3-1.5 $ ./configure --prefix=/usr/local/stow/cvc3-1.5 --disable-zchaff Apply following patch for GCC 4.3.x: === patch begin === diff -ur /tmp/cvc3-1.5/src/include/command_line_flags.h ./include/command_line_flags.h --- /tmp/cvc3-1.5/src/include/command_line_flags.h 2006-08-09 23:19:30.000000000 +0200 +++ ./include/command_line_flags.h 2009-02-27 13:34:05.000000000 +0100 @@ -24,6 +24,7 @@ #include <sstream> #include <vector> #include <map> +#include <string.h> #include "command_line_exception.h" #include "debug.h" diff -ur /tmp/cvc3-1.5/src/include/memory_manager.h ./include/memory_manager.h --- /tmp/cvc3-1.5/src/include/memory_manager.h 2006-08-09 23:19:30.000000000 +0200 +++ ./include/memory_manager.h 2009-02-27 13:33:06.000000000 +0100 @@ -34,6 +34,8 @@ #ifndef _cvc3__memory_manager_h #define _cvc3__memory_manager_h +#include <malloc.h> + namespace CVC3 { class MemoryManager { diff -ur /tmp/cvc3-1.5/src/util/debug.cpp ./util/debug.cpp --- /tmp/cvc3-1.5/src/util/debug.cpp 2007-06-27 06:35:44.000000000 +0200 +++ ./util/debug.cpp 2009-02-27 13:27:15.000000000 +0100 @@ -22,7 +22,7 @@ #include <fstream> #include "debug.h" - +#include <cstdlib> using namespace std; namespace CVC3 { diff -ur /tmp/cvc3-1.5/src/util/rational-gmp.cpp ./util/rational-gmp.cpp --- /tmp/cvc3-1.5/src/util/rational-gmp.cpp 2007-08-07 22:46:03.000000000 +0200 +++ ./util/rational-gmp.cpp 2009-02-27 13:30:21.000000000 +0100 @@ -24,6 +24,7 @@ #include "compat_hash_set.h" #include "rational.h" +#include <limits.h> #include <sstream> #include <gmp.h> === patch end === $ make $ make install $ cd /usr/local/stow/ $ stow cvc3-1.5 == APRON == $ wget http://apron.cri.ensmp.fr/library/apron-0.9.9.tgz $ tar zxf apron-0.9.9.tgz $ cd apron-0.9.9 # aptitude install libgmp3-dev libmpfr-dev # aptitude install camlidl $ cp Makefile.config.model Makefile.config --- Makefile.config.model 2008-06-09 16:10:50.000000000 +0200 +++ Makefile.config 2009-02-27 09:54:44.000000000 +0100 @@ -29,7 +29,7 @@ # Where to install and to find APRON # ($(APRON_PREFIX)/include, $(APRON_PREFIX)/lib) # -APRON_PREFIX = /usr +APRON_PREFIX = /usr/local/stow/apron-0.9.9 # Where to install and to find MLGMPIDL # ($(MLGMPIDL_PREFIX)/lib) $ make $ make install $ cd /usr/local/stow/ $ stow apron-0.9.9 == Frama-C Lithium == # aptitude install coq coq-doc $ ./configure --prefix=/usr/local/stow/frama-c-lithium-2008-12-01 $ make $ make doc $ make ptests $ make oracles $ make tests Running ptests Command: ./bin/toplevel.opt -val -out -input -deps -journal-disable tests/jessie/minix3_strcpy.c 2>tests/jessie/result/minix3_strcpy.err.log >tests/jessie/result/minix3_strcpy.res.log --- tests/jessie/oracle/minix3_strcpy.err.oracle 2009-02-27 10:23:14.000000000 +0100 +++ tests/jessie/result/minix3_strcpy.err.log 2009-02-27 11:20:22.000000000 +0100 @@ -1,10 +1,10 @@ tests/jessie/minix3_strcpy.c:10:35: error: minix3_include/string.h: No such file or directory -Failed to run: gcc -C -E -I. -o '/tmp/minix3_strcpy.cd7b819.i' 'tests/jessie/minix3_strcpy.c' +Failed to run: gcc -C -E -I. -o '/tmp/minix3_strcpy.c8cbb0f.i' 'tests/jessie/minix3_strcpy.c' You may set the CPP environment variable to select the proper preprocessor command ... or use the -cpp-command program argument. -Error: Cannot find input file /tmp/minix3_strcpy.cd7b819.i (exception Sys_error("/tmp/minix3_strcpy.cd7b819.i: No such file or directory") +Error: Cannot find input file /tmp/minix3_strcpy.c8cbb0f.i (exception Sys_error("/tmp/minix3_strcpy.c8cbb0f.i: No such file or directory") Skipping file "tests/jessie/minix3_strcpy.c" that has errors. Error during linking Your code cannot be parsed. Aborting analysis. % Dispatch finished, waiting for workers to complete % Comparisons finished, waiting for diffs to complete % Diffs finished. Summary: Run = 932 Ok = 1914 of 1915 real 187.61 user 314.73 sys 23.25 $ make install [...] Cannot copy to Coq standard library. Add /usr/local/stow/frama-c-lithium-2008-12-01/share/frama-c/why/coq to Coq include path. $ cd /usr/local/stow/ $ stow frama-c-lithium-2008-12-01/ == Configure Why to recognise installed provers == $ why-config