Hello all,
I have problem with this error:
\singly_linked_list_test_vcc.c(28,2) : error VC9502: Call 'stack_free(&list)' did not verify.
\Vcc\Headers\Vcc3Prelude.bpl(1529,3) : error VC9599: (related information) Precondition: 'the extent of the object being reclaimed is mutable'.
This is a part of my code, contained in header file, where I am using data structures like this:
typedef _(dynamic_owns) struct tElem {
T data;
struct tElem *Nextptr;
_(invariant \mine(Nextptr))
} tElem;
typedef _(dynamic_owns) struct {
tElem *First;
tElem *Last;
_(ghost size_t size;)
_(ghost \bool val[int];)
_(ghost tElem *find[int];)
_(ghost int elements[size_t];)
_(ghost \natural idx[tElem *])
_(invariant size >= 0)
_(invariant First == NULL ==> size == 0)
_(invariant First != NULL ==> size > 0)
_(invariant First != NULL ==> \mine(First) && \wrapped(First))
_(invariant Last != NULL ==> \mine(Last) && \wrapped(Last))
_(invariant \forall tElem *x; \mine(x) && x>Nextptr ==> \mine(x>Nextptr))
_(invariant \forall tElem *x; \mine(x) ==> val[x>data])
_(invariant \forall int v; val[v] ==> \mine(find[v]) && find[v]>data == v)
_(invariant First ==> idx[First] == 0 && idx[Last] == size  1)
_(invariant \forall tElem *x, *y; \mine(x) && \mine(y) ==>
First
&& (idx[x] == 0 ==> x == First)
&& (x>Nextptr ==> idx[x>Nextptr] == idx[x] + 1)
&& (idx[y] == idx[x] + 1 ==> y == x>Nextptr)
&& (idx[y] > idx[x] ==> x>Nextptr)
&& (y>Nextptr == NULL ==> y == Last)
)
} tList;
Then in same .h file I have initialization function like this:
void InitList (tList *L)
_(requires \extent_mutable(L))
_(writes \extent(L))
_(ensures L>First == NULL)
_(ensures L>Last == NULL)
_(ensures \wrapped(L) && L>val == \lambda int a; \false)
_(ensures L>size == 0)
_(decreases 0)
{
L>First = NULL;
L>Last = NULL;
_(ghost {
L>\owns = {};
L>size = 0;
L>val = (\lambda int a; \false);
_(ghost L>find = (\lambda int a; (tElem *) NULL))
})
_(wrap L)
}
Then in .c file I want to call function InitList() like this:
void test_01(void)
{
tList list;
InitList(&list);
}
But I got this error, can anyone help me with what caused the error.
Thanks a lot.
