This project is read-only.

A conditional writes clause

May 26, 2011 at 9:13 AM

How can I specify a conditional writes clause? For example, when the value input parameter is 0, the array a0 should be writable. When 1, the array a1 should be writable.

In this code fragment, the function "readPED" writes array "PedReadFrame0" or "PedReadFrame1", depending the parameter "portIdx".

Now I just specify two writes clauses on both array "PedReadFrame0" and "PedReadFrame1".

 

#define PedFramesNR  8  
#define frameLength  8  

typedef struct _CCtmrFrame
{
	unsigned int Header;
	unsigned int Data[frameLength];
} CCtmrFrame;

CCtmrFrame PedWriteFrame[PedFramesNR];
CCtmrFrame PedReadFrame0[PedFramesNR];
CCtmrFrame PedReadFrame1[PedFramesNR];

typedef struct _ctmr_port
{
	volatile unsigned int WDATA;
	volatile unsigned int HEADER;
	volatile unsigned int CTL;
	volatile unsigned int RDATA;
	volatile unsigned int STATUS;
} CTMR_PORT;

CTMR_PORT PORTS[2];

unsigned int readPort(unsigned int portIdx, CCtmrFrame *framePtr)
	requires(portIdx == 0 || portIdx == 1)
	maintains(mutable(&PORTS[portIdx]))
	writes(extent(framePtr))
{
	volatile unsigned int frameHeader;
	volatile unsigned int indxData;

	volatile unsigned int *dataPtr;
	volatile unsigned int *headPtr;
	volatile unsigned int counter=0;

	indxData = 0;			
	headPtr = &(framePtr->Header); 
	dataPtr = &(framePtr->Data[0]);
	
	frameHeader = PORTS[portIdx].STATUS;//*(volatile unsigned int *)(port_ptr->STATUS) ;
	*headPtr = frameHeader;
	assert(framePtr->Header == PORTS[portIdx].STATUS);
	while ( (frameHeader & 0x4000)== 0x0) 
		invariant(indxData < frameLength) 
		invariant(counter <= indxData)
		invariant(dataPtr == &(framePtr->Data[indxData]))
	{
		*dataPtr = PORTS[portIdx].RDATA;//*(volatile unsigned int *)(port_ptr->RDATA) ;
		assert(framePtr->Data[indxData] == PORTS[portIdx].RDATA);
		dataPtr++;
		indxData++;
		if (indxData == frameLength)
		{
			break;
		}
		frameHeader = PORTS[portIdx].STATUS;//*(volatile unsigned int *)(port_ptr->STATUS) ;
		counter++;	
	}
	return counter; 
}

unsigned int readPED(int portIndex,int frameIndex)
	requires(portIndex == 0 || portIndex == 1)
	maintains(mutable(&PORTS[portIndex]))
	writes(extent(&PedReadFrame0[frameIndex]))
	writes(extent(&PedReadFrame1[frameIndex]))
{
	CCtmrFrame *framePtr ;
	if (portIndex == 0)
	{
   		framePtr=(CCtmrFrame *)(PedReadFrame0 + frameIndex);
	}
	else
	{
		framePtr=(CCtmrFrame *)(PedReadFrame1 + frameIndex);	
	}
	
	if (readPort((unsigned int)portIndex, framePtr)>0) 
	{
		return 1;
	}
	else
	{
		return 0;
	}
}

May 27, 2011 at 9:33 PM
Hi,

  you can use the ternary operator (?:) to do a conditional writes clauses. Here's a simple example (new syntax):

#include <vcc.h>

typedef struct _S { int a; } S;

void foo(S *s, S *t, unsigned i, unsigned v)
  _(requires i < 2)
  _(maintains \wrapped(s) && \wrapped(t))
  _(writes i == 0 ? s : t)
  _(ensures i == 0
      ? s->a == 42
      : t->a == 42)
{
  unsigned result;
  if (i == 0) {
    _(unwrap s)
    s->a = 42;
    _(wrap s)
  } else {
    _(unwrap t)
    t->a = 42;
    _(wrap t)
  }
}

Hope that helps,

  Mark