強力な型チェックは、しばしば、プログラミングエラーを 明らかにします。 Splintは典型的なコンパイラ(4.1)よりも厳密かつ柔軟にC言語基本型をチェックすることが出来、 真偽型(4.2)のサポートを提供します。さらに、ユーザは 情報隠蔽を提供する抽象型を定義することが出来ます(0)。
2つの型が同じである場合、それらには compatible （互換性のある）型があります。
ANSI C, 3.1.2.6.
SplintはC言語組込みの型の厳格なチェックをサポートします。charとenum型 は異なる型のようにチェックでき、様々な数値型は、厳密に型チェックすることができます。
基本char型は 特殊タイプとして型チェックすることができます。charが特殊タイプとして使用される場合、 charsにintsの割り当てを伴う一般的なエラーが検出されます。
+charintフラグはcharとintが交換できるように使用される従来のプログラム をチェックするために使用されます。 charintがオンの場合、charはintから区別できないものとして区別します。 charとint異なる型のままとするためには、 しかし、charの配列要素への使用を許してしまいますが、+charindexを使用してください。
標準C言語はちょうど整数と同じようなユーザ宣言のenum型を扱います。 列挙メンバーとしてリスト化されてるかどうかに関係なく、任意の整数値がenum型に割り当てられている可能性があります。 Splintは異なる型としてそれぞれのユーザ宣言のenumをチェックします。 列挙メンバーではない値がenum型に割り当てられたとき、 もしくは、enum型が算術演算子へのオペランドとして使用された場合、 エラーが報告されます。 enumintフラグがオンになっていれば、enum型とint型は 互換的に使用されてもかまいません。 charindexと同じように、enumindexフラグがオンの場合、enum型は配列の要素として使用されてもかまいません。
Splintは数値型が危険あるいは矛盾した方法で使用されている場所を報告します。 厳しいチェックにより、Splintは数値型が完全にマッチしていない、どんな時でも、エラーを報告します。 relax-qualsフラグがオンの場合、 値が間違っている可能性のある矛盾のみが報告されます。 例えば、intがlong型の変数へ割り当てられた場合（もしくはlongの仮引数に渡された場合）、 Splintはrelax-qualsがオンのときには エラーを報告しません。なぜなら、longは少なくともデータロスすることなく intを格納するのに十分なビットを持っていなければならないためです。 それに引き換え、int型はlong値 を格納する十分なビットを持っていないため、longがintへ割り当てられた場合はエラーが報告されます。
同様に、signed（符号ありの）値がunsigned（符号なし）へ割り当てられた場合、 unsigned（符号なし）型は全てのsigned（符号ありの）値を正確に表現できるとは限らないため、 Splintはエラーを報告するでしょう。 +ignore-signsフラグがオンの場合、チェックは、 型比較において全ての符号を限定するものを無視することで、緩和されます （これは、本当のバグの報告を隠してしまうため、推奨されません。しかし、ある程度の過去のソースを 素早くチェックするためには必要でしょう）。
いくつかの型は整数型であると宣言されていますが、 実際の型は実装依存の可能性があります。 例えば、標準ライブラリは型、size_t、ptr_diffとwchar_tを宣言しています。 しかし、それらを整数型に制限する以外に型を強制させていません。 プログラムはそれらが数値型であることに依存しても良い （例えば、2つのsize_tデータに対して+演算子を使用できる）のですが、 特定の表現に依存すべきではありません （例えば、long unsigned（符号なしのlong型））。
Splintは3つの異なる種類の任意の整数型をサポートしています。
/*@integraltype@*/
/*@unsignedintegraltype@*/
/*@signedintegraltype@*/
コードが任意の整数型として宣言された型の実表現に依存している場合、 Splintはエラーを報告します。match-any-integralフラグは チェックを緩和し、任意の整数型がどのような整数型にも一致するように許されることを 許します。
他のフラグは任意の整数型を実際の型へ設定します。 異なる表現を使用する可能性のあるプラットフォームへの移植が重要ではない場合のみ、 これらは使用されるべきでしょう。 long-integralとlong-unsigned-integralフラグはそれぞれ、/*@integraltype@*/をunsigned longとlongに相当する型に設定します。 long-unsigned-unsigned-integralフラグは/*@unsignedintegraltype@*/をunsigned longに相当する型に設定します。 long-signed-integralフラグは/*@signedintegraltype@*/をlongに相当する型に設定します。
ISO99以前のC言語は真偽値の表現がありませんでした。 –比較演算子の結果は整数値であり、判別式に対して型チェックは行われませんでした。 C99は真偽値型（stdbool.hにて_Boolとbool、trueとfalseマクロ）を導入しましたが、 型チェックを強化しませんでした。 Splintは整数型から明白にチェック可能な真偽値型をサポートします。 多くの一般的なエラーは異なる真偽値型と強力な型チェックを導入することにより 検出することが出来ます。
Splintはif、while、もしくはforステートメントの中、あるいは、 &&、||、もしくは、!算子のオペランドの中の判別式が 真偽値であることをチェックします。 判別式の型が真偽値ではない場合、Splintは判別式の型とフラグの設定に依存する警告を表示します。 判別式がポインタ型の場合、警告は-predboolptrによって抑制されます （これはポインタをnullとの比較なしで判別する習慣に対して、メッセージを抑制するのに使用されます）。 intの場合、警告は-pred-bool-intによって抑制されます。 他のすべての型に対しては、-pred-bool-othersが設定されていない限り、 Splintは警告を行います。 関係式、比較、特定の標準関数は真偽値型を返すように宣言されています。
==の代わりに=を使用することは 非常に良くあるバグであるため、代入している判別式の報告はpred-assignラグにより制御できます。 メッセージは判別式の周りに余計な括弧を追加することにより抑制することが出来ます。
真偽値を表現するために使用される型名を選択するためには-booltypeフラグを使用して下さい。 習慣でboolが使用されますが、デフォルトの真偽値型はありません。 TRUEとFALSEの名前は は真と偽の真偽値を表現すると想定されています。 真と偽の名前を変更するためには、-booltrueと-boolfalseを使用して下さい。 （Splintの配布物にはlib/bool.hの中にboolの実装が含まれています。 しかし、真偽値チェックのメリットを得るためにはこの実装を使用する必要はありません。）
図 4はSplintによって行われる真偽値チェックの一部を示しています。
|
bool.c |
Running Splint |
|
# include "bool.h" int f (int i, char *s, bool b1, bool b2) { 6 if (i = 3) 7 return b1; 8 if (!i || s) 9 return i; 10 if (s) 11 return 7; 12 if (b1 == b2) 13 return 3; 14 return 2; } |
> splint bool.c +predboolptr –booltype bool
bool.c:6: Test expression for if is assignment expression: i = 3 bool.c:6: Test expression for if not bool, type int: i = 3 bool.c:7: Return value type bool does not match declared type int: b1 bool.c:8: Operand of ! is non-boolean (int): !i bool.c:8: Right operand of || is non-boolean (char *): !i || s bool.c:10: Test expression for if not bool, type char *: s bool.c:12: Use of == with bool variables (risks inconsistency because of multiple true values): b1 == b2
Finished checking --- 7 code warnings found |
|
図 4. 真偽値チェック |
情報隠蔽は複雑さを処理するための技術です。 実装の詳細を隠すことにより、プログラムは理解され、個別のモジュール、 にて開発され、変更の影響が局所化されます。 情報隠蔽する１つの技術は、データの抽象化です。 抽象型はある自然なプログラムの抽象化を表すために使用されます。 型のインスタンスを操作するための関数が提供されます。 これらの関数を実装するモジュールをimplementation（実装）モジュール と呼びます。 我々は抽象型のそのoperations（操作）の実装の一部である関数を呼び出します。 抽象型を使用する他のモジュールはclients（クライアント）と呼ばれます。
クライアントは型名と操作を使用するかもしれませんが、 型の実際の表現を操作したり、それに依存してはなりません。 実装モジュールだけは抽象型の実際の表現を操作してかまいません。 実装者とクライアントモジュールの保持者 が抽象型がどうやって実装されたかについて一切知る必要が無いため、これは情報を隠蔽します。 抽象型の実際の表現をクライアントコードへの変更無しに可能なため、 モジュール性がもたらされます。
Splintは抽象型の実際の表現に依存するクライアントコードが ある場所を検知することにより、抽象型をサポートしています。 Splintにより検知された抽象違反のいくつかの例を図5に示します。
抽象型を宣言するためにabstractアノテーションがtypedefに追加されます。 例えば（mstring.hの中）、
抽象型としてmstringを宣言しています。 char *を使用して実装されていますが、しかし、 型のクライアントはこれに依存するすべきではなく、また、知る必要もありません。 後で、文字列テーブルとして、より良い表現が使用されるべきであることが明らかになった場合、 どのクライアントコードも変更、検査をすることなく、mstringの実装を変更できるはずです。
クライアントモジュールでは、抽象型は構造ではなく名前によりチェックされます。 mstringのインスタンスがchar *として（例えばstrlenへの引数として）渡された場合、 Splintはエラーを報告します。なぜなら、この呼び出しの正しさは抽象型の実際の表現に依存する ためです。代入（=とsizeofを除くC言語の演算子が抽象型に使用された場合も、 Splintはエラーを報告します。 代入演算子が許可されるのは、そのセマンティクスが型の表現に依存していないためです （インスタンスが値が変更可能である抽象型に対して、 代入がSection 4.3.2で説明するコピーあるいは共有セマンティクスを持つ場合、 クライアントは知る必要が無い）。 sizeofの使用も許可されるのは これが、抽象型へのポインタを割り当てるためにクライアントに対する唯一の方法であるためです。 クライアントモジュールでの抽象型への、あるいは、からの、オブジェクトのキャストは 抽象違反であり、警告メッセージを生成するでしょう。
通常、Splintは/*@abstract@*/修飾子が使用されていない限りは型定義が抽象ではないと想定します。 代わりに、concrete（具象）アノテーション としてマークされない限りはユーザ定義型を抽象型としたい場合は、 +imp-abstractフラグが使用できます。 これは、/*@concrete@*/でマークされていない 全てのtypedefに 暗黙のabstractアノテーション を追加します。
|
palindrome.c |
Running Splint |
|
# include "bool.h" # include "mstring.h"
bool isPalindrome (mstring s) { 6 char *current = (char *) s; 7 int i, len = (int) strlen (s);
for (i = 0; i <= (len+1) / 2; i++) { 11 if (current[i] != s[len-i-1]) return FALSE; } return TRUE; }
bool callPal (void) { 19 return (isPalindrome ("bob")); } |
> splint palindrome.c
palindrome.c:6: Cast from underlying abstract type mstring: (char *)s palindrome.c:7: Function strlen expects arg 1 to be char * gets mstring: s palindrome.c:11: Array fetch from non-array (mstring): s[len - i - 1] palindrome.c:19: Function isPalindrome expects arg 1 to be mstring gets char *: "bob"
Finished checking --- 4 code warnings
|
|
図 5. 情報隠蔽違反 |
伝統的に、それらが抽象データ型の話題になったとき、プログラミングの書籍は数学的になっていく・・・。
このような書籍はあなたが、睡眠補助薬としてを除き、実際に抽象データ型を使用したことが無い様に思えるようにする。
McConnell
コードが抽象型の実表現を操作する可能性のある場所を、 我々はコードはその型へのaccess（アクセス）権があると言います。 コードが抽象型へアクセス権がある場合、型の実表現と抽象型は区別が付きません。 通常、単一のプログラムモジュール（実際の型表現へのアクセス権を持つコードのみのモジュール）が抽象型を実装します。 時には、抽象型の実装が複数のプログラムファイルにまたがって分割されている場合や 特定のクライアントコードが実表現にアクセスする必要がある場合は、 より複雑なアクセス制御が望ましいです。
何のコードが抽象型の実表現へのアクセス権があるかを選択する方法は いくつかあります。
我々はmutable（ミュータブル、可変）または、 immutable（イミュータブル、不変）であると型を表示することが出来ます。 関数の呼び出しの引数として渡すと、型のインスタンスの値が変更されうる場合、 型はミュータブル（可変）です。 例えば、基本型intはイミュータブル（不変）です。 iが型intのローカル変数で、 どの変数もiが格納されている場所を指していない場合、 iの値は、f (i)の呼び出しの前後で同じ値にならなければなりません。 構造体と共用体（Union）型もイミュータブル（不変）です。なぜなら、 引数として渡されたとき、コピーされるためです。 これに反して、ポインタ型はミュータブル（可変）です。 もし、xが型int *のローカル変数である場合、*x の値（そして、その結果として、オブジェクトxの値） は関数呼び出しg(x)により変更される可能性があります。
具象型（訳注：concrete type。インスタンスを生成できる型のこと）の可変性は その型の定義によって決まります。抽象型については、可変性は型の実表現に依存するのではなく、 型が提供する操作するものに依存します。 もし、抽象型が型のインスタンスの値を変更する可能性のある操作を持っている場合、 その型はミュータブル（可変）です。 そうでなければ、イミュータブル（不変）です。 イミュータブル（不変）型のインスタンスの値は、決して変更しません。 オブジェクトの共有はミュータブル（可変）型に対してのみ重要であるため、 イミュータブル（不変）型とは違い、チェックされます。
/*@mutable@*/と/*@immutable@*/アノテーションはミュータブル（可変）あるいはイミュータブル（不変）として 抽象型を宣言するために使用します。 （もし、どちらも使用されない場合、抽象型はミュータブル（可変）であると想定されます） 例えば、
ミュータブル（可変）抽象型としてmstringを、 イミュータブル（不変）抽象型としてweekDayを宣言します。
ミュータブル（可変）抽象型のクライアント（使用者）は 割り当てのセマンティクスを知っている必要があります。 代入式s = tの後、sとtは 同じオブジェクトを参照します（つまり、sの値の変更は、tの値も変更します。）
Splintは全ての抽象型が共有セマンティクスを持つと定めますので、sとtは 実際に同じオブジェクトでしょう。 ミュータブル（可変）型が共有セマンティクス（mutrepフラグにより制御される）を提供していない実表現（例えば、struct）で実装されている場合、 Splintは警告を生成します。
抽象型の可変性は必ずしもその実表現の可変性と同じであるとは限りません。 我々は、文字列テーブルへのインデックスを使用して可変文字列を表現するために イミュータブル（不変）具象型intを使用するかもしません。 もしくは、mstringの値を修正することを提供されている操作が無い限り イミュータブル（不変）としてmstringを宣言するかもしれません。
時々、いくつかの方法により抽象型を持つことが便利な場合がありますが、 標準の数値演算子を使用する場合があります。 Splintはこの目的のために数値抽象型をサポートします。 /*@numabstract@*/アノテーションは数値抽象型を示します。 Splintは数値抽象型が一貫して使用されるときは警告を報告しますが、 2つの同じ数値抽象型の値を操作するためのバイナリ数値操作を許可します。 複数のフラグが数値抽象型に対する型チェックの厳格さを制御します： numabstract、numabstractcast、numabstractlit、numabstractindexとnumabstractprint。
C言語では、全ての宣言子は正確に１つの型を 持つように宣言しなくてはなりません。 これは、１つより多くの引数の型を操作する関数を書くことが不可能なことを意味します。 –例えば、我々はint（複数）とfloat （複数）に対して 同じ二乗関数を使用することは出来ません。 Splintによって可能となった厳密な型チェックのため、 しばしば1つより多くの可能な型を持つ引数を宣言することが役に立ちます。
Splintは、宣言がいくつかの可能な型のいずれかであることを 示すために代替型を提供します。/*@alt type,+@*/アノテーションは 共用型を作成します。 例えば、int /*@alt char, unsigned char@*/ cはcがint、charまたはunsigned char値を警告なしでそれへ割り当て可能であると宣言します。
替型のいずれかを使用することは、 オペランドの複数の型の上で動作するマクロの型を指定することです（Section 11.2.1参照）。 代替型は無視されても問題ない戻り値を持つ関数の宣言に対して便利です（Section 8.4.2参照）。 関数は型t /*@alt void@*/を戻すことを宣言するかもしれませんが、値が無視される場合は、警告は出さないべきでしょう。
このドキュメントはSplint(英)のサイトを元に作成しました
[PageInfo]
LastUpdate: 2014-02-11 15:05:10, ModifiedBy: daruma_kyo
[License]
Creative Commons 2.1 Attribution-ShareAlike
[Permissions]
view:all, edit:login users, delete/config:members
edit