Как вернуть указатель памяти из аргумента для применения к шине

Question

Я столкнулся с проблемой использования шины. Вот похожий код

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

static void getMem(/*@null@*/void **out, size_t size)
{

    if(out == NULL)
        return;

    *out = malloc(size);
}

int main(/*@unused@*/int argc, /*@unused@*/char *argv[])
{
    char *str = NULL;

    getMem((void **)&str, 1);
    if(str != NULL)
    {
        *str = 'a';
        (void)putchar(*str);
        free(str);
    }

    return 0;
}

шина выдает предупреждающее сообщение, как это,

main.c: (in function getMem)
main.c:11:2: Function returns with possibly null storage derivable from
                parameter *out
  A possibly null pointer is reachable from a parameter or global variable that
  is not declared using a /*@null@*/ annotation. (Use -nullstate to inhibit
  warning)
   main.c:10:12: Storage *out may become null
main.c:11:2: Function returns storage out reachable from parameter not
                completely defined (**out is undefined)
  Storage derivable from a parameter, return value or global is not defined.
  Use /*@out@*/ to denote passed or returned storage which need not be defined.
  (Use -compdef to inhibit warning)
   main.c:10:12: Storage **out allocated

Для аргумента в функции getMem мне нужно проверить NULL-указатель перед использованием. А затем вернуть адрес памяти. Аннотация "/@ out @/" не может быть помещена перед первым аргументом, так как она используется в функции. И "/@ null @/" только означает, что out может быть нулевым, но не *out. Я понятия не имею, как с этим бороться. Может ли кто-нибудь дать несколько советов? Заранее спасибо.

Answer 1

В конечном итоге вы не можете выразить то, что вы хотите выразить с помощью шины. Это просто невозможно с данным прототипом. Основная причина в том, что вам нужно сказать шине, что *out является /*@out@*/ и /*@only@*/, За исключением того, что шина не имеет понятия о возвращении /*@only@*/ хранение через параметры. Всякий раз, когда вы размещаете /*@only@*/ в параметре splint предполагает, что рассматриваемая функция free()память, но вы намерены выделить здесь. Теперь у вас есть два варианта:

• Измените свой прототип функции так, как может обрабатывать шина. Специально избегайте возврата выделенной памяти через параметры.
• Расслабьтесь, проверяя эту функцию (например, поместив ее в отдельный непроверенный файл), и напишите функцию-обертку, имеющую прототип, который может обрабатывать шину.