This project is read-only.

Problem in writing into subfield of a nested structure

Dec 13, 2013 at 2: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>

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

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

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

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

_(ghost Lists *lsts )

_(dynamic_owns)
struct State{
unsigned value;

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


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

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 11:06 AM
Edited Dec 14, 2013 at 11: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.