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'
