--- layout: fc_discuss_archives title: Message 33 from Frama-C-discuss on May 2010 ---
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; }