Disposing Arrays of Objects
UPDATE: I think I figured this one out. See here: http://vc3d.tumblr.com/post/72820494021/fixed-disposing-arrays-of-objects
I have been trying to verify an object array disposal method which takes an array of wrapped objects, unwraps them, then frees the memory the array used.
I started with this simple example:
#include <vcc.h> #include <stdlib.h> //malloc typedef struct MyObject { int field; } MyObject;void ObjectArrayMallocAndFree_OK() { MyObject* arr; size_t size = 10; arr = malloc(sizeof(MyObject) * size); _(assume arr != NULL) free(_(MyObject[size])arr); }
Then I added on more structure until I have this.
void ObjectArrayMallocAndFree_StillOK() { MyObject* arr; size_t size = 10; arr = malloc(sizeof(MyObject) * size); _(assume arr != NULL) //I would like to do things to the elements here _(writes \extent((MyObject[size])arr)) _(requires \full_context()) { free(_(MyObject[size])arr); } }
Let's say I want to wrap up the array elements and then unwrap them before freeing the array...
void ObjectArrayMallocAndFree_WrapUnwrap_OK() { MyObject* arr; size_t size = 3; arr = malloc(sizeof(MyObject) * size); _(assume arr != NULL) _(wrap &arr[0]) _(wrap &arr[1]) _(wrap &arr[2]) _(unwrap &arr[0]) _(unwrap &arr[1]) _(unwrap &arr[2]) _(writes \extent((MyObject[size])arr)) _(requires \full_context()) { free(_(MyObject[size])arr); } }
Okay... still verifies. What about bunching the unwraps in with the free()?
void ObjectArrayMallocAndFree_UnwrapBlock_FAIL() { MyObject* arr; size_t size = 3; arr = malloc(sizeof(MyObject) * size); _(assume arr != NULL) _(wrap &arr[0]) _(wrap &arr[1]) _(wrap &arr[2]) _(writes \extent((MyObject[size])arr) ) _(writes (MyObject[size])arr ) _(writes \array_members(arr,size) ) //for the unwraps _(requires \full_context() ) //_(requires \malloc_root((MyObject[size])arr) ) //_(requires \forall size_t i; i < size ==> \wrapped(&arr[i])) { _(unwrap &arr[0]) _(unwrap &arr[1]) _(unwrap &arr[2]) free(_(MyObject[size])arr); } }
That doesn't verify. \array_members(arr,size) need to be writable for the unwraps and \extent((MyObject[size])arr) needs to be writable to call free().
Commenting _(writes \extent((MyObject[size])arr)) produces this error:
error VC8510: Assertion '\extent(p) is writable in call to free(_(MyObject[size])arr)' did not verify.
But uncommenting it produces this one:
error VC8027: writes clause of the block might not be included writes clause of the function.
Since the previous attempt (function ObjectArrayMallocAndFree_StillOK above) only required _(writes \extent((MyObject[size])arr) ) and it verifies fine, I believe that the _(wrap &arr[0]) lines are affecting what the prover thinks are things (the array elements) within \extent((MyObject[size])arr), and so it thinks that parts of \extent((MyObject[size])arr) may not be writable within the nested block, HOWEVER, the VCC Manual says:
If the base type of the array is an object type, the array object has no fields (other than the implicit ones present in all objects), and so is not very useful.
So I would think that the elements of the array are not fields of the object-base-type array object and so not included in \extent((MyObject[size])arr), so I'm not sure why there is this interference.
\extent() is defined like this in the manual, and clearly deals only with "fields" and the object itself:
\objset \extent(\object o)
This returns \span(o), along with \extent of any struct fields of o.
\objset \span(\object o)
The set consisting of o, along with a pointer to each primitive field of o.