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



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