gc-splint.h

/*
    BoehmGC annotated API
*/

extern void GC_INIT(void);

extern /*@shared@*/ /*@null@*/ static void * GC_MALLOC(size_t size) /*@*/
/*@ensures MaxRead(result) == (size - 1) /\ MaxSet(result) == (size - 1) @*/;

extern /*@shared@*/ /*@null@*/ static void * GC_MALLOC_ATOMIC(size_t size) /*@*/
/*@ensures MaxRead(result) == (size - 1) /\ MaxSet(result) == (size - 1) @*/;

extern /*@shared@*/ /*@null@*/ static void * GC_REALLOC(/*@out@*/ void *ptr, size_t size) /*@*/;

extern size_t GC_get_heap_size(void) /*@*/;