Write access to an array of pointers to structure

Jan 29, 2013 at 9:44 PM


I would like to allow a function to write into an array of non-primitive \objects. I can write into array using \array_range function and into structure accessible via pointer using \span (or \extent). But how can I do both all together? The annotations cannot be combined, because each of both takes \object as its first parameter, but they return \objset.


#include <vcc.h>

typedef struct {
	unsigned int field;
} Structure;

#define ARRAY_SIZE 77
Structure struct_array[ARRAY_SIZE];
Structure * struct_ptr;
Structure * struct_ptr_array[ARRAY_SIZE];

void test(void)
	_(requires \program_entry_point())
	_(writes \array_range(struct_array, ARRAY_SIZE))
	_(writes \span(struct_ptr))
	/* _(writes \span(\array_range(struct_ptr_array, ARRAY_SIZE))) */
	struct_array[31].field = 7;
	struct_ptr->field = 11;
	struct_ptr_array[47]->field = 5417; /* It will not verify */

Any idea? I was thinking that I would create a pure function and put there for loop to fill a \objset using \set_union function, but unfortunately I cannot use for loop construct inside pure function. I miss some functionality to create, edit, and iterate over the array or set.



Feb 11, 2013 at 8:40 PM
Hi David,

set comprehension are a little awkward to do in VCC. The testsuite has an example, http://vcc.codeplex.com/SourceControl/changeset/view/ce4fe3537574#vcc/Test/testsuite/vcc3/index-within, which you can try to extrapolate from. Alternatively, you could define a "container object", that owns the individual structures, and then add an updates clause for the container. This would require you unwrapping the container, do the modification, and then wrap it back up again.

Hope this helps,