Fixed: Arrays of Objects
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))); }
I had searched through the whole website, the tutorial, the manual, the samples, and the test suite to try to figure this out. Only now that I know what to be looking for do I see that testsuite file arrays-12 shows this use of \array_members!!