Admissibility annotations

void funcname(Type *p) { 
   // Custom admissibility check

For specifying custom admissibility checks, a function, which takes a pointer of type Type, for which the admissibility check should be executed, is prefixed with the keyword isadmissibilitycheck. Within this function assert and assume statements may be specified to guide the prover through proving the admissibility of the invariants. It is not allowed to modify the state of p in function marked as isadmissibilitycheck, this will yield in an error message by VCC.
Such functions are usually combined with the havoc_others() notation, to check the admissibility of the invariants of p with respect to other objects, that might change, while p is closed.

void havoc_others(void* p)

This function is usually used within custom admissibility check functions as explained above. This function destroys the meta and state information of all objects, that are not pointed to by p. The function still ensures, that p remains closed and typed and that the span of p does not change.

Last edited Oct 17, 2009 at 12:13 PM by MarkHillebrand, version 3


No comments yet.