Assertion pointer is writable did not verify.

Jan 4, 2013 at 3:49 PM

Hi all,

First wish you all a happy new year! :-)


Second, I am evaluating VCC to use it on a project and I am having some issues. 

When I try to verify this toy code:


typedef struct PartitionWindow{
	int partitionID;
	int partitionWLenght;
} PartitionWindow;

typedef _(dynamic_owns) struct TimeFrameWindow{
	PartitionWindow partitionWindow;
	struct TimeFrameWindow *next;
} TimeFrameWindow; 

typedef _(dynamic_owns) struct schedule{
	TimeFrameWindow *timeFrameWindow;
	_(invariant timeFrameWindow != NULL ==> \mine(timeFrameWindow)) 
    _(invariant \forall TimeFrameWindow *n; \mine(n) && n->next 
	==> \mine(n->next))
	TimeFrameWindow *currentPartition;
} schedule;

void scheduleTest(schedule sch) 
	_(writes \span(sch.currentPartition))
	if(sch.currentPartition->next !=NULL)
	  sch.currentPartition = sch.currentPartition->next;
	else sch.currentPartition = sch.timeFrameWindow;

int initSchedule(schedule *sch)
	_(writes \span(sch))
	TimeFrameWindow * ptr;
	ptr=(TimeFrameWindow *) malloc(sizeof(TimeFrameWindow));
	if(ptr==NULL) return 0;
	ptr->partitionWindow.partitionID = 0;
	ptr->partitionWindow.partitionWLenght= PARTITIONWLENGTH;
	sch->timeFrameWindow = ptr; 
	for(int i=1;i<NTIMEWINDOWS;i++){
		ptr->next=(TimeFrameWindow *) malloc(sizeof(TimeFrameWindow));
		if(ptr->next == NULL) return 0;
		ptr->partitionWindow.partitionID = i;
		ptr->partitionWindow.partitionWLenght= PARTITIONWLENGTH;
	return 1;

I get the following:

C:\Users\David\Documents\Visual Studio 2012\Projects\ScheduleTest\scheduleTest.c(50,3) : error VC8507: Assertion 'ptr->next is writable' did not verify.


But I can not see how avoid that error. It seems that is because the loop, should I add some invariant?


Thank you and best,



Jan 21, 2013 at 7:09 PM
Edited Jan 21, 2013 at 7:23 PM

Yes, you need to provide a suitable invariant. All that VCC knows at the top of a loop is (1) whatever the invariant says, and (2) any variables not changed in the loop body have the same value they held at loop entry. (Note that the definition of what constitutes a variable is somewhat subtle.) These issues are covered in the loop section of the tutorial.

In this case, you need something like

_(writes &ptr->nxt) _(invariant \writable(&ptr->next))