--- layout: fc_discuss_archives title: Message 50 from Frama-C-discuss on April 2010 ---
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