トップC-Tips > splint(C言語ソースコード静的解析ツール)

splint(C言語ソースコード静的解析ツール)

splint(Secure Programming Lint) のインストール方法は別のページに記述したので省略する。 このページには、マニュアル[1][2]を参照しながら、splintの使い方の要点をまとめる。

2.Null Dereferences(NULLポインタへの値の参照)

nullアノテーションは ポインタの値がNULLである可能性があることを示すために使用される。

notnullアノテーションは宣言が明確にNULLではないことを示す。 デフォルトではこれが指定される。 しかし、型宣言上でnullを上書きするためにnotnullを使用する必要がある場合もある。

5.Memory Management(メモリ管理)

5.1 Storage Model(記憶領域モデル)

記憶領域に値が割り当てられていない場合、それは未定義である。 値が割り当てられた後は、定義されている。 記憶領域から到達可能な全てのそれが定義されている場合、オブジェクトは完全に定義されている。 どのような記憶領域がオブジェクトから到達可能なのかは、オブジェクトの型と値に依存する。 例えば、pが構造体へのポインタの場合、pの値がNULLであるか、 pが指す構造体の全てのフィールドが 完全に定義されている場合にpは完全に定義されている。

ポインタは型指定されたメモリのアドレスである。 ポインタは生きている(live)か、死んでいる(dead)のどちらかである。 生きているポインタはNULLか、 割り当てられている記憶領域内のアドレスである。

5.2 Deallocation Errors(解放エラー)

5.2.1 Unshared References(共有されていない参照)

onlyアノテーションは、 参照が、そのオブジェクトへの唯一のポインタであることを示すために使用される。 このような参照は記憶領域を返却する責務を持っている。 この責務は以下の3つのうちの1つの方法により、他の参照へ移すことにより果たされる。

責務の返却が移った後、元の参照は死んでいるポインタとなり、 それが指す記憶領域は使用することはできない。

記憶領域を返却する全ての責務は、 基本割り当てルーチン(例えば、malloc)に由来し、 最終的にはfreeの呼び出しによって果たされる。 基本的なメモリ割り当て関数、mallocは以下のように宣言される。

/*@only@*/ /*@null@*/ void *malloc (size_t size); 
関数の戻り値によって参照されるオブジェクトを返す。

解放関数、freeは以下のように宣言される。

void free (/*@only@*/ /*@out@*/ /*@null@*/ void *ptr); 

次のプログラムは standardモードでは警告は一切でない。 hfree関数の引数に付けた outアノテーションは無くても警告は出なかった。 この outアノテーションの役割は後で調べよう。

#include <stdlib.h>

typedef struct { 
    int key;
    int sqn;
} Data;

typedef struct {
    int   size, nData;
    Data  data[0];
} Hash;

/*@only@*/ /*@null@*/static Hash *halloc(size_t size) {
    return (Hash *)calloc(1, sizeof(Hash) + size * sizeof(Data));
}

void static hfree(/*@only@*/ /*@out@*/ /*@null@*/Hash *pHash) {
    free(pHash);
}

int main() {
    Hash *pHash = halloc(100);
    hfree(pHash);
    return 0;
}

pHashをグローバル変数とするときには、次のようにすれば standardモードでは警告が出ない。

/*@only@*/ /*@null@*/static Hash *pHash;

int main() /*@globals undef pHash@*/ {
    pHash = halloc(100);
    hfree(pHash);
    pHash = NULL;
    return 0;
}

上で定義したHash構造体は末尾要素を可変長配列としている。 別の定義方法として、次のようにする方法がある。

typedef struct {
    size_t size;
    int    nData;
    Data  *data;
} Hash;

プログラム全体を下に示す。 Hash構造体領域の獲得とData構造体領域の獲得が必要となるため、 プログラム行数は若干増加する。

#include <stdlib.h>

typedef struct { 
    int key;
    int sqn;
} Data;

typedef struct {
    size_t size;
    int    nData;
    /*@only@*/ /*@null@*/Data  *data;
} Hash;

/*@only@*/ /*@null@*/
static Hash *halloc(size_t size) {
    Hash *pHash = malloc(sizeof(Hash));
    if (pHash == NULL) return NULL;
    pHash->data = calloc(size, sizeof(Data));
    pHash->size = size;
    pHash->nData = 0;
    return pHash;
}

void static hfree(/*@only@*/ /*@null@*/Hash *pHash) {
    if (pHash != NULL) free(pHash->data);
    free(pHash);
}

/*@only@*/ /*@null@*/
static Hash *pHash;

int main() /*@globals undef pHash@*/ {
    pHash = halloc((size_t)100);
    hfree(pHash);
    pHash = NULL;
    return 0;
}
 extern /*@null@*/ /*@only@*/ void *
   realloc (/*@null@*/ /*@only@*/ /*@out@*/ /*@returned@*/ void *p, size_t size)
      /*@modifies *p, errno @*/ /*@ensures MaxSet(result) == (size - 1) @*/;

5.3 Implicit Memory Annotations(暗黙的なメモリアノテーション)

アノテーションが無い関数の引数はtempであると仮定される。

いくつかの暗黙的なアノテーションを以下に示す。 フラグの設定状態により、暗黙的に太字のアノテーションが付いているものとみなされる。

typedef struct {
   only char *name;
   int   val;
} *rec;

extern only rec rec_last ;

extern only rec rec_create (temp char *name, int val) ;

アノテーションの無い戻り値、構造体フィールド、そしてグローバル変数は onlyであると仮定される。

7.Function Interfaces(関数インタフェース)

7.1 Modifications(変更)

宣言、

int f (int *p, int *q) /*@modifies *p@*/; 
は、 関数 f が 第一引数で指し示されている値が変更されうること、 しかし、 第二引数とどんなグローバルの状態も変更しないことを宣言する。

7.2 Global Variables(グローバル変数)

strictモードでは、グローバル変数を使用するとき、globalsアノテーションを付ける。 但し、standardモードでは、globalsアノテーションを付けなくても警告は出ない。

static int glob1 = 1, glob2 = 2;

int main(/*@unused@*/int argc, /*@unused@*/char *argv[]) /*@globals glob1, glob2@*/
{
   int n = glob1 + glob2;
   return n;
}

グローバル変数を修正する場合には、次の例に示すように、modifiesアノテーションを付加する。 但し、standardモードでは、globalsアノテーションと同様にmodifiesアノテーションを付けなくても警告は出ない。

static int glob1 = 1, glob2 = 2;

int main(/*@unused@*/int argc, /*@unused@*/char *argv[]) 
/*@globals glob1, glob2@*/ /*@modifies glob1@*/ 
{
   glob1 += glob2;
   return 0;
}

globals と modifies がないときの省略形は /*@*/ である。

7.2.2 Definition State(定義状態)

グローバル変数にundefアノテーションが付いている場合、 呼び出し前は未定義であると想定される。 定義される前に関数の本体で グローバル変数が使用された場合はエラーが報告される。

killedアノテーションは 呼び出しが戻ってきたときに未定義になるグローバル変数を表す。

            annotglobs.c

Running Splint

int globnum;

 

struct {

  char *firstname, *lastname;

  int id;

} globname;

 

void

initialize (/*@only@*/ char *name)

  /*@globals undef globnum,

             undef globname @*/

{

13 globname.id = globnum;

  globname.lastname = name;

15}

 

void finalize (void)

  /*@globals killed globname@*/

{

  free (globname.lastname);

21 }

> splint annotglobs.c

 

annotglobs.c:13: Undef global globnum used

                    before definition

annotglobs.c:15: Global storage globname

    contains 1 undefined field when call

    returns: firstname

annotglobs.c:21: Only storage

    globname.firstname (type char *) derived

    from killed global is not released

    (memory leak)

図 14.  アノテーション付きのグローバルリスト

7.4 State Clauses(状態句)

specialアノテーションは 状態句を使用して記述される 引数、グローバル変数、あるいは戻り値をマークするために使用される。 状態句は関数の呼び出しの前あるいは後の引数や戻り値の 状態を制限するために使用することが出来る。

状態句の中で、resultは 関数の戻り値を示すために使用される。

以下の状態句は、定義状態、あるいは、関数の呼び出し前後の引数と関数から返った後の戻り値、 を記述するために使用される。

/*@uses <references>@*/

uses句の中の参照は、関数が呼ばれる前に完全に定義されていなければならない。

/*@sets <references>@*/

sets句の中の参照は関数が呼ばれる前に割り当てられていなければならない。 記憶領域は未定義であると仮定される。 それらは、関数が戻った後は完全に定義されている。

/*@defines <references>@*/

defines句の中の参照は関数の呼び出し前では未共有の割り当てられている 記憶領域を参照してはならない。それらは関数の呼び出しの後で完全に定義される。

/*@allocates <references>@*/

allocates句の中の参照は関数呼び出し前で未割り当てである必要がある。 それらは関数が戻った後に割り当てられているが、必ずしも定義されているとは限らない。

/*@releases <references>@*/

releases句の中の参照は関数によって解放される。 それらは関数が呼ばれる前にonly引数として渡される記憶領域である必要がある。 そして、関数から戻った後は死んでいるポインタとなる。 それらは関数の入り口で定義されていると仮定される。

8.Control Flow(制御フロー)

8.1 Execution(実行)

追加の情報がない場合、Splintは全ての関数は最終的に戻り、 実行が呼び出し側では 正常に継続するものと想定する。

noreturnアノテーションは 決して戻ることがない関数を示すために使用される。 例えば、

  extern /*@noreturn@*/ void fatalerror (/*@observer@*/ char *s); 

つまり、次の error関数には noreturnアノテーションを付けよ、ということである。 observerアノテーションについては後で調べよう。

vprintf関数の戻り値は使用していないので キャスト(void)を付けないと、Splintは警告を出す。

/*@noreturn@*/ void error(const char *format, ...) {
    va_list arg;
    va_start(arg, format);
    (void)vfprintf(stderr, format, arg);
    va_end(arg);
    exit(EXIT_FAILURE);
}

maynotreturn アノテーションは関数が戻ったり、戻らなかったりする場合があることを示す。 ドキュメントとしては役立つが、Splintのチェックにはあまり役に立たない。


参考文献

[1] Splint Manual(Version 3.1.1)
[2] Splint翻訳