c - 如何从参数返回内存指针以应用于夹板

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 中的参数 out，我需要在使用前检查 NULL 指针。然后返回内存地址。注释“/@out@/”不能放在第一个参数之前，因为它在函数中使用。而“/@null@/”只表示out可以为null，不能为*out。我不知道如何处理它。谁能给一些建议？提前致谢。

Answer 1

最终你无法用夹板表达你想表达的。给定的原型(prototype)根本不可能。主要原因是你需要告诉 splint，*out 是一个 /*@out@*/ 和一个 /*@only@*/。除了夹板没有通过参数返回 /*@only@*/ 存储的概念。每当您将 /*@only@*/ 放在参数中时，splint 都会假定所讨论的函数 free() 是内存，但您打算在此处分配。您现在基本上有两个选择:

• 以夹板可以处理的方式更改您的函数原型(prototype)。特别要避免通过参数返回分配的内存。
• 放松对此函数的检查(例如，将其放在一个单独的、未经检查的文件中)并编写一个具有 splint 可以处理的原型(prototype)的包装函数。