This project is read-only.

error VC9502: Call 'stack_free()

Apr 15, 2013 at 3:20 PM
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.
Apr 21, 2013 at 11:07 AM
Hi,

when a function returns, VCC adds a check that (non-primitive) local variables have a mutable extent, which allows their memory to be freed when the stack frame of the function is destroyed. In your case, VCC can't prove that the 'list' variable doesn't leak, leading to the crypting warning about 'stack_free'. Either, you need to pass in an appropriate pointer in your test_01() function, or you destroy the list before your function returns.

Hope this helps, Mark
Apr 23, 2013 at 8:14 PM
Thanks Mark a lot,

if I understand you right, i should destroy "list" before the end of test_01() function. So I can call my DisposeList() function:
void test_01(void)
{
   tList *list = malloc(sizeof(tList));

   InitList(list);  

   DisposeList(list);
    
}
inside DisposeList() I just destroy nodes of the list one by other in while loop, inside looks like this:
void DisposeList (tList *L)

_(requires \wrapped(L))
_(requires \thread_local(L))
_(writes \span(L))
_(ensures L->First == NULL && L->Last == NULL)
_(ensures \wrapped(L))
_(decreases 0)

{
    tElem *hlp_p1 = NULL;
    tElem *hlp_p2 = NULL;

    _(unwrapping L) {

        hlp_p1 = L->First;
        L->First = NULL;
        L->Last = NULL;

        while (hlp_p1 != NULL)

        _(invariant hlp_p1 ==> hlp_p1 \in L->\owns && hlp_p1 \in \domain(L))
        _(decreases 0)
        {
            hlp_p2 = hlp_p1->Nextptr;
            free(_(tElem*) hlp_p1);
            hlp_p1 = hlp_p2;
        }
    }
}
So I think I would destroy the "list" properly, but now I am getting these errors:

\singly_linked_list_test_vcc.c(46,3) : error VC8510: Assertion '\extent(L) is writable in call to InitList(list)' did not verify.
\singly_linked_list_test_vcc.c(49,3) : error VC8510: Assertion '\span(L) is writable in call to DisposeList(list)' did not verify.

It seems there is some problem with _(write) clause. Can you help me with that please or anyone else?

Thanks in advance.
Apr 26, 2013 at 7:03 PM
Hi,

I guess this is (partially?) answered by the other discussion (malloc() can fail; DisposeList() should only write L, not \span(L)).

Cheers, Mark
Apr 26, 2013 at 7:54 PM
Ok Mark,

I changed specification of DisposeList() function like below, but now I cant change values of abstract variables and fields of L, which I need for abstract representation of list. Sorry that I didnt mention them in previous post.
    void DisposeList (tList *L)

    _(requires \wrapped(L))
    _(requires \thread_local(L))
    _(writes L)
    _(ensures L->size == 0)
    _(ensures L->values == \lambda int a; \false) 
    _(decreases 0)
    {
        tElem *hlp_p1 = NULL;
        tElem *hlp_p2 = NULL;

        _(unwrap L)

        hlp_p1 = L->First;
        L->First = NULL;
        L->Last = NULL;

        while (hlp_p1 != NULL)

        _(invariant hlp_p1 ==> hlp_p1 \in L->\owns && hlp_p1 \in \domain(L))
        _(decreases 0)
        {
            hlp_p2 = hlp_p1->Nextptr;
            free(_(tElem*) hlp_p1);
            hlp_p1 = hlp_p2;
        }

        _(ghost { 
            L->\owns = {}; 
            L->size = 0;
            L->values = (\lambda int k; \false);
            _(ghost L->find = (\lambda int k; (tElem *) NULL))
        })
    }
Now I get:
error VC8510: Assertion '\span(obj) is writable in call to L->\owns = {}' did not verify.
error VC9502: Call 'L->\owns = {}' did not verify.
error VC9599: (related information) Precondition: 'the owner is mutable'.

So therefore I thought i need \span(L). Thanks

Jan
Apr 27, 2013 at 6:22 AM
Hi,

the old writes clause introduced an inconsistency, which made the proof seemingly run through. (Hint: "vcc /smoke" should have complained about it).

With regards to the latest assertion failure you need to strengthen the loop invariants. VCC doesn't know that the fields of L are writable anymore after L was unwrapped earlier. "_(invariant \mutable(L))" may fix that.

Cheers, Mark