2

スプリントを使用する際に問題が発生しました。ここに同様のコードがあります

#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 ではないことを示しているだけです。私はそれに対処する方法がわかりません。誰かアドバイスをいただけますか？前もって感謝します。

4

1 に答える 1

2

結局表現したいことを添え木で表現することはできません。与えられたプロトタイプでは不可能です。主な理由は、スプリントに と を伝える必要がある*outから/*@out@*/です/*@only@*/。splint には、/*@only@*/パラメーターを介してストレージを返すという概念がないことを除いて。/*@only@*/パラメータ splint に配置するときはいつでも、問題free()の関数がメモリであることを前提としていますが、ここに割り当てるつもりです。基本的に、次の 2 つのオプションがあります。

  • スプリントが処理できる方法で関数プロトタイプを変更します。具体的には、割り当てられたメモリをパラメーター経由で返すことは避けてください。
  • この関数のチェックを緩和し (例えば、別のチェックされていないファイルに入れることによって)、スプリントが処理できるプロトタイプを持つラッパー関数を記述します。
于 2014-01-27T07:25:13.973 に答える