2

次のようなことを行うプログラムがあります。

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

int f(char *result)
{
    if (result != NULL)
    {
        *result = 'a';
    }
    return 0;
}

int main ()
{
    char s = 0;
    (void)f(&s);
    printf("f gave %c\n", s);
    return 1;
}

関数にポインターを渡し、逆参照して、何かを保存します。Splint はmaxSet(result) >= 0、f の制約を解決できないと報告しています。

test.c: (in function f)
test.c:8:9: Possible out-of-bounds store: *result
    Unable to resolve constraint:
    requires maxSet(result @ test.c:8:10) >= 0
     needed to satisfy precondition:
    requires maxSet(result @ test.c:8:10) >= 0
  A memory write may write to an address beyond the allocated buffer. (Use
  -boundswrite to inhibit warning)

&sスタック上の単一の文字を指すため、注釈を追加せずに maxSet を 1 にする必要があります。Splint が不平を言っているのはなぜですか?

4

1 に答える 1

1

私が知る限り、スプリントは、実際のバッファーまたは配列を検証可能に指していないポインターでは制約を検証できないと報告しています。1 の配列に相当する単一の変数を処理できない理由がないように思われるため、これは奇妙に思えますが、そうであるようです。

たとえば、次のコードを使用します。

int main (void)
{
    int a = 5;
    int b[1] = {6};
    int * pa = &a;
    int * pb = b;

    char c = (char) 0;
    char d[1] = {(char) 0};
    char * pc = &c;
    char * pd = d;

    *pa  = 6;       /*  maxSet warning  */
    *pb  = 7;       /*  No warning      */
    *b   = 8;       /*  No warning      */

    *pc = 'b';      /*  maxSet warning  */
    *pd = 'c';      /*  No warning      */
    *d  = 'd';      /*  No warning      */

    return 0;
}

スプリントは次の出力を提供します。

paul@thoth:~/src/sandbox$ splint -nof +bounds sp.c
Splint 3.1.2 --- 20 Feb 2009

sp.c: (in function main)
sp.c:15:5: Possible out-of-bounds store: *pa
    Unable to resolve constraint:
    requires maxSet(&a @ sp.c:7:16) >= 0
     needed to satisfy precondition:
    requires maxSet(pa @ sp.c:15:6) >= 0
  A memory write may write to an address beyond the allocated buffer. (Use
  -boundswrite to inhibit warning)
sp.c:19:5: Possible out-of-bounds store: *pc
    Unable to resolve constraint:
    requires maxSet(&c @ sp.c:12:17) >= 0
     needed to satisfy precondition:
    requires maxSet(pc @ sp.c:19:6) >= 0

Finished checking --- 2 code warnings
paul@thoth:~/src/sandbox$

ここで、(1 つの要素) 配列の最初の文字へのポインターを逆参照し、配列名自体を逆参照すると、どちらもエラーは発生しませんが、単一の変数を指すだけのポインターを逆参照すると、 forcharとの両方でエラーが発生しintます。奇妙な行動のように見えますが、それはそれです。

ちなみに、あなたの関数では、何を指しているのかをf()実際に推論することはできません。これらの 2 つの関数を単独で見ると、有効な参照であるべきものを指していることは明らかですが、splint が知る限り、他の翻訳単位からさらに多くの呼び出しを行うことができ、それはわかりませんそのような場合に何を指している可能性があるので、それ自体が持っている情報を使用する必要があります。resultmain()resultfresultf()

たとえば、ここに：

static void f(char * pc)
{
    if ( pc ) {
        *pc = 'E';      /*  maxSet warning  */
    }
}

int main(void)
{
    char c[25] = "Oysters and half crowns.";
    *c = 'U';           /*  No warning      */

    f(c);

    return 0;
}

splint は の代入について警告しますが、 の代入については警告しf()ませんmain()。まさにこの理由からです。ただし、注釈を付けると、それを理解するのに十分な情報が得られます。

static void f(char * pc) /*@requires maxSet(pc) >= 0; @*/
{
    if ( pc ) {
        *pc = 'E';      /*  No warning      */
    }
}

int main(void)
{
    char c[25] = "Oysters and half crowns.";
    *c = 'U';           /*  No warning      */

    f(c);

    return 0;
}

しかし、ここでもcsinglecharに変更すると、注釈付きの制約が満たされていることを splint が検証しないため、説明したのと同じ問題が発生するため、次のようになります。

static void f(/*@out@*/ char * pc) /*@requires maxSet(pc) >= 0; @*/
{
    if ( pc ) {
        *pc = 'E';      /*  No warning      */
    }
}

int main(void)
{
    char c;
    f(&c);              /*  maxSet warning  */

    return 0;
}

あなたにこれを与えます：

paul@thoth:~/src/sandbox$ splint -nof +bounds sp3.c
Splint 3.1.2 --- 20 Feb 2009

sp3.c: (in function main)
sp3.c:11:5: Possible out-of-bounds store: f(&c)
    Unable to resolve constraint:
    requires maxSet(&c @ sp3.c:11:7) >= 0
     needed to satisfy precondition:
    requires maxSet(&c @ sp3.c:11:7) >= 0
     derived from f precondition: requires maxSet(<parameter 1>) >= 0
  A memory write may write to an address beyond the allocated buffer. (Use
  -boundswrite to inhibit warning)

Finished checking --- 1 code warning
paul@thoth:~/src/sandbox$
于 2015-03-28T01:36:58.673 に答える