This project is read-only.

Bug? Function pointer call of pure spec function

Aug 26, 2009 at 12:29 PM


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"

	 unsigned int ispure func();

	 typedef unsigned int ispure (*funcptr)();

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

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


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


Aug 26, 2009 at 2: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 3: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?

Aug 26, 2009 at 3: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.