This project is read-only.

Function Pointer problem

Apr 18, 2014 at 6:23 PM
Hi together,

I'm new to VCC and software verification and now I have some problems with the verification of function pointers. I have following code:

#include <vcc.h>

/*****
     TYPES
****/
typedef struct tag_State_t
{
    int state;
} State_t;

typedef void (*transitionFuncPointerHand_t)(void);

typedef void (*funcPointer_t)(State_t* pState, int eventId)
    _(writes &pState->state)
    _(ensures (\old(pState->state == 0)) && (eventId == 1) ==>  pState->state == 1)
    _(ensures (\old(pState->state == 1)) && (eventId == 2) ==>  pState->state == 2)
    ;

/****
     FORWARD DECLARATION
****/

void testFunc1(State_t* pState, int eventId)
    _(writes &pState->state)
    _(requires pState->state == 0)
    _(ensures eventId == 1 ==>  pState->state == 1)
    ;

void testFunc2(State_t* pState, int eventId)
    _(writes &pState->state)
    _(requires pState->state == 1)
    _(ensures eventId == 2 ==>  pState->state == 2)
    ;


void transitionFunctionHand1(void);
void transitionFunctionHand2(void);

/****
     LOCAL VARIABLES
****/

/****
     LOCAL FUNCTIONS
****/
void testFunc(void)
{
    
    State_t stateVar;
    funcPointer_t pFunc1 = &testFunc1;
    funcPointer_t pFunc2 = &testFunc2;

    
    stateVar.state = 0;
    pFunc1( &stateVar, 1 );
    _(assert stateVar.state == 1);

    pFunc2( &stateVar, 2 );
    _(assert stateVar.state == 2);
}

void testFunc1(State_t* pState, int eventId)
{
    if (eventId == 1)
    {
        transitionFunctionHand1( );
        pState->state = 1;
    }
}

void testFunc2(State_t* pState, int eventId)
{
    if (eventId == 2)
    {
        transitionFunctionHand2( );
        pState->state = 2;
    }
}

void transitionFunctionHand1(void)
{

}

void transitionFunctionHand2(void)
{

}
My problem is, that the lines:
    funcPointer_t pFunc1 = &testFunc1;
    funcPointer_t pFunc2 = &testFunc2;
will trigger an error, that the precondition could not be hold:

Error 1 Call '&testFunc2' did not verify.
Error 2 (related information) Precondition: 'pState->state == 1'.

Error 3 Call '&testFunc1' did not verify.
Error 4 (related information) Precondition: 'pState->state == 0'.

Can you please give me any hint.
Thanks for your help.

Uwe