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

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.
Alternatively, -cpp-extra-args="-DNULL=0" should do the trick for this
particular case.

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.

Hope this helps,
-- 
E tutto per oggi, a la prossima volta.
Virgile