Allocating ghost memory

VCC 'injects' its own contracts for the stdlib functions malloc and free, which capture a particular notion of heap memory. The fact that malloc can fail (return NULL) makes it unsuitable for the allocation of ghost memory, which should never fail. For this purpose, the functions/macros spec_malloc and spec_malloc_array should be used. Both take a type parameter that specifies the type of the memory that should be allocated. Additionally, spec_malloc_array takes a unsigned int parameter that specifies the number of elements in the array to be allocated. Here is how to use them:

#include <vcc.h>

struct S { int a; };

void foo() {
  spec(struct S ^p = spec_malloc<struct S>();)
  spec(struct S ^a = spec_malloc_array<struct S>(10);)

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


No comments yet.