#array_range

I posted yesterday, confused about working with arrays of objects. The post can be found here: http://vc3d.tumblr.com/post/72590187480/arrays-of-objects

I posted a discussion thread on the VCC site here: https://vcc.codeplex.com/discussions/484017

I think I may have figured it out. I took a look through the VCC source and see that \array_range corresponds with $array_range which mentions $array_range_no_state which, for non-primitives, branches to a use of $full_extent. So, is it that \array_range (for objects / structs) is like the following?

\objset \array_range(\object o, size_t s) The set of the extents of all objects o+i where size_t i < s.

Also in the source I see \array_members, corresponding with $array_members, which only mentions $in_array and not any extent. When I replace \array_range with \array_members in my last function, it verifies (well, after removing the _(assert \false), and it does trip that now so the contract must be consistent) and seems to behave how I want it to there.

//Dispose a MyObject array with size 2 void MyObjectArrayDispose_2(MyObject** test) _(requires \forall size_t i; i < 2 ==> \wrapped(&(*test)[i]) ) //conflicts with writes arrayrange _(requires \wrapped((MyObject[2])(*test)) ) _(requires \malloc_root((MyObject[2])(*test)) ) _(writes (MyObject[2])(*test) ) _(writes test) //_(writes &(*test)[0]) //_(writes &(*test)[1]) //Use this instead: _(writes \array_members(*test,2)) { _(unwrap *test+0) _(unwrap &(*test)[1]) //Make arrayobject writable. This shows VCC that the free() below is okay _(unwrap (MyObject[2])(*test) ) free((void*) speccast(MyObject[2], (*test))); }