--- layout: fc_discuss_archives title: Message 58 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



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