[Gc] Re: Boehm GC and Splint

Andrew Pennebaker andrew.pennebaker at gmail.com
Thu Aug 4 00:19:58 PDT 2011


Guillermo on StackOverflow<http://stackoverflow.com/questions/6903272/how-do-i-annotate-boehmgc-collected-code-for-splint/6904955#6904955>believes
that the Boehm GC API, and any code that uses it, can pass Splint
with no warnings if the API is annotated as follows:

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) /*@*/;

Cheers,

Andrew Pennebaker
www.yellosoft.us

On Mon, Aug 1, 2011 at 3:17 PM, Andrew Pennebaker <
andrew.pennebaker at gmail.com> wrote:

> Splint (http://www.splint.org/) is a static code analyzer for C. Perhaps
> its chief feature is its ability to track down sources of memory leaks.
>
> Splint knows every malloc() should have a matching free(). Obviously, it
> has trouble reasoning about GC_MALLOC().
>
> Does anyone know how to properly annotate code for Splint so that it
> ignores apparent memory leaks caused by Boehm GC code?
>
> In particular, could someone offer an annotated version of the Wikipedia
> Boehm GC example that does this?
>
> http://en.wikipedia.org/wiki/Boehmgc#Example
>
> Cheers,
>
> Andrew Pennebaker
> www.yellosoft.us
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://napali.hpl.hp.com/pipermail/gc/attachments/20110804/edaf3194/attachment.htm


More information about the Gc mailing list