--- layout: fc_discuss_archives title: Message 63 from Frama-C-discuss on May 2010 ---
On Mon, 2010-05-17 at 14:59 +0200, Julien Signoles wrote: > It works if you insert a space between .. and BUFF_SIZE like this: > > /*@ requires \valid(msg+(0.. BUFF_SIZE)); > Jessie is still unable to verify the postcondition in my example. The relevant VC is integer_of_int8(select(char_P_char_M_msg_1_1, shift(msg, 4))) = 0. I use the Beryllium2 distribution. #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; }