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