How do I annotate BoehmGC-collected code for Splint?

Splint does a good job tracking down memory leaks in C code. Every malloc() should have a matching free(). But BoehmGC-collected code uses GC_MALLOC() with no matching GC_FREE(). This makes Splint go crazy with tons of messages about memory leaks that aren't actually there.

Does anyone know the proper annotation for such code so that Splint no longer shows spurious memory leak messages?

In particular, could someone annotate Wikipedia's BoehmGC example?

#include <assert.h>
#include <stdio.h>
#include <gc.h>

int main(void)
{
    int i;

    GC_INIT();
    for (i = 0; i < 10000000; ++i)
    {
        int **p = GC_MALLOC(sizeof(int *));
        int *q = GC_MALLOC_ATOMIC(sizeof(int));

        assert(*p == 0);
        *p = GC_REALLOC(q, 2 * sizeof(int));
        if (i % 100000 == 0)
            printf("Heap size = %zu\n", GC_get_heap_size());
    }

    return 0;
}

Solution

I think that you should annotate the BoehmGC API itself, and then the annotations needed for the example (if any) will become obvious.

For starters, any pointer returned by a function with no annotation is implicitly @only, which means that you must release the associated memory before reference is lost. Therefore, the first step would be to annotate the allocators so that they no longer return an @only reference. Instead, the manual advises using shared references:

If Splint is used to check a program designed to be used in a garbage-collected environment, there may be storage that is shared by one or more references and never explicitly released. The shared annotation declares storage that may be shared arbitrarily, but never released.

If you didn't want to modify the BoehmGC API, you could work around it by creating properly annotated, wrapper functions. In addition, you would need to disable specific transfer errors within your wrapper functions (because they get an implicit @only reference from the BoehmGC API and then return it as @shared).

For example, this is the way you would disable the "Statement has no effect" error at a given point of your code:

/*@-noeffectuncon@*/
not_annotated_void_function();
/*@=noeffectuncon@*/

The wrapper function would be something like this:

/*@shared@*/ /*@null@*/ /*@out@*/ static void * MY_GC_MALLOC(size_t size) /*@*/{
    /*@-onlytrans@*/
    return( GC_MALLOC(size) );
    /*@=onlytrans@*/
}

Then in the example you'd use MY_GC_MALLOC rather than GC_MALLOC.