--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on March 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Frama-C compilation: questions on APRON, test error and missing plugin?



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