--- layout: fc_discuss_archives title: Message 57 from Frama-C-discuss on May 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Small function on buffer doesn't verify



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.