Splintはスタック変数へのポインタのmaxSetをチェックできません

私の知る限り、スプリントは、実際のバッファーまたは配列を検証可能に指していないポインターでは制約を検証できないと報告しています。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$ 

（一つの要素）の配列の最初の文字へのポインタを間接参照し、配列名自体を逆参照、両方のエラーを生じないが、の両方、ない単一の変数にだけポイントポインタ間接参照場所charとをint。奇妙な振る舞いのように見えますが、それはそれが何であるかです。

ちなみに、あなたのf()関数では、で何をresult指しているのかを実際に推論することはできませんmain()。これらの2つの関数を分離しresultて見ると、スプリントが知る限り、有効な参照となるはずのものを指していることは明らかですがf、他の翻訳ユニットからさらに多くの呼び出しが行われる可能性があり、それはわかりません。何がresult中を指している可能性があり、それらのそれはちょうどそれがために持っている情報で行かなければならないので、場合によってf()、それ自体の。

たとえば、ここで：

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

スプリントは、の割り当てについて警告しますが、の割り当てについては警告し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;
}

ただし、ここでもc、単一charに変更すると、スプリントは注釈付き制約が満たされていることを確認しないため、説明したのと同じ問題が発生します。したがって、次のようになります。

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$