Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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?

  • Subject: [Frama-c-discuss] Frama-C compilation: questions on APRON, test error and missing plugin?
  • From: dmentre at linux-france.org (David MENTRE)
  • Date: Mon, 2 Mar 2009 09:15:11 +0100
  • In-reply-to: <5BB074F4-9F67-4095-BEF5-4E762AFA1ED1@cea.fr>
  • References: <3d13dcfc0902270554t4f72e405yfc99280aa7a9959c@mail.gmail.com> <5BB074F4-9F67-4095-BEF5-4E762AFA1ED1@cea.fr>
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