Verifying while loop

Feb 26, 2013 at 1:02 PM
Second problem:

I need verify my function DisposeList in implementation of data structure library and i have header file with structures and others needed things:
typedef struct tElem {
    struct tElem *ptr;
    int data;
} *tElemPtr;                   
                                                       
typedef struct { 
    tElemPtr Act;
    tElemPtr First;
} tList;
and then function:
void DisposeList (tList *L) 
_(requires \thread_local(L))
_(writes &L->First)
_(writes &L->Act)
{

  //helpful pointers
  tElemPtr zat = NULL;
  tElemPtr dal = NULL;
    
  if (L->First != NULL)
  {
    dal = L->First;
    L->First = NULL; 
    L->Act = NULL;
    
    while (dal != NULL)
    {
      zat = dal->ptr;
      free(dal);
      dal = zat;
    }
  }
}
VCC gives me:
Verification of DisposeList failed. [0,22]
...: error VC8512: Assertion 'dal is thread local (accessing field ptr)' did not verify.
...: error VC8510: Assertion 'dal is writable in call to free(dal)' did not verify.
... : error VC8510: Assertion '\extent(p) is writable in call to free(dal)' did not verify.
... : error VC9502: Call 'free(dal)' did not verify.
...: error VC9599: (related information) Precondition: 'the extent of the object being reclaimed is mutable'.
...: error VC9599: (related information) Precondition: 'the pointer being reclaimed was returned by malloc()'.
Verification errors in 1 function(s)
Exiting with 3 (1 error(s).)
=== Verification failed. ===

I dont know how to verify while loop exactly, thanks for any answer.
Mar 3, 2013 at 11:21 PM
I think that you will need _(dynamic_owns) and invariants on the tElem structure to specify ownership of the object pointed to by ptr. The VCC tutorial has an example of a SafeString type. Also, Ernie Cohen has posted some linked list code to the website for his CIS 800 Verified Programming course: https://sites.google.com/site/verifiedprogramming/assignments/2527

To be candid, I just now tried creating a singly-linked-list-of-ints structure that was verifiable with VCC, but I was having trouble with malloc() and making sure that objects were writable.