cmemorysplint

Memory leak after using free() in destroyer function in c (according to splint)

I am relearning C, and using splint to test my source code.

I am trying to do the following:

However, when I test my code with splint, it issues warnings related to temp storage within the destructor, and a memory leak after calling the destructor.

I am wondering (a) whether splint is correct about a memory leak in my code (I think it is not), and (b) what I should to do either fix my code or make splint understand what I am doing.

Anyway, here is the code:

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

// define the structure
struct Boring {
    int amount;
};

// the creator
static struct Boring *Boring_create(int amount) {
    struct Boring *really = malloc(sizeof(struct Boring));
    assert(really != NULL);
    really->amount=amount;
    return really;
}

// the destroyer
static void Boring_destroy(struct Boring *really) {
    assert( really != NULL );
    // free the memory of the Boring structure
    free(really);
}

int main( /*@unused@*/ int argc, /*@unused@*/ char *argv[]) {
    int amount = 5;
    struct Boring *tv = Boring_create(amount);
    printf("The TV is boring level %d\n",tv->amount);

    // destroy the tv!
    Boring_destroy(tv);

    printf("The TV is now boring level %d\n",tv->amount);
    return 0;
}
/* Output */
/*
* $> ./destroytv
* The TV is boring level 5
* The TV is now boring level -538976289 (or 0 depending on OS/compiler)
*/

The code compiles and runs fine with gcc.

However, when I use splint to test it, splint issues the following warnings:

$> splint boringtv.c
destroytv.c: (in function Boring_destroy)    
destroytv.c: Implicitly temp storage really passed as only param: free (really)
 Temp storage (associated with a formal parameter) is transferred to a new non-temporary reference. The storage may be released or new aliases crated. (Use -temptrans to inhibit warning)
destroytv.c: (in function main)
destroytv.c: Fresh storage tv not released before return
 A memory leak has been detcted. Storage allocated locally is not released before the last reference to it is lost (use -mustfreefresh to inhibit warning)
 Fresh storage tv created

The first warning, the more I think about it, the less I understand. But I haven't read enough of the manual to justify a proper question about that one.

The second warning, about the memory leak, it seems splint just doesn't realize that the memory is freed elsewhere, which seems strange to me. The warning goes away if I just call free() within main.

Thanks in advance for the help. Please let me know if more details like line numbers for the warnings would be helpful.

Solution

  • There is no memory leak, as suspected.

    In order to tell splint what function should have control of the structure's memory, the input to the destructor function should be annotated with /*@only@*/. 

    static void Boring_destroy( /*@only@*/ struct Boring *really ) {...

    This tells splint that that function is taking sole control of the variable, thus allowing it to free the memory peacefully without raising any warnings.

    More specifically, the only annotation 'indicate[s] a reference is the only pointer to the object it points to.' (splint manual)

    The annotation removes both the warnings mentioned in the original question, and replaces them with a warning indicating that tv is being used after it has been destroyed. This new warning is desirable, because as mentioned by WhozCraig in the comments, calling on memory once it has been freed is undefined behavior and hence should be avoided.

    References: