Specification code can be used to aid the verification process. There are multiple aspects of specification code:

Specification Fields

It is possible to declare specification fields in structs and unions. These fields are invisible for the normal C compiler, but can be used in specification code to store artifacts or abstraction used for verification. The are declared using the spec macro as follows:

struct S {
  int normalField;
  int anotherNormalField;
  spec(bool specField;)
  spec(struct T t;)
};


Similarly, specifcation fields can be added to unions, in which case they are not added to the union facets but are rather present as normal struct fields. Specification fields do not contribute to the size of the structure.

Specification variables

Specification variables can be declared in functions to help verification purposes. Again, specification variables are invisible for the C compiler. They are also declared using the spec macro:

void foo() {
  int normalVar;
  spec(int specVar;)
  /* ... */
}

Specification functions

Auxiliary functions for verification purposes can be declared using the spec macro; they are invisible for the C compiler:

spec(int specFunction(int a);

Specification Parameters

For verification purposes, it is possible to pass extra parameters to non-specification functions. These are declared using the spec macro, after all the normal function parameters:

int foo(int normalPar spec(int specPar) { ... }


Note the missing comma between the normal parameter and the specification parameter. Calls to a function with specification parameters similarly used the spec macro:

void bar() {
  int a = 5;
  spec(int b = 10;)

  int c = foo(a spec(b));
}

Separation of specification code and normal code

These specification artefacts must not be referenced from non-specification code. Failure to do so currently yields a warning, which will be turned into an error at a later stage. Code that exists for verification purposes only must be guarded by the spec macro:

void foo(int a spec(int b)) {
  spec(int c;)
  spec(
    if (b == 0) {
      c = 1; 
    } else {
      c = 2;
    }
  )
  /* ... */
}


Some cases do not require such an explicit annotation, in particular, the use of verification primitives wrap, unwrap, and expose, as well as assigning to a specification field, variable or parameter. So, the above code could be more concisely be written as:

void foo(int a spec(int b)) {
  spec(int c;)
  c = (b == 0) ? 1 : 2;
  /* ... */
}

Pointers to specification memory

VCC distinguishes between pointers to physical memory locations and pointers to specification memory. Pointers to specification memory are declared using "^" instead of "*" and are incompatible with physical pointers. Internally, VCC simply places specification objects at adresses beyond the physical address range. The address of a specification field, variable, or parameter is implicitly of spec pointer type, so are the addresses of non-spec fields pointed to from via a spec pointer. For example:

#include <vcc.h>

struct S {
  int a;
  spec(int b;)
};

struct T {
  struct S s;
  spec(struct S r;)
};

void foo(struct T *p) {
  spec(int ^i1 = &(p->s.b);)
  spec(int ^i1 = &(p->r.a);)
}

void bar(struct T ^p) {
  spec(int ^i1 = &(p->s.a);)
}



Last edited Feb 11, 2011 at 6:58 PM by MarkHillebrand, version 7

Comments

No comments yet.