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?

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.

> 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.

We will.

Note that at this time APRON is used only by the Jessie plug-in
for trying to find invariants automatically on functions that make
use of common C string manipulation idioms.

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

Another polyhedra library, NewPolka, is always compiled in APRON,
so don't worry about it.

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

They are experimental and therefore not distributed at this point.
We will try to make this clearer in the output of configure.

> * 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
> """

The difference that you see is caused by the name of a temporary
file which changes from execution to execution. The real problem is
that this name shows in the log because Frama-C fails to
run on this particular example. A file, minix3_include/string.h, seems
to be missing. This may be an omission on our part. Again, do not
worry about it, it does not imply that Frama-C is incorrect or
mis-installed on your computer.

> * I'm looking for Free Software / Open Source automatic provers [...]
>  Are there any other provers available?

The page at http://why.lri.fr/ lists haRVey.

I have heard that sources for Simplify were still floating around,
again please follow the links from the Why webpage and see if
what you find is acceptable to you (shortcut: you'll probably end up at
http://secure.ucd.ie/products/opensource/ESCJava2/license.html
at some point).
Although Zenon is not listed on the Why webpage, I think that there
is a good chance that it is supported:
http://focal.inria.fr/zenon/

Regards,

Pascal