Frama-C/WP/ACSL Correct use of \valid on structures

Question

I'm having some doubts on how to correctly use the \valid annotation on structs.

struct someStruct{
    int size1;
    int size2;
    char *str1;
    char *str2;
}

A correct predicate to verify memory safety of the struct would be:

/*@
    predicate validStruct(struct someStruct *p) =
       \valid(p) && 
       \valid(p->str1+(0..((p->size1)-1))) && 
       \valid(p->str2+(0..((p->size2)-1)));
@*/

or

/*@
    predicate validStruct(struct someStruct *p) =
       // 16 bytes: 2 int * 4 bytes + 2 pointers* 4 bytes.
       // Although may depend on implementation and system arch
       \valid(p+(0..15) &&   
       \valid(p->str1+(0..((p->size1)-1))) && 
       \valid(p->str2+(0..((p->size2)-1)));
@*/

The first example assumes that \valid(p) (where p is a pointer to a structure) ensures memory safety on the structure it points to, whereas the second I must specify the range (taking into account the size of the memory fields) manually

Looking at the Stack example in ACSL by Example (page 125). They adopt the first example. However in many places \valid(some_string+(0..strlen(some_string))) is used to ensure memory safety on those specific memory locations.

EDIT:

In response to the answer given. A correct memory safety predicate for this (taken from stdio.h)

struct _IO_file {
    int _IO_fileno;     /* Underlying file descriptor */
    _Bool _IO_eof;      /* End of file flag */
    _Bool _IO_error;    /* Error flag */
};
typedef struct _IO_file FILE;


struct _IO_file_pvt {
    struct _IO_file pub;    /* Data exported to inlines */
    struct _IO_file_pvt *prev, *next;
    char *buf;      /* Buffer */
    char *data;     /* Location of input data in buffer */
    unsigned int ibytes;    /* Input data bytes in buffer */
    unsigned int obytes;    /* Output data bytes in buffer */
    unsigned int bufsiz;    /* Total size of buffer */
    enum _IO_bufmode bufmode; /* Type of buffering */
};

would be, for ex:

/*@

predicate valid_FILE(FILE *f) = 
    \valid(f) && f->_IO_fileno >= 0;

predicate valid_IO_file_pvt(struct _IO_file_pvt *f) = 
    \valid(f)
    // buffer offset
    && f->buf == (char *)f + ((sizeof(*f) + 4*sizeof(void *) - 1)
                                        & ~(4*sizeof(void *) - 1))
    // 16K
    && f->bufsiz == 16384
    && 0 <= f->ibytes <= f->bufsiz
    && 0 <= f->obytes <= f->bufsiz
    && valid_FILE(&(f->pub))
    && (f->next != \null ==> \valid(f->next))
    && (f->prev != \null ==> \valid(f->prev))
    // 16384 + 32 (ungetc_slop)
    && \valid(f->buf+(0..(f->bufsiz+32-1)))
    // data points to address in valid buffer region
    && f->buf <= f->data < (f->buf + f->bufsiz + 32)
;
@*/

Answer 1

Solution 1 is clearly the good one, as it abstracts over the memory layout chosen by your compiler, and by Cil within Frama-C.

Solution 2 is in fact incorrect as written. Your range p+(0..15) must be understood using pointer arithmetics on objects of type struct someStruct, and you are in fact requesting that p points to an area where 16 * sizeof(struct someStruct) bytes are valid.

A correct reformulation of solution 2, for standard memory layouts, would have been

\valid(((char*)p)+(0..15))

In fact, the ACSL reference manual explicitly mentions the following equivalence page 56. (I have removed labels for clarity.)

\valid(p) <==> \valid(((char*)p)+(0..sizeof(*p))

For strings, the cast (char*)p becomes superfluous, as strings are already pointers to char. Thus, writing valid(p+(0..strlen(p)) requires that p points to a memory are where strlen(p)+1 bytes are valid -- but only because p has type char*, and sizeof(char)=1.