--- layout: fc_discuss_archives title: Message 58 from Frama-C-discuss on May 2010 ---
Hello, Boris Hollas a ?crit : > On Sun, 2010-05-16 at 08:51 +0200, Claude Marche wrote: >> See the FAQ or the manual about the --pp-annot option > > Only -pp-annot is recognized as an option, not --pp-annot. pp-annot is > not mentioned in the ACSL reference. -pp-annot is an option of Frama-C. Thus it is described in the Frama-C manual (http://frama-c.com/download/user-manual-Boron-20100401.pdf), not in the ACSL reference. > However, this code still doesn't verify: > > #define BUFF_SIZE 4 > > /*@ requires \valid(msg+(0..BUFF_SIZE)); > ensures msg[BUFF_SIZE] == '\0'; > */ > int setFoo(char* msg) { > msg[BUFF_SIZE] = '\0'; > msg[BUFF_SIZE-1] = '\0'; > return 0; > } > > ~/progs/C/frama-c/test$ frama-c -jessie -pp-annot t.c > [kernel] preprocessing with "gcc -C -E -I. -dD t.c" > t.c:3:[kernel] user error: Error during annotations analysis: unbound > logic variable BUFF_SIZE > [kernel] user error: skipping file "t.c" that has errors. > [kernel] Plugin kernel aborted because of invalid user input(s). It works if you insert a space between .. and BUFF_SIZE like this: /*@ requires \valid(msg+(0.. BUFF_SIZE)); Please feel free to add a feature wish on the BTS in order to support the form without extra space. -- Julien