Array Object fields when the base type is a struct object type

Jan 10, 2014 at 12:51 AM
Edited Jan 10, 2014 at 1:07 AM
This has caused me significant confusion over the past few days:
In section 5.9 Array Object Types, the manual states:
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.
Is the following the complete set of "implicit fields" which all objects have? (taken from vccp.h)
// built-in fields
_(struct \TypeState {
  _(ghost \integer \claim_count)
  _(ghost \bool \closed)
  _(ghost \objset \owns)
  _(ghost \object \owner)
  _(ghost \bool \valid)
The manual specifies \extent and \span like this, in terms of fields:
\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.
Since an array object with object base type has only those implicit fields and none of those fields have struct type, the array object should not have any "struct fields", so its \span should match its \extent.

This code verifies:
#include <vcc.h>
#include <stdlib.h>   //malloc
typedef struct MyObject
    int field;
} MyObject;
void ObjectArrayMallocAndFree_UnwrapBlock_OK()
    MyObject* arr;
    size_t size = 3;
    arr = malloc(sizeof(MyObject) * size);
    _(assume arr != NULL)
    _(wrap &arr[0])
    _(wrap &arr[1])
    _(wrap &arr[2])
    _(writes \span((MyObject[size])arr) )
    _(writes \array_members(arr,size) ) //for the unwraps
    _(requires \full_context() )
        _(unwrap &arr[0])
        _(unwrap &arr[1])
        _(unwrap &arr[2])
If you replace \span((MyObject[size])arr) with \extent((MyObject[size])arr), it no longer verifies. What's going on?