Splintユーザーズマニュアル
Version 3.1.1
2003年4月27日
Splint*1はセキュリティの脆弱さとプログラミングのミスを修正するためにC言語のプログラムを 静的にチェックするためのツールです。 Splintは未使用の宣言、型の不整合、定義する前での使用、到達不能コード、 戻り値の無視、リターンが無い実行パス、無限ループの可能性、そして、 フォールスルー(fall through)caseを含む多くの従来のlintチェックを行います。 より強力なチェックがソースコードのアノテーションで指定された追加情報により 可能になっています。 アノテーションは定型化されたコメントで、 関数、変数、引数や型についての仮定を文書化します。 特に、アノテーションによって有効になるチェックに加えて、 多くの従来のlintチェックがこの追加情報を利用することにより改善されています。
より多くの労力をプログラムにアノテーションを付ける事により、 チェックはより良くなります。Splintを使用する際の作業量と効果のイメージ曲線は 図1のようになります。 Splintは柔軟に設計され、プログラマが特定のプロジェクトに対する作業量と効果の曲線上で適切な点を選択 できるようにしています。 異なるチェックが有効にされると、より多くの情報がコードアノテーションにて与えられ、 発見されるバグの数は劇的に増えます。
Splintによって発見できる問題は以下です。
Splintのチェックは、 何のエラーの種類がコマンドラインのフラグとコード上の定型化されたコメントを 使用して報告されるかを選択するためにカスタマイズすることが可能です。 さらに、ユーザは、Splintのチェックを拡張したり、アプリケーション固有のプロパティ(Section 10)を強制したりするために、新しいアノテーションと関連するチェックを を定義することが出来ます。
About This Document（このドキュメントについて）
このドキュメントはSplintを使用するためのガイドです。
Section 1ではSplintを実行する方法を説明し、
メッセージとチェックの制御を説明しています。
Sections 2–13では、Splintによって行われる個々のチェックについて説明しています。
section間には少しだけ依存関係がありますが、一般的にどのような順序でも読むことが出来ます。
Section 14は大きなシステム上でSplintを実行するために重要なヘッダファイルのインクルードとライブラリに関係する問題をカバーしています。
このドキュメントではチェックの技術的な詳細は説明していません。
技術的なバックグラウンドと実例によるSplintの有効性の分析については、
http://www.splint.org/から利用可能な論文を参照してください。
人自体がまだ完全にデバッグされていないため、何をするかに関係なく、そのコードにはバグが存在するでしょう。
Chris Mason,Zero-defects memo (quoted in Microsoft Secrets, Cusumano and Selby)
Splintはチェック対象のファイルのリストに対して呼び出されます。 初期化フラグ、コマンドラインフラグ、及び、定型化されたコメントは 全体的に、かつ、局所的にチェックをカスタマイズするために使用されます。
Splintを使用することを学ぶための最も良い方法は、もちろん、 実際に使うことです（もし、システム上にインストールされたSplintをまだ持っていないなら、 Appendix Aを参照してください）。 このドキュメントを読む進める前に、小さなCプログラムを見つけることをお勧めします。 そして、実行してみてください。
ほとんどのCプログラムに対して、これはたくさんの警告を生じさせます。 いくつかの警告に対する報告をオフにするために、以下を試してください。
-weakフラグは デフォルトモードで行われるよりも弱いチェックを選択するために 多くのチェックパラメータを設定するモードフラグです。 他のSplintのフラグは次のsectionで紹介されます。 完全なリストはAppendix Bに記載されています。
典型的な警告メッセージは以下です。
sample.c: (in function faucet) sample.c:11:12 : Fresh storage x not released before return A memory leak has been detected. Storage allocated locally is not released before the last reference to it is lost. (Use -mustfreefresh to inhibit warning) sample.c:5:47: Fresh storage x allocated
最初の行はエラーが発見された関数の名前を提供します。 これは関数に対して報告された最初のメッセージの前に出力されます。 2行目はメッセージのテキストです。 このメッセージはメモリリークを報告しています （関数内で割り当てた記憶領域が関数が戻る前に解放されていない）。 エラーがあるファイル名、行数、列数がテキストの前に出力されます。
次の行では、 警告メッセージを抑制することが出来る方法についての情報を含む、エラーが疑われる箇所、 についてのさらなる情報を与えるヒントとなります。このメッセージは -mustfreefreshフラグを使用すると 報告されてからこの警告が出力されないようにするでしょう。 このフラグはコマンドラインにより設定、あるいは、アノテーション（Section 1.3.2参照） の使用により問題のコード位置の周りにちょうど正確に設定されます。
メッセージの最後の行は追加の場所の情報を提供します。 このメッセージは、リークしている記憶領域が割り当てられた場所を伝えています。
一般的なメッセージの書式は以下の通りです （角括弧で囲まれた部分は省略可能です）。
edit [<file>:<line> (in <context>)]
<file>:<line>[,<column>]: message
[hint]
<file>:<line>,<column>: extra location information, if appropriate
ユーザはSplintから出力されるメッセージの形式と内容を カスタマイズすることが出来ます。-showfuncフラグが使用されている場合、 関数の内容は出力されません。-showcolフラグ が使用されている場合、列数は出力されません。+parenfileformatフラグは Microsoft Visual Studioが認識できる形式でファイルの場所を生成するために使用可能です。 +parenfileformatフラグが設定された場合、 行番号はカッコ内にファイル名に続けられます（例えば、sample.c(11)）。 メッセージは-linelenフラグを使用されて設定された値未満の長さの行に 分割されます。 デフォルトの行の長さは80文字です。Splintは可能な限り、長さの制限に近くなるよう かなりの場所で行を分割しようとします。
-hintsフラグは出力されてからの全ての ヒントを抑制します。通常、ヒントは初めてエラーの種類が報告されたときのみ提供されます。 Splintに、とにかく全てのメッセージに対するヒントを出力させるためには、+forcehintsフラグを使用してください。
多くのプログラミングスタイルをサポートするために、 Splintはチェックとメッセージの報告を制御するために数百のフラグを提供しています。 フラグのいくつかは、このドキュメントの本文で紹介しています。 Appendix Bでは全てのフラグを説明しています。 モードとショートカットのフラグは一度に多くのフラグを設定するために提供されています。 個々のフラグはモードの設定を上書きすることが出来ます。
フラグには+あるいは-が先に付きます。 +が付いた場合はオンと呼び、-が付いた場合はオフと呼びます。 オンとオフの正確な意味はフラグの種類に依存します。
-フラグの設定は一貫性と明確さのために使用されますが、しかし、 標準UNIXの使用と矛盾します。そして、偶然に間違って使用することは容易にあります。 間違ったフラグの使用の可能性を減らすために、Splintは普通ではない方法でフラグが設定された場合に 警告を出します。 フラグが重複し、既にある値に設定されていた場合（フラグが定型化されたコメントを使用して設定されたとき、 エラーが報告されます）、モードフラグや特殊なフラグが一般的なフラグにより設定されるであろうより具体的なフラグ が既に設定された後に設定されている場合、 値フラグに不当な値が与えられた場合、もしくは、フラグが矛盾する方法で設定されていた場合、 警告が出されます。 -warnflagsフラグは これらの警告を抑制します。
デフォルトのフラグは、読むことが出来れば、~/.splintrcから読み込まれます。 作業ディレクトリ内に.splintrcが存在する場合は、 このファイルの設定は次に読み込まれ、~/.splintrc 内の値を上書きします。 コマンドラインでのフラグはファイルの設定を上書きします。 .splintrcファイルの 構文は、フラグを別の行にすることが出来ること、#文字で行の残りの部分がコメントであることを示すことを除き、 コマンドラインでのフラグのそれと同じです。 -nofフラグは~/.splintrcファイルが ロードされないようにします。 -f <filename>フラグはfilenameから任意にロードします。
フラグの名前を読みやすくするために、コマンドラインのフラグの中にある ハイフン（-）、アンダースコア（_）、スペースは無視されます。 従って、warnflags、warn-flagsとwarn_flagsは全て、warnflagsオプションを選択します。
定型化されたコメントは チェックを良くするため、又は、局所的にフラグの設定を制御するために、 型、変数あるいは関数のインタフェースについての追加情報を提供するために使用されます。
全ての定型化されたコメントは/*@で始まり、コメントの終わりによって閉じられます。@の役割は どんな出力可能文字によって行われてもかまいません。 異なる定型化されたコメントマーカーを選択するには、 -commentchar <char>を使用してください。
アノテーションは明確な構文に従う定型化されたコメントです。 それらはコメントですが、固定的な文法上のコンテキスト上でのみ使用されます （例えば、型の修飾子の様な）。
Sections 2–6 では、変数、引数、戻り値、構造体のフィールドと、 型の定義についての仮定を表現するためのアノテーションについて説明しています。 例えば、/*@null@*/は 引数がNULLである可能性があるという仮定を表現するために使用されます。 Section 7では関数のインタフェースを記述するためのアノテーションを説明します。 他のアノテーションは後のsectionで説明し、 Section 10ではユーザが新しいアノテーションを定義するために使用することが出来る メカニズムについて説明します。 アノテーションの概要は Appendix Cに記載されています。
制御コメントとして知られているいくつかのアノテーションは、 C言語のプログラムの中に2つの任意のトークンの間に現れる場合があります （通常のC言語のコメントとは異なり、制御コメントがコード内に新しい区切り文字を導入するように 単一のトークンの中で使用されるべきではありません。） 文法的に、それらは、標準コメントとは異なっていません。 制御コメントはSplintのチェックのソースレベルの制御を提供するために使用されます。 それらは、偽のメッセージの抑制するため、フラグを設定するため、そして、他の方法での局所的なチェックの制御をするために 使用される場合があります。
ほとんどのフラグ（Appendix Bの中で“global”として
特徴付けられているフラグを除く全て）は、制御コメントを使用して局所的に設定される場合があります。
制御コメントはコマンドラインの設定を上書きするために、局所的にフラグを設定できます。
元のフラグの設定は次のファイルを処理する前に復元されます。
制御コメント内でフラグを設定するための構文はコマンドラインのそれと同じです。
ただし、そのフラグもまた、元のコマンドラインの値にそれらの設定を復元ために、
=によって選考されている場合を除きます。
例えば、
は、charintフラグをオン （これはcharとintを区別しない型とする） に設定し、modifiesフラグ をオフ（これは変更エラーの報告を抑制する）に設定し、そして、showfuncフラグを 元の値（これは関数の名前がメッセージの前に表示されるかどうかを制御する）に設定します。
このドキュメントはSplint(英)のサイトを元に作成しました
[PageInfo]
LastUpdate: 2014-02-11 15:04:43, ModifiedBy: daruma_kyo
[License]
Creative Commons 2.1 Attribution-ShareAlike
[Permissions]
view:all, edit:login users, delete/config:members