Как аннотировать собранный BoehmGC код для Splint?

Question

Splint хорошо отслеживает утечки памяти в C-коде. каждый malloc() должен иметь соответствующий free(), Но BoehmGC-собранный код использует GC_MALLOC() без соответствия GC_FREE(), Это заставляет Сплинта сходить с ума от множества сообщений об утечках памяти, которых на самом деле нет.

Кто-нибудь знает правильную аннотацию для такого кода, чтобы Splint больше не отображал ложные сообщения об утечке памяти?

В частности, кто-то может прокомментировать пример BoehmGC из Википедии?

#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;
}

Answer 1

Я думаю, что вы должны аннотировать сам API BoehmGC, и тогда аннотации, необходимые для примера (если таковые имеются), станут очевидными.

Для начала, любой указатель, возвращаемый функцией без аннотации, неявно @onlyЭто означает, что вы должны освободить связанную память, прежде чем ссылка будет потеряна. Поэтому первым шагом будет аннотирование распределителей, чтобы они больше не возвращали @only ссылка. Вместо этого руководство рекомендует использовать общие ссылки:

Если Splint используется для проверки программы, предназначенной для использования в среде сбора мусора, может существовать хранилище, которое совместно используется одной или несколькими ссылками и никогда не освобождается явно. Общая аннотация объявляет хранилище, которое может быть разделено произвольно, но никогда не освобождается.

Если вы не хотите изменять API BoehmGC, вы можете обойти его, создав должным образом аннотированные функции-оболочки. Кроме того, вам нужно будет отключить определенные ошибки передачи в ваших функциях-оболочках (потому что они получают неявные @only ссылка из API BoehmGC, а затем вернуть его как @shared).

Например, вот как вы можете отключить ошибку "Выражение не имеет эффекта" в заданной точке вашего кода:

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

Функция-оболочка будет выглядеть примерно так:

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

Тогда в примере вы будете использовать MY_GC_MALLOC скорее, чем GC_MALLOC,