How to declare and use a pointer to a pure function

Feb 17, 2011 at 7:06 PM

How can I declare and use a pointer to a pure function?

Here is what I tried

#include <vcc.h>

struct Foo {
   int a ;
   _( pure ) bool (*f)() ;
} ;

void bar( struct Foo *obj )
   _(requires obj->f() )
{
}

 

The error is : "function 'fnptr#1' used in pure context, but not marked with 'ispure'" on line 9.

Editor
Feb 17, 2011 at 7:53 PM

I don't have an answer to that, Theodore, sorry, but I do have a question complement... Is it possible to declare a function pointer to have a certain contract and have VCC check that the function that is used to instantiate it does fulfill this contract (pointer's preconditions imply the function's preconditions, function's writes are a subset of the pointer's writes, and function's postconditions imply the pointer's postconditions).

I remember seeing something like this in the documentation a long time ago, but can't seem to find it anymore... Or maybe i dreamt it to begin with?

Cheers,
Francois 

Feb 18, 2011 at 9:28 AM
Edited Feb 18, 2011 at 9:37 AM

@ Francois:

Yes you can do this, at least I tried out defining function pointers with contracts like one and a half year ago and it worked. Just define a function pointer type and add annotations to the type declaration:

my example from that time (DISCLAIMER: old syntax and i didnt check it still verifies)

 

int bla(int *a,int b)
writes(a)
maintains(mutable(a))
ensures(*a == b)
returns(42)
{ 
  *a=b;
  return 42;
}

typedef int (*FP)(int * x, int y) 
writes(x) 
maintains(mutable(x)) 
ensures(*x == y) 
returns(42);
int main()
{
FP fp; 
int a,b; 

fp=&bla;

b=7; 
b=(*fp)(&a,b);

assert(a==7); 
assert(b==42);

return 0;
}

I don't know what VCC checks for the function pointer assignment though. 

Editor
Feb 18, 2011 at 9:32 AM
Edited Feb 18, 2011 at 9:43 AM

Thanks Christoph, I'll have a look.

If this still works, maybe it also works with the "is_pure" contract with an intermediate typedef. I'll give it a quick try later on today and come back to this thread.

EDIT: I took the time to do it now, in the end. Apart from the fact that you forgot to initialise the function pointer, the code you provided verifies fine, thanks a lot.
Unfortunately for you, Theodore, my attempts at making it work for pure functions were less fruitful. Maybe this is something that a more active developer could look at? It doesn't sound like a huge fix, as some contracts are obviously already taken into account.

Feb 18, 2011 at 9:55 AM
Edited Feb 18, 2011 at 9:55 AM

Yes, I edited my example above. I accidently through out the initialisation when I removed some redundant assertions and additional code. But good to know it still works!

Feb 21, 2011 at 3:18 PM

Christoph and François:  Interesting discussion.  I learned a few things from it.

My original question remains unanswered:  (How) Can I declare and use a pointer to a pure function?  Anybody?

Coordinator
Mar 24, 2011 at 6:51 AM

Hi Theodore,

  unfortunately this is not currenty supported; Ernie posted an issue about it (http://vcc.codeplex.com/workitem/6348), which you may have already seen.

  Best, Mark

Mar 24, 2011 at 12:56 PM

Is there some way to  persuade vcc to ignore the fact that a pointer is not pure and go ahead with the verification anyway.

Coordinator
Mar 25, 2011 at 8:10 AM

I'm afraid that I don't know of a way. If you are willing to modify your code for now, you could verify it against a known pure function, though.

Best, Mark