--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on February 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,

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