--- layout: fc_discuss_archives title: Message 52 from Frama-C-discuss on April 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] why-2.24 install question



On Wed, 21 Apr 2010, Virgile Prevosto wrote:

> Le mer. 21 avril 2010 10:58:41 CEST,
> Nicholas Mc Guire <der.herr at hofr.at> a ?crit :
> 
> > /*@ requires \valid(i) && \valid(j);
> >   @ requires r == NULL || \valid(r);
> >   @ assigns *r;
> >   @ behavior zero:
> >   @   assumes r == NULL;
> >   @   assigns \nothing;
> >   @   ensures \result ==  -1;
> >   @ behavior normal:
> >   @   assumes \valid(r);
> >   @   assigns *r;
> >   @   ensures *r == ((*i < *j) ? *j : *i);
> >   @   ensures \result == 0;
> >   @*/
> > int max(int *r, int* i, int* j) {
> >         if (!r) return -1;
> >         *r = (*i < *j) ? *j : *i;
> >         return 0;
> > }
> > 
> > ...
> > max1.c:2:[kernel] user error: Error during annotations analysis: unbound logic variable NULL
> > ...
> > 
> There are 2 points here:
> NULL is supposed to be a macro, but the jessie tutorial does not
> include stddef.h, which is supposed to define it. #include "stddef.h"
> in max1.c should do the trick, together with the option
> -cpp-extra-args="-I`frama-c -print-path`/libc", to retrieve the header
> provided by frama-c.

hmm..

rand1:~/example#  frama-c.byte -cpp-extra-args=" -I /usr/local/share/frama-c/libc/ " -pp-annot -jessie -jessie-atp alt-ergo max1.c
[kernel] preprocessing with "gcc -C -E -I.  -I /usr/local/share/frama-c/libc/  -dD max1.c"
max1.c:2:[kernel] user error: Error during annotations analysis: unbound logic variable NULL
[kernel] user error: skipping file "max1.c" that has errors.
[kernel] Frama-C aborted because of an invalid user input.
AthlongII2X_250_1:~/example# grep NULL  /usr/local/share/frama-c/libc/*
...
/usr/local/share/frama-c/libc/__fc_define_null.h:#define NULL ((void*)0)
...

..so this should actually owrk (?)


> Alternatively, -cpp-extra-args="-DNULL=0" should do the trick for this
> particular case.

while this seems fine:

rand1:~/example#  frama-c.byte -cpp-extra-args="-DNULL=0" -pp-annot
-jessie -jessie-atp alt-ergo max1.c
[kernel] preprocessing with "gcc -C -E -I. -DNULL=0 -dD max1.c"
[jessie] Starting Jessie translation
[jessie] Producing Jessie files in subdir max1.jessie
...


> 
> The second point is what Claude said: C pre-processors do not
> traverse comment, which is what an annotation is for what cpp is
> concerned. Normally, you would need to add the option -pp-annot to
> frama-c's command-line to force the pre-processing of annotation. Note
> that this can be done only when the pre-processor is cpp/gcc. This is
> why -pp-annot is not the default. However, If I recall correctly, the
> Jessie plug-in already sets that automatically for you (without much
> regard of what your pre-processor looks like, but that's another
> story).
> 
> Anyway, using the \null built-in of ACSL is definitely the recommended
> way.
>

that works fine.

thx!
hofrat