CodePlexProject Hosting for Open Source Software

error VC9703: Memory allocation in pure context is not allowed. error VC9703: Writing memory location 'p' in pure context is not allowed.

ispure int f() ensures(result == result + 1); ispure int g() ensures(result == h()); ispure int h() ensures(result == g() + 1);

A valid pure postcondition has one of the following forms:

- result.f1.f2...fN == EXPR where EXPR doesn't contain result and N >= 0 (that is result == EXPR is also allowed)
- (a let expression) exists(T v; v == EXPR; POST) where EXPR doesn't contain result and doesn't contains v, and POST is a valid pure postcondition

A pure function can have any number of valid pure postconditions, either as separate ensures(...) clauses or conjoined with &&.

However, two different postconditions of the form result.f1...fN == EXPR1 and result.f1...fM == EXPR2 where N <= M are not allowed. This is to prevent specification of a substructure as a whole and then some of its components, e.g., result.x == { .y = 10, .z = 20 } && result.x.y = 30 .

Take a directed graph, where nodes are pure functions. If a contract of function f calls function g then there is an edge going from f to g. This graph is not allowed to have cycles.

For example, the following are valid pure function definitions:

struct IN { int d0; int d1; int d2; }; struct A { int x; int y; }; ispure struct A ok1(struct IN *x) requires(thread_local(x)) ensures(result.x == x->d0 && result.y == x->d0) reads(x); struct B { struct A a; int z; }; ispure struct A ok2(struct IN *x) requires(thread_local(x)) ensures(result == { .x = x->d0, .y = 7 }) reads(x);

Given a pure function:

ispure T f(P) requires(R) ensures(E);

The following definition axiom is generated:

axiom(forall(P; E [result := f(P)]))

That is the requires(...) clause is ignored in the axiom. Still, if you call f in non-contract context (i.e., assign its result to a local ghost variable), the pre-condition will be checked.

For example:

ispure int f(int x) ensures(result == x + 7);

will generate:

axiom(forall(int x; {f(x)} f(x) == x + 7))

If you want to have a post-condition in a pure function of a different form, you need to use an explicit axiom, for example:

ispure int f(int x); axiom(forall(int x; {f(x)} f(x) > 0))

Then it is however up to you to make sure such a function, characterized by the axiom, actually exists.

ispure bool isPositive(int *x) reads(x) ensures(result == (*x > 0));

However, if you list precisely what location a pure function reads, then you would expect it to depend not on the entire heap, but only on those locations. This is where a frame axiom comes into play. If you add frameaxiom specifier to the function above, VCC will implicitly generate the following:

bool isPositive_frame(int vx, int *x); axiom(forall(state_t s; int vx; int *x; isPositive(s, x) == isPositive_frame(s[x], x)));

Thus, if VCC has two states s1 and s2, and knows they are the same at x, then it will also know isPositive(s1, x) == isPositive(s2, x).

Now, you might wonder why to bother with passing pointers, if we end up dereferencing them at call site anyway, with this additional axiom. The reason is that you might also list a root of ownership domain, and be allowed to read the entire ownership domain.

A good question is why we don't always generate a frame axiom. The answer is that it is costly for the prover to instantiate those, so we only want them when they are really needed.

Note that the reads(...) clause has only any positive effects on verification, when you also have frameaxiom. Otherwise it's only informational, but still generates a reads check. If you don't need the frameaxiom, and have a pure function that reads the state you can say reads(set_universe()), which will prevent generation of a reads check.

ispure unsigned foo(unsigned x) ensures(result == x - 10); ... unsigned tmp = foo(0);

Because the pure function has no body, there is no place to put the check that x - 10 does not overflow. Still, even if we required a body, the fix would be to add precondition x >= 10 to foo(...). Such precondition would again go unchecked when the function would be called in contract context.

ispure int foo() { int uninitialized; return uninitialized; } ... int x1 = foo(); int x2 = foo(); assert(x1 == x2);

Before we would generate a free postcondition on Boogie procedure foo(), binding the result returned to result of function #foo(), representing the pure function. Now this postcondition is not free, preventing this kinds of problem.

Last edited Nov 13, 2009 at 1:06 PM by stobies, version 8