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



I can't test it for the moment, but my guess is that Jessie does not 
consider BUFF_SIZE as a true constant. I'm not sure if the C norm 
guarantees that it cannot change. To check if it is the problem, you can 
try adding BUFF_SIZE == 4 as a precondition.

Anyway, the best solution is to keep using #define

Expanding the macro definitions in annotations is not a task of Jessie 
but of Frama-C kernel.
See the FAQ or the manual about the --pp-annot option

- Claude

Boris Hollas wrote:
> Jessie is unable to verify the following code for reasons that I don't
> understand. I get "?" for postcondition, pointer dereferencing,
> arithmetic overflow. Using #define instead of const doesn't work either
> because it seems that Jessie doesn't read #defines.
>
>
> const int 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;
> }
>
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>