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