--- layout: fc_discuss_archives title: Message 57 from Frama-C-discuss on May 2010 ---
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. 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). > Anyway, the best solution is to keep using #define I keep telling C-programmers to use const instead of #define because consts contain type information that can be understood by the c-compiler. Therefore, I'd like frama-c to support it. At least gcc issues an error if a const is assigned twice.