関数はインタフェースを通して呼び出し元の環境と情報交換を行います。 呼び出し元は、関数へ実引数とグローバル変数の値を伝え、 関数は戻り値とグローバル変数と実引数から到達可能な記憶領域を通して呼び出し元へ伝えます。 狭い（関数インタフェースをまたがって表示可能な情報の量を制限されている） インタフェースを保持することにより、 私たちは独立して関数を理解し、実装することが出来ます。
関数のプロトタイプは関数へのインタフェースを説明しています。 関数と呼び出し元の間の契約事項となっています。 C言語の初期のバージョンでは、関数の「プロトタイプ」は非常に制限されていました。 関数によって戻る型が記述されますが、引数については何も記述がありませんでした。 ANSI C (1989)は関数のプロトタイプに関数への引数の数と型についての情報を追加する機能を 提供しました。 Splintは、関数が使用するグローバル変数は何か？と、 関数が変更し、呼び出し元が見る値は何か？というような関数インタフェースについての 多くを表現する手段を提供します。
追加したインタフェースの情報は どのように関数が呼ばれるか？や、 どのように関数が実装されるか？の両方の制約を課します。 Splintはこれらの制約が満たされていない場所を報告します。 通常、コード内のバグかインタフェースの文書（訳注：恐らくアノテーションのこと）のエラーを示します。
このsectionでは 関数の実装が使用するグローバル変数が何であるか？と、 関数の実装が変更する、呼び出し元が見る値は何か？を文書化するために関数の宣言に 追加することが可能なアノテーションについて説明します。
変更句は、呼び出し側から見える値が関数によって変更されることを リスト化します。 変更句は関数が何の値を変更する可能性があるか？に制限をかけますが、 制限された値が常に変更されることを要求しません。 宣言、
は、 関数fが 第一引数で指し示されている値が変更されうること、しかし、 第二引数とどんなグローバルの状態も変更しないことを宣言します。
Splintは関数が 変更句に含まれない呼び出し側から見える値を変更しないこと、 関数のいくつかの可能な実行で、その修正句にリスト化された全ての値を 変更することをチェックします。 図12にSplintによる変更チェックの例を示します。
|
Running Splint | |
|
/*@modifies *x@*/ { 4 *y = *x; }
void sety (int *x, int *y) /*@modifies *y@*/ { setx (y, x); } |
> splint modify.c +checks modify.c:4: Undocumented modification of *y: *y = *x modify.c:5: Suspect object listed in modifies of setx not modified: *x modify.c:1: Declaration of setx
setyに対してのエラーはありません。 - setxへの呼び出しは変更区によってドキュメント化されている第一引数（y）が指す値を変更します。 checksモードがmustmodチェックになっているため、 ドキュメント化された変更がされていないことに関する2番目のエラーが報告されています。 |
|
図 12. 変更 |
引数あるいはグローバル変数を通して 識別できない結果をもたらす関数の変更を記述するために いくつかの特別な名前が提供されています：
internalState
fileSystem
nothing
アノテーション、関数の宣言あるいは定義の中にある/*@*/ （引数リストの後ろで、セミコロンあるいは関数本体の前にある）は、 何も変更せず、どのグローバル変数も使用しない関数（Section 7.2参照）であることを示します。
Splintは、変更句無しで宣言された多くの関数を持つ プログラムが効果的にチェックされるように設計されています。 modnomodsがオンになっていない限り、 変更句無しで宣言された関数をチェックし、 変更エラーが報告されることは、ありません。
変更句が無い関数は何が変更されうるかについての 制約が文書化されていないため、unconstrained（制約が無い）関数です。 制約が無い関数が呼び出された場合、変更句で宣言された関数とは異なるチェックがされます。 偽のエラーを防ぐため、 mod-uncon フラグがオンでなければ、呼び出し側で、変更エラーは報告されません。 フラグは、制約が無い関数を含むエラーが変更（副作用の無いマクロの引数（Section 11.2.1）、評価順（Section 8.2）、無限ループの可能性（Section 8.3.1））に依存する他のチェックにより 報告されるかどうかを制御します。
関数インタフェースのもうひとつの側面は それが使用するグローバル変数です。 関数の宣言中でのグローバルリストは関数本体にて使用される 外部変数の一覧を示します。 Splintは処理手順の中で使用されているグローバル変数がそのグローバルリストでリスト化された それと一致していることをチェックします。 グローバル変数が関数本体で直接現れるか、関数本体で呼び出された関数のグローバルリストに ある場合、グローバル変数が関数の中で使用されています。 Splintは、処理手順の中で使用されているグローバル変数がグローバルリストの中に入っていない場合、 及び、リスト化されたグローバルが関数の実装にて使用されていない場合、報告を行います。 図13は、Splintによって行われるグローバルリストによる関数宣言の例と関連するチェック を示しています。
|
globals.c |
Running Splint |
|
int glob1, glob2;
3 int f (void) /*@globals glob1;@*/ { 5 return glob2; } |
> splint globals.c +checks
globals.c:3: Global glob1 listed but not used
|
|
図 13. グローバル変数 |
与えられた関数の中でのグローバル変数の使用に対してエラーが報告されるかどうかは、 変数のスコープ（ファイル静的（file static）、又は、外部（external））と、 変数宣言で使用されたアノテーションあるいはアノテーションチェックが使用されない場合は暗黙のアノテーションのチェックと、 関数がグローバルリストとともに宣言されたかどうかと、 フラグの設定に依存します。
グローバルあるいはファイル静的変数の宣言は 変数がチェックされるべきかどうかを示すためのアノテーションが付く場合があります。 チェックを減らすために、以下のアノテーションがあります。
/*@checkedstrict@*/
/*@checked@*/
/*@checkmod@*/
/*@unchecked@*/
変数がこれらのアノテーションのどれも持っていない場合、 暗黙のアノテーションがフラグの設定により決定されます。
別のフラグは グローバルスコープで宣言された変数とファイルスコープ（すなわち、static記憶修飾子を使用している）で宣言された変数 に対しての暗黙のアノテーションを制御します。 context （ 外部変数に対するglobsと ファイル静的変数に対するstatics ）の中で宣言されるグローバル変数に対しての暗黙のアノテーションを annotation (checked、 checkmod、 checkedstrict) に設定するためには、imp <annotation> <context>を使用してください。 例えば、+imp-checked-strict-statics は、修飾されていないファイル静的変数についての暗黙的なチェックを checkedstrictとします。 グローバル変数チェックのフラグの完全な一覧についてはAppendix Bを参照してください。
アノテーションは関数呼び出しの前後でのグローバル変数の状態を 記述するために関数宣言のグローバルリストにて使用することが出来ます。 グローバル変数にundefアノテーションが付いている場合、 呼び出し前は未定義であると想定されます。 このように、関数が呼び出されたときにグローバル変数が未定義の場合は エラーは報告されませんが、しかし、定義される前に関数の本体で グローバル変数が使用された場合はエラーが報告されます。 killedアノテーションは 呼び出しが戻ってきたときに未定義になるグローバル変数を表します。 動的に割り当てられる記憶領域を含むグローバル変数に対して、 killedグローバル変数は only引数（Section 5.2参照） と同様です。 呼び出しが帰る前に解放されていない記憶領域への参照のみ含む場合、 エラーが報告されます。 図14にkilledとundefグローバル を示しました。
|
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
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. アノテーション付きのグローバルリスト |
後の宣言は最初の宣言で含まれていない グローバルリスト内の変数を含めることは出来ません。 最初の宣言がヘッダファイルにあり、かつ、後の宣言か定義が ファイル静的変数を含む場合は、これの例外となります。 これらは、ヘッダファイル内に現れないため、それらはヘッダファイルの宣言内に 含めることは出来ません。 同様に、後の宣言での変更句は、最初の宣言内での変更不能なオブジェクトを含めることは出来ません。 後の宣言はより具体的にしてもかまいません。例えば、もし、ヘッダファイル内に：
とあった場合に、後の宣言は以下のようにすることが出来ます。
employeeが抽象型の場合、 ヘッダー内の宣言は特定の実装を参照すべきではありません （すなわち、nameフィールドに依存すべきではありません）、 しかし、実装の宣言はより具体的に指定することが可能です。
このルールはファイル静的変数へも適用されます。 ファイル静的変数を変更する関数に対してのヘッダでの宣言は、 modifies internalStateアノテーションを使用する必要があります。 なぜなら、ファイル静的変数は、クライアントからは見えないためです。 実装宣言は変更される可能性のある実際のファイル静的変数をリスト化する必要があります。
時には、 標準的なアノテーションで可能であるよりも低いレベルで関数インタフェース を指定する必要があります。例えば、関数が返される構造体のいくつかのフィールド を定義しているが、全てのフィールドは定義していない場合です。 /*@special@*/アノテーションは 状態句を使用して記述される 引数、グローバル変数、あるいは戻り値をマークするために使用されます。
状態句は関数の呼び出しの前あるいは後の引数や戻り値の 状態を制限するために使用することが出来ます。 1つ以上の状態句が、変更句やグローバル句の前に、関数の宣言に現れてもかまいません。 状態句は任意の順で一覧にされてもかまいませんが、同じ状態句を複数回使用することは出来ません。 状態句の中で、resultは 関数の戻り値を示すために使用されます。
以下の状態句は、定義状態、あるいは、関数の呼び出し前後の引数と関数から返った後の戻り値、 を記述するために使用されます。
/*@uses <references>@*/
/*@sets <references>@*/
/*@defines <references>@*/
/*@allocates <references>@*/
/*@releases <references>@*/
状態句のいくつかの例を図15に示します。record_newに対するdefines句は戻り値によって示される構造体のidフィールドが定義されることを示します。 しかし、nameフィールドは 定義されません。そのため、record_createはnameフィールドを定義するために record_setNameを呼び出す必要があります。同様に、record_clearNameに対するreleases句 は、戻った後で、その引数のnameフィールドにて 割り当てられている記憶領域が無いことを示します。なぜなら、 record_free内のfreeへの呼び出しに対して、 記憶領域の返却失敗のメッセージは生じることが無い為です。 ensures isnull句は次のsctionで説明します。
|
clauses.c |
|
typedef struct { int id; /*@only@*/ char *name; } *record;
static /*@special@*/ record record_new (void) /*@defines result->id@*/ { record r = (record) malloc (sizeof (*r));
assert (r != NULL); r->id = 3; return r; }
static void record_setName (/*@special@*/ record r, /*@only@*/ char *name) /*@defines r->name@*/ { r->name = name; }
record record_create (/*@only@*/ char *name) { record r = record_new (); record_setName (r, name); return r; }
void record_clearName (/*@special@*/ record r) /*@releases r->name@*/ /*@ensures isnull r->name@*/ { free (r->name); r->name = NULL; }
void record_free (/*@only@*/ record r) { record_clearName (r); free (r); }
|
|
図 15. 状態句 |
関数の呼び出し前後の引数とグローバル変数の状態について より一般的な仮定は、requires句とensures句を使用して記述可能です。 requires句は 呼び出し側で真になる必要のある述部を指定しま。すると、関数の実装をチェックし、 関数の入り口でそのrequires句で与えられた制約が真になると Splintが仮定します。ensures句は 呼び出しが戻った後で呼び出し側にて真である述部を指定します。 すると、関数の実装をチェックし、そのensures句の中で与えられた制約 を満足する状態で戻らない実行経路が存在するときにSplintが警告を発します。 関数の宣言は、その意味が矛盾しない限り、多くのrequires句とensures句 を持つことが出来ます。
以下の制約はrequires句とensures句を使用して 定めることが出来ます。
/*@requires only<references>@*/; /*@ensures only<references>@*/
/*@requires shared<references>@*/; /*@ensures shared<references>@*/
/*@requires owned<references>@*/; /*@ensures owned<references>@*/
/*@requires dependent<references>@*/; /*@ensures dependent<references>@*/
/*@requires observer<references>@*/; /*@ensures observer<references>@*/
/*@requires exposed<references>@*/; /*@ensures exposed <references>@*/
/*@requires isnull<references>@*/; /*@ensures isnull<references>@*/
/*@requires notnull<references>@*/; /*@ensures notnull<references>@*/
このドキュメントはSplint(英)のサイトを元に作成しました
[PageInfo]
LastUpdate: 2014-02-11 15:05:53, ModifiedBy: daruma_kyo
[License]
Creative Commons 2.1 Attribution-ShareAlike
[Permissions]
view:all, edit:login users, delete/config:members
edit