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