sec3 - Splint翻訳 Wiki - Splint翻訳

Up: マニュアル

Prev: 2 Null Dereferences（NULLポインタへの値の参照）

Next: 4 Types（型）

Section：1　2　3　4　5　6　7　8　9　10　11　12　13　14　A　B　C　D　E

3 Undefined Values（未定義の値）

多くの静的チェックツール同様、Splintは 定義前に使用されている場所の値のインスタンスを検知します。 この解析は処理手順レベルで行われます。 もし、宣言される前にローカル変数を使用する処理手順を通るパスが存在する場合、 used before definition（定義前に使用された）エラーが報告されます。 usedefフラグが定義前の使用のチェックを制御しています。

Splintは標準的なチェックツールよりチェックを行うことが出来ますが、 これは、アノテーションが、何の記憶領域が定義されていなければならないか、 何の記憶領域がインタフェースポイントにて定義されていない可能性があるか、を記述するのに使用されるためです。 アノテーションが付いていない参照はインタフェースポイントにて完全に定義されていることと予想されます。 これは全てのグローバル変数から到達可能な記憶領域、関数への引数、あるいは、戻り値が関数呼び出し前後で定義される ことを意味します。

3.1.1 Undefined Parameters（未定義の引数）

時々、関数の引数、戻り値は未定義あるいは部分的に定義されている記憶領域を参照することが期待されています。 例えば、ポインタ引数は結果を格納するためのアドレスとしてのみの意図だったり、 メモリアロケータは割り当てられているが、定義されていない記憶領域を返すかもしれません。 outアノテーションは 定義されていない可能性のある記憶領域へのポインタを示します。

割り当てられているが未定義の記憶領域へのポインタがout引数に渡された場合、 Splintはエラーを報告しません。 関数の本体内ではSplintはoutは 割り当てられているが、必ずしも値へバインドしていないものとして想定します。 そのため、定義される前に値が使用されるとエラーが報告されます。

関数から返るとき、その呼出し後に呼び出し側から参照できる記憶領域が定義されていない場合 Splintはエラーを報告します。 これは-must-define により抑制可能です。 呼び出しが戻った後、out引数に対応する実引数 は完全に定義されているものとして想定されます。

アノテーションが付いてないプログラムをチェックするとき、 たくさんの偽use before definition（定義前の使用）エラーが報告される可能性があります。 impoutsフラグがオンの場合、 不完全定義引数がアノテーションで定義されていない仮引数に渡されたとき、 エラーは報告されませんし、実引数は呼出し後に定義されると想定されます。 imp-outsフラグがオンのときでも、/*@in@*/アノテーションは 完全に定義される必要のある引数を表すために使用することができます。 imp-outsがオフのとき、 アノテーションの定義がない全ての引数はinアノテーションが暗黙的にあります。

usedef.c

Running Splint

extern void   setVal (/*@out@*/ int *x); extern int   getVal (/*@in@*/ int *x); extern int mysteryVal   (int *x);   int dumbfunc    (/*@out@*/ int *x, int i) {   if (i > 3) 11   return *x;   else if (i > 1) 13   return getVal (x);   else if (i == 0) 15   return mysteryVal (x);   else     { 18    setVal (x); 19    return *x;     } }

> splint usedef.c usedef.c:11: Value *x used before definition usedef.c:13: Passed storage x not completely defined                 (*x is undefined): getVal (x) usedef.c:15: Passed storage x not completely defined                 (*x is undefined): mysteryVal (x)   Finished checking --- 3 code warnings   18行目ではエラーは報告されません。なぜなら、不完全に定義された記憶領域 x が out 引数として渡されているためです。 呼出し後、 x は 参照先へアクセス可能でしょう。なぜなら、 setVal は完全に out引数を表すと仮定されているためです。 15行目の警告は +impouts が使用された場合は現れないでしょう。なぜなら、 mysteryValへの引数に in アノテーションが無い為です。

図 3.  定義前の使用

3.1.2 Relaxing Checking（チェックの緩和）

reldefアノテーションは 特定の宣言に対してチェックしている定義を緩くします。 reldefアノテーションで宣言された 記憶領域はそれが使用されたときに定義されるものとして想定されます。 しかし、関数から返されるか、引数として渡されるかする前に定義されていない場合 エラーは報告されません。

reldefフィールドが 正しく使用されていることをチェックするのはプログラマの責任です。 それらは多くの場合、避けるられるべきですが、そのほかの制約により 定義されているか、されていないかわからない構造体のフィールドに対しては 役に立つかもしれません。

3.1.3 Partially Defined Structures（部分的に定義された構造体）

partialアノテーションは 構造体フィールドのチェックを緩めるために使用できます。 未定義のフィールドを持つ構造体はpartial引数として渡されたり、あるいは、 partial戻り値として返されたりする場合があります。 関数の本体内部ではpartial 構造体のフィールドが 使用されたときエラーは報告されません。 呼び出しの後、partial引数として渡された 構造体の全てのフィールドは完全に定義されていると想定されます。

このドキュメントはSplint(英)のサイトを元に作成しました

Up: マニュアル

Prev: 2 Null Dereferences（NULLポインタへの値の参照）

Next: 4 Types（型）