Bug? Function pointer call of pure spec function

Aug 26, 2009 at 11:29 AM

Hi,

as a follow-up to my last problem i discovered an issue concerning function pointers on pure spec functions. Please consider the example below.

#include "vcc.h"

spec(
	 unsigned int ispure func();
)

spec(
	 typedef unsigned int ispure (*funcptr)();
)

void main()
{
	spec(funcptr p = &func;)

	assert((*p)() == func());

	return;
}

The assertion fails and I don't really see why. maybe you can shed some light on this.

Thanks,
Christoph

Coordinator
Aug 26, 2009 at 1:26 PM
As a general advice I would recommend you use maps and lambda expressions instead of pointers to specification functions. They have the advantage of having lexical scoping and are easier to reason about. For example:

typedef bool int_predicate[int];

void f(int_predicate p) { ... p[7] ... }

f(lambda(int x; my_spec_function(x)))
Aug 26, 2009 at 2:18 PM

Thanks for your reply!

can you point me to some documentation on maps?

what about spec functions with more than one parameter / do we support multidimensional maps? In that case how should the lambda expression look like?

Coordinator
Aug 26, 2009 at 2:24 PM

Documentation, no. Examples, yes: have a look at the test files include in the vcc relase under test\testsuite\vcc2\maps and ...\mapofmap.

We do support multi-dimensional maps and also lambda-expressions for those.