This project is read-only.

how to verify the assignment on a struct in a loop?

Apr 12, 2011 at 3:03 AM

 

#define SIZE 4
#define LENGTH 8

struct SA
{
	int header;
	int data[LENGTH];
};

struct SA frames[SIZE];

void datainit()
	writes (array_range(frames, SIZE))
	ensures (forall(unsigned int i; i < SIZE ==> frames[i].header == 0))
	ensures (forall(unsigned int i, j; i < SIZE && j < LENGTH ==> frames[i].data[j] == 0))
{
	unsigned int i;
	unsigned int j;
	struct SA *p;
	volatile int *pheader;
	volatile int *pdata;

	p = &frames[0];
	for(i = 0; i < SIZE; i++)
		invariant (i <= SIZE)
		invariant (p == &frames[i])
		invariant (forall(unsigned int k; k < i ==> frames[k].header == 0))
  	{
		pheader = &(p->header);

		pdata = &(p->data[0]);

		*pheader = 0;

		for (j = 0; j < LENGTH; j++)
			invariant (pdata == &(p->data[j])) 
			invariant (forall(unsigned int k; k < j ==> frames[i].data[k] == 0))
		{
			*pdata = 0;
			pdata ++;
		}
		p ++;
	}
}

The loop invariant "forall(unsigned int k; k < i ==> frames[k].header == 0" in the outer loop did not verify.

If I remove it, VCC reports the Post condition did not verify.

 

Apr 12, 2011 at 11:15 PM

Hi,

  the problem here is that the inner loop may destroy the invariant you are trying to maintain in the outer loop to establish the post conditions. The writes clause of the inner loop (all the information that the inner loop may destroy) here equals the writes of the complete function - it may destroy any data in frames[]. There are two solutions to this: maintain the outer loop's invariants also in the inner loop or restrict the inner loop's write clause:

for (j = 0; j < length; j++)
  invariant (pdata == &(p->data[j]))
  invariant (forall(unsigned int k; k <= i ==> frames[k].header == 0))
  invariant (forall(unsigned int k, j; k < i && j < LENGTH ==> frames[k].data[j] == 0))
  invariant (forall(unsigned int k; k < j ==> frames[i].data[k] == 0))

// or (preferably):

for (j = 0; j < LENGTH; j++)
  invariant (pdata == &(p->data[j]))
  invariant (forall(unsigned int k; k < j ==> frames[i].data[k] == 0))
  writes(array_range(&p->data, LENGTH))

To prove your postcondition, you also have to maintain "invariant (forall(unsigned int k, j; k < i && j < LENGTH ==> frames[k].data[j] == 0))" in the outer loop.

HTH, Mark

Apr 13, 2011 at 4:17 AM

It's OK now. thank you!

#define SIZE 4
#define LENGTH 8

struct SA
{
	int header;
	int data[LENGTH];
};

struct SA frames[SIZE];

void datainit()
	writes (array_range(frames, SIZE))
	ensures (forall(unsigned int i; i < SIZE ==> frames[i].header == 0))
	ensures (forall(unsigned int i, j; i < SIZE && j < LENGTH ==> frames[i].data[j] == 0))
{
	unsigned int i;
	unsigned int j;
	struct SA *p;
	volatile int *pheader;
	volatile int *pdata;

	p = &frames[0];
	for(i = 0; i < SIZE; i++)
		invariant (i <= SIZE)
		invariant (p == &frames[i])  
invariant (forall(unsigned int k; k < i ==> frames[k].header == 0)) invariant (forall(unsigned int k, j; k < i && j < LENGTH ==> frames[k].data[j] == 0)) { pheader = &(p->header); pdata = &(p->data[0]); *pheader = 0; for (j = 0; j < LENGTH; j++) invariant (pdata == &(p->data[j])) invariant (forall(unsigned int k; k < j ==> frames[i].data[k] == 0)) writes(array_range(p->data, LENGTH)) { *pdata = 0; pdata ++; } p ++; } }