#array objects

To add the object in array in for Loop we have several methods: first we can have to simply add those objects to the array then we can add them using for loop in array..... **IN example:** we have a simple object *object that we added 3 times at diffrent index postion in array(**mutArray)..** And other method is to add the object from another array: for that we accessed the each object at current index from the array and added that to the another array(**myMutableArray**)...

NSMutableArray *mutArray=[[NSMutableArray alloc]init];

   for(int i=0;i<=2;i++)

   {

       NSString *object=@"Hello";

       [mutArray addObject:object];

   }

    NSLog(@"Mutable Array==%@",mutArray);

   //if the object are in other array then

   NSArray *objArray=[[NSArray alloc]initWithObjects:@"1",@"2",@"3",@"4",@"5",@"6",@"7",@"8",@"9",@"10",nil];

   NSLog(@"obje==%@",objArray);

   NSMutableArray *myMutableArray=[[NSMutableArray alloc]init];;

   for(int index=0;index<objArray.count;index++)

   {

       [myMutableArray addObject:[objArray objectAtIndex:index]];

   }

   NSLog(@"myMutable Array==%@",myMutableArray);

Almost as soon as submitting my last post here, I think I determined the correct way to annotate the joint unwrapping and freeing of an array of objects.

The post describing my problem: http://vc3d.tumblr.com/post/72817418657/disposing-arrays-of-objects

Working code:

#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]) free(_(MyObject[size])arr); } }

As explored in my last post, \array_members(arr,size) and \extent( (MyObject[size])arr ) seemed to be overlapping. I changed "writes \extent" to "writes \span", and also included \array_members in the writes clause. This verifies, even with smoke testing, so I think it's actually what I want.

I think the array object actually contains "struct fields" of the array elements, so trying to write the \extent of the array object was bringing in the \extent of the array elements too, which didn't jive with their wrapped state, similar to trying to have _(writes \extent(someObject)) and _(requires \wrapped(someObject)) both in a contract at once. See here for more information on that kind of inconsistency: http://vc3d.tumblr.com/post/72017742298/updated-with-explanation-below-i-am-currently

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.