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



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;
}