This section is severly out of date and needs to be re-written entirely.

C has only a weak type system and no automatic garbage collection. C programs can access memory outside the bounds of allocated objects. For example, it is possible to dereference a pointer after it has been freed or to write beyond the end of an allocated C region. Since allowing such behavior makes it hard to reason about the correctness of a C program, we impose several restrictions that together ensure that C programs can only write to allocated regions. In particular, we check at each memory access (both read and write) that the accessed memory is part of an allocated region and may be access by the current thread.

explain about wrapped(), mutable()

#include <vcc.h>
#include <limits.h>

void increment(int *x)
    requires(mutable(x))
    requires(*x < INT_MAX)
    writes(x)
    ensures(*x == old(*x) + 1)
{
    *x = *x + 1;
}

The additional glitch here is that we need to specify where the function is going to write. It can be done with a writes(…) clause, which takes a set of memory locations, which are modified in the implementation of the function. The pointers refered to by the writes clause, must only list those pointers to objects, which are owned by the current thread, i.e. either wrapped() or mutable(). All nested object in the ownership domain of references objects, may be accessed by unwrapping a wrapped object, which contains the nested objects. Those nested objects must not be listed in the writes clause.

Now we arrive at the old expression. It is used in postconditions to refer to the state of the world before the call. So the postcondition on the increment function states, that the new value of *x is one more than it used to be.

Last edited Nov 13, 2009 at 12:00 PM by stobies, version 6

Comments

No comments yet.