Problem in writing into subfield of a nested structure

Dec 13, 2013 at 1:33 PM
I would like to use VCC for checking the validity of mathematical model specifying a software system. The ghost maps are used to specify the mathematical objects. It involves nested structures and I am unable to specify the contract (write clause) for updating the subfield of an element in an array of structures.

Following is the VCC model

include <vcc.h>

include <limits.h>

typedef struct iseq{
_(ghost int elements[unsigned] )
unsigned dummy;

_(invariant \forall unsigned i,j;
        ( i!=j )   ==> ( elements[i] != elements[j] ) 
} iSeq;

typedef struct lists{
_(ghost iSeq seqGroup[10] )
_(ghost iSeq  seq )
unsigned dummy;

_(invariant \forall unsigned i;
        ( i < 10 )  ==> \mine(&seqGroup[i])
_(invariant \mine(&seq)  )

_(ghost Lists *lsts )

struct State{
unsigned value;

_(invariant \mine(\embedding(&lsts) ) )
_(invariant \mine(lsts) )
_(invariant ( value < 100 ) )

void update()
_(requires \wrapped(&state) )
_(writes &state )
_(ensures \wrapped(&state) )
//_(ensures \false )
_(unwrap &state )
_(unwrap lsts )
_(ghost lsts->seqGroup[0].elements = 
    \lambda unsigned i;
        ( i < 100 ) ? lsts->seqGroup[0].elements[i] : INT_MAX
_(wrap lsts )
_(wrap &state )

VCC gives the error message "Assertion 'lsts->seqGroup[0].elements is writable' did not verify." .
Can someone tell me how can I specify the write clause for updating the field such as 'lsts->seqGroup[0].elements'
Dec 14, 2013 at 10:06 AM
Edited Dec 14, 2013 at 10:07 AM
I could solve the above problem by owning all such compound objects in a single structure.
Then one can 'unwrap' and 'wrap' as when she need to write into a subfield/component.

But in this case the invariants on such subcomponents need to be specified in the
single structure owning these components.

It would be nice if there exist a way of specifying the invariants in the
respective structures as it makes the model more readable.