verification of function pointers?

Jun 21, 2011 at 2:14 AM

Hi, I am new to vcc and I hope that someone can point me to a tutorial for verification of function pointers. 

For example: 

typedef struct type_2{ 
      int test1; 
      int test2;
} type2;

typedef struct  type_1{
        type2(*types)(int, int);  
} type1;

type1* abc;

type2 getme()
maintains(wrapped(abc))
writes(&abc)
{
      type2 a = abc->types(10,15);
     return a;

}

I keep getting the error code VC8504: Assertion 'abc->types is a valid function pointer  did not verify'

Thanks.

Coordinator
Jun 22, 2011 at 7:59 PM

Hi,

  unfortunately function pointers support in VCC is not quite complete, and there's even less documentation.

  An example that works is this:

#include <vcc.h>

typedef int (*TF)(int x)
  requires(x > 1)
  ensures(result > 0);

int bar(int x)
  requires(x > 0)
  ensures(result > 1);

void foo() {
  TF p = &bar;
  int res = p(3);
  assert(res > 0);
}

  Some similar example are in the file "vcc\Test\testsuite\vcc2\functionPtrs" in the VCC repository, which you can browse to via the http://vcc.codeplex.com/SourceControl/BrowseLatest link.

In your case, the missing condition for calling the function pointer is the typedness of the function pointer held in the structure. Adding "assume(typed(abc->types));" makes the error go away. Normally, this should be in the invariant of the structure (like "invariant(typed(types))"), but in this case, VCC complains about the inadmissibility of the structure, due to an incompleteness in function pointer support (VCC think that the typedness of a function pointer can go away in the admissibility check, which it can't.). 

Hope this helps, Mark