--- layout: fc_discuss_archives title: Message 50 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



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