This project is read-only.

how to update the array member in a struct variable?

Mar 28, 2011 at 2:28 AM

The function "initdata" will set all the member in the array "PedReadFrame0" and "PedReadFrame1" to be zero:

#define PedFramesNR  8
#define frameLength  8

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

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

void initdata(void)
    ensures(ReadCounter0 == 0)
    ensures(ReadCounter1 == 0)
    ensures(WriteCounter0 == 0)
    ensures(WriteCounter1 == 0)
    ensures(forall (unsigned int i; i < PedFramesNR ==> PedReadFrame0[i].Header == 0))
    ensures(forall (unsigned int i, j; i < PedFramesNR && j < frameLength ==> PedReadFrame0[i].Data[j] == 0))
    ensures(forall (unsigned int i; i < PedFramesNR ==> PedReadFrame1[i].Header == 0))
    ensures(forall (unsigned int i, j; i < PedFramesNR && j < frameLength ==> PedReadFrame1[i].Data[j] == 0))
{
    int i,j;

    CCtmrFrame *framePtr;
    volatile unsigned int *readdataPtr;
    volatile unsigned int *readheadPtr;
   
    for (j = 0; j < PedFramesNR && j < INT_MAX; j++)
    {
        framePtr = &(PedReadFrame0[j]);   
        readheadPtr = &(framePtr->Header);
        readdataPtr = &(framePtr->Data[0]); 
        *readheadPtr = 0;
        for (i = 0; i < frameLength && i < INT_MAX; i++)
            invariant(i <= frameLength)
        {
            *readdataPtr = 0;
            readdataPtr++;
        }

        framePtr = &(PedReadFrame1[j]);   
        readheadPtr = &(framePtr->Header);
        readdataPtr = &(framePtr->Data[0]);   
         
        *readheadPtr = 0;
        for (i = 0; i < frameLength; i++)
            invariant(i <= frameLength)
        {             
            *readdataPtr = 0;
            readdataPtr++;
        }
    }
      
      ReadCounter0 = 0;
      ReadCounter1 = 0;
      WriteCounter0 = 0;
      WriteCounter1 = 0;
}

At first, I specify "writes", but VCC reports the "Assertion 'readdataPtr is writable' did not verify". Then I specify "wrapped", and everything seems to be OK. BUT when I change the post-condition to "ensures(forall (unsigned int i, j; i < PedFramesNR && j < frameLength ==> PedReadFrame1[i].Data[j] == 1))", VCC also reports "succeed".

Mar 28, 2011 at 8:09 AM
Edited Mar 28, 2011 at 8:43 AM

Hi,

  my guess is that you have specified contradicting requirements to the function via its "requires()" and "writes()" clauses [EDIT: said "ensures()" earlier], which allows VCC to deduce anything. An example of such a function / requirements is this:

 

#include <vcc.h>

struct S { int a; };

void foo(struct S *s)
    requires(wrapped(s))
    writes(&s->a)
{
    // anything can be shown
}

 

The problem here is that a field of a wrapped structure cannot be writable. Unfortunately, it's not always that easy to spot inconsistent requirements. VCC provides a switch ("/smoke") that can be of help sometimes. In smoke mode, for all control points in the code VCC checks for a certain time whether it can prove false (i.e., "anything"); if so, there might be a problem, which gets reported. For example, on the example above, VCC says this: 

 

Verification of foo succeeded.
C:\x\y\d251424_2.c(7): found unreachable code, possible soundness violation, please check the axioms or add an explicit assert(false)

 

(Note that using the Visual Studio plugin, this output will only show up in the VCC output window, and may not be marked as an error)

Below, I've given requirements to prove memory safety for your code.

Hope that helps,

Mark

 

#include <vcc.h>
#include <stdlib.h>

#define PedFramesNR  8
#define frameLength  8

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

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

unsigned ReadCounter0;
unsigned ReadCounter1;
unsigned WriteCounter0;
unsigned WriteCounter1;

void initdata(void)
    ensures(ReadCounter0 == 0)
    ensures(ReadCounter1 == 0)
    ensures(WriteCounter0 == 0)
    ensures(WriteCounter1 == 0)

    writes(array_range(PedReadFrame0,PedFramesNR))
    writes(array_range(PedReadFrame1,PedFramesNR))
    writes(extent(gemb(&ReadCounter0)))
    writes(extent(gemb(&ReadCounter1)))
    writes(extent(gemb(&WriteCounter0)))
    writes(extent(gemb(&WriteCounter1)))

    ensures(mutable(gemb(&ReadCounter0)))
    ensures(mutable(gemb(&ReadCounter1)))
    ensures(mutable(gemb(&WriteCounter0)))
    ensures(mutable(gemb(&WriteCounter1)))

    //ensures(forall (unsigned int i; i < PedFramesNR ==> PedReadFrame0[i].Header == 0))
    //ensures(forall (unsigned int i, j; i < PedFramesNR && j < frameLength ==> PedReadFrame0[i].Data[j] == 0))
    //ensures(forall (unsigned int i; i < PedFramesNR ==> PedReadFrame1[i].Header == 0))
    //ensures(forall (unsigned int i, j; i < PedFramesNR && j < frameLength ==> PedReadFrame1[i].Data[j] == 0))
{
    int i,j;

    CCtmrFrame *framePtr;
    volatile unsigned int *readdataPtr;
    volatile unsigned int *readheadPtr;
    
    for (j = 0; j < PedFramesNR && j < INT_MAX; j++)
    {
        framePtr = &(PedReadFrame0[j]);    
        assert(framePtr == &(PedReadFrame0[j]));
    
        readheadPtr = &(framePtr->Header);
        readdataPtr = &(framePtr->Data[0]);  
        *readheadPtr = 0;

        for (i = 0; i < frameLength && i < INT_MAX; i++)
            invariant(i <= frameLength)
            invariant(readdataPtr == &framePtr->Data[i])
        {
            *readdataPtr = 0;
            readdataPtr++;
        }

        framePtr = &(PedReadFrame1[j]);    
        readheadPtr = &(framePtr->Header);
        readdataPtr = &(framePtr->Data[0]);    
          
        *readheadPtr = 0;
        for (i = 0; i < frameLength; i++)
            invariant(i <= frameLength)
            invariant(readdataPtr == &framePtr->Data[i])
        {              
            *readdataPtr = 0;
            readdataPtr++;
        }

    }

    ReadCounter0 = 0;
    ReadCounter1 = 0;
    WriteCounter0 = 0;
    WriteCounter1 = 0;
}

 

Mar 28, 2011 at 9:24 AM

Thank you for your help! But I still don't know how to give the appropriate pre-condition to make the array member in a struct variable writable.

The pointer "readdatePtr" points to the array element in a struct variable. And VCC reports that it is not writable...

D:\PhD\hangtian\OS\VCC\studyvcc\studyvcc\initdata.c(99,5) : error VC8506: Assertion 'readdataPtr is typed' did not verify.
D:\PhD\hangtian\OS\VCC\studyvcc\studyvcc\initdata.c(99,5) : error VC8507: Assertion 'readdataPtr is writable' did not verify.
D:\PhD\hangtian\OS\VCC\studyvcc\studyvcc\initdata.c(112,5) : error VC8506: Assertion 'readdataPtr is typed' did not verify.
D:\PhD\hangtian\OS\VCC\studyvcc\studyvcc\initdata.c(112,5) : error VC8507: Assertion 'readdataPtr is writable' did not verify.
Exiting with 3 (1 error(s).)

Mar 28, 2011 at 9:30 AM

Hi,

  did you also add the loop invariants, that I had in my example ("invariant(readdataPtr == &framePtr->Data[i])")? If no, please try. If yes, could you post the full non-working example again?

  Thanks, Mark

Mar 28, 2011 at 9:45 AM

Oh! When I add the loop invariant, it's OK. It seems that VCC doesn't know the pointer "readdataPtr" points to the array element in the struct variable "PedReadFrame0", "PedReadFrame1"?

Mar 28, 2011 at 9:46 AM

void initdata(void)
	ensures(ReadCounter0 == 0)
    ensures(ReadCounter1 == 0)
    ensures(WriteCounter0 == 0)
    ensures(WriteCounter1 == 0)

    writes(array_range(PedReadFrame0,PedFramesNR))
    writes(array_range(PedReadFrame1,PedFramesNR))
    writes(extent(gemb(&ReadCounter0)))
    writes(extent(gemb(&ReadCounter1)))
    writes(extent(gemb(&WriteCounter0)))
    writes(extent(gemb(&WriteCounter1)))

    ensures(mutable(gemb(&ReadCounter0)))
    ensures(mutable(gemb(&ReadCounter1)))
    ensures(mutable(gemb(&WriteCounter0)))
    ensures(mutable(gemb(&WriteCounter1)))

{
	int i,j;

	CCtmrFrame *framePtr;
	volatile unsigned int *readdataPtr;
	volatile unsigned int *readheadPtr;
	
    for (j = 0; j < PedFramesNR && j < INT_MAX; j++)
		invariant(j <= PedFramesNR)
	{
		framePtr = &(PedReadFrame0[j]);    
		readheadPtr = &(framePtr->Header);
		readdataPtr = &(framePtr->Data[0]); 
		*readheadPtr = 0;
		for (i = 0; i < frameLength && i < INT_MAX; i++)
			invariant(i <= frameLength)
			invariant(readdataPtr == &framePtr->Data[i])

		{
			*readdataPtr = 0;
			readdataPtr++;
		}

		framePtr = &(PedReadFrame1[j]);    
		readheadPtr = &(framePtr->Header);
		readdataPtr = &(framePtr->Data[0]);    
	      
		*readheadPtr = 0;
		for (i = 0; i < frameLength; i++)
			invariant(i <= frameLength)
			invariant(readdataPtr == &framePtr->Data[i])
		{	  		
			*readdataPtr = 0;
			readdataPtr++;
		}
	}
   	
  	ReadCounter0 = 0;
  	ReadCounter1 = 0;
  	WriteCounter0 = 0;
  	WriteCounter1 = 0;
}

Mar 28, 2011 at 10:27 AM

That's right. Variables 'i' and 'readdataPtr' are both modified in the loop, and VCC wouldn't be able to figure out the relation between them when proving an iteration of the loop. Without the loop invariant, readdataPtr could point to any integer location from VCC point of view...

Mark