Comparision in struct variable with array

May 26, 2011 at 7:14 AM

#define PedFramesNR  8  
#define frameLength  8  

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

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

#define Same(PedWriteFrame, PedReadFrame) \
	forall(unsigned int i, j; j >= 4 && j < PedFramesNR && i < frameLength ==> \
			PedWriteFrame[j].Data[i] & 0xffff == PedReadFrame[j].Data[i] & 0xffff)

#define NotSame(PedWriteFrame, PedReadFrame) \
	exists(unsigned int i, j; j >= 4 && j < PedFramesNR && i < frameLength ==> \
			PedWriteFrame[j].Data[i] & 0xffff != PedReadFrame[j].Data[i] & 0xffff)

int vote(unsigned int port)
	requires(port == 0x1 || port == 0x0)
	requires(forall (unsigned int i; i < PedFramesNR ==> thread_local(as_array(PedWriteFrame[i].Data, frameLength))))
	requires(forall (unsigned int i; i < PedFramesNR ==> thread_local(as_array(PedReadFrame0[i].Data, frameLength))))
	requires(forall (unsigned int i; i < PedFramesNR ==> thread_local(as_array(PedReadFrame1[i].Data, frameLength))))
	ensures(port == 0x1 && Same(PedWriteFrame, PedReadFrame1) ==> result == 1)
	ensures(port != 0x1 && Same(PedWriteFrame, PedReadFrame0) ==> result == 1)
	ensures(port == 0x1 && NotSame(PedWriteFrame, PedReadFrame1) ==> result == 0)
	ensures(port != 0x1 && NotSame(PedWriteFrame, PedReadFrame0) ==> result == 0)
{
	unsigned int i,j;

	for (j = 4; j < PedFramesNR;j++)
		invariant(port == 0x1 ==> 
					forall(unsigned int k; k >= 4 && k < j ==> 
						forall(unsigned int l; l < frameLength ==> 
									(PedWriteFrame[k].Data[l] & 0xffff) == (PedReadFrame1[k].Data[l] & 0xffff)
							   )
						  )
			     )
		invariant(port != 0x1 ==> 
					forall(unsigned int k; k >= 4 && k < j ==> 
						forall(unsigned int l; l < frameLength ==> 
									(PedWriteFrame[k].Data[l] & 0xffff) == (PedReadFrame0[k].Data[l] & 0xffff)
							   )
						  )
			     )
	{
		// comparise every frame
		if (port == 0x1) 
		{ // check port 1
			for (i = 0; i < frameLength;i++)
				invariant(port == 0x1 && forall(unsigned int k; 0 < i ==> (PedWriteFrame[j].Data[k] & 0xffff) == (PedReadFrame1[j].Data[k] & 0xffff)))
			{
				//only care for the low 16-bit
				if ( (PedWriteFrame[j].Data[i] & 0xffff) != (PedReadFrame1[j].Data[i] & 0xffff)  )
					return 0;
			}
		}
		else 
		{      // check port 0
			for (i=0;i<frameLength;i++)
				invariant(port != 0x1 && forall(unsigned int k; 0 < i ==> (PedWriteFrame[j].Data[k] & 0xffff) == (PedReadFrame0[j].Data[k] & 0xffff)))
			{
				if ( (PedWriteFrame[j].Data[i] & 0xffff) != (PedReadFrame0[j].Data[i] & 0xffff)  )
					return 0;
  			}
		}				
	}
    return 1;
}

May 26, 2011 at 7:17 AM

This function is used to comparise if the data in the struct array "PedWriteFrame" is the same with "PedReadFrame1" when the value of parameter "port" is 0x1, to comparise if the data in the struct array "PedWriteFrame" is the same with "PedReadFrame0" otherwise.

The last two "ensures" can not verify.

How can I trace the why it can not verify?