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: Fri, 27 Feb 2009 14:54:52 +0100
Hello,

I have successfully compiled Frama-C Lithium on Debian Lenny 5.0 (I
can give my installation notes if needed). I have a few questions and
remarks regarding the compilation process:

* APRON is not mentioned explicitly in the INSTALL. I stumble upon it
after reading a configure warning. You should probably include a
pointer to http://apron.cri.ensmp.fr/library/ in the INSTALL file.

* In APRON installation process, it is said one can optionally use
Parma Polyhedra Library (PPL). As it was necessary to patch PPL, I
have not bothered with it. Is there any use of it within Frama-C
context?

* During configure, two plugins are missing, "miel" and "wp". I
haven't found any reference to them on Frama-C web site or through
Google. Are there experimental plugins, non-public ones or simply
available somewhere?

* After doing a "make tests", there was one error:
"""
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
"""

* I'm looking for Free Software / Open Source automatic provers that
could be used in conjunction with Jessie plugin / Why. From Frama-C
web site, I have successfully compiled and installed Alt-Ergo and CVC3
(without zchaff). Are there any other provers available?

Are excluded:
 * Simplify: binary only;
 * Yices: binary only, non-commercial;
 * Z3: non-commercial.

Sincerely yours,
david