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

End Notes(文末脚注)

1

 LintはC言語のプログラムの異常を検知するための一般的なプログラミングツールです。S. C. Johnsonは1970年代後半に元のlintを開発しました。 主な理由はC言語の初期のバージョンでは、関数のプロトタイプをサポートしていなかったためです。 Splintは元々、LCLintと名づけられました。理由はLCLの使用とCの実装の間の矛盾をチェックするために 意図されていたためです。 LCLからの相違とセキュリティ上の脆弱性を検知することで増加した焦点を反映するため、 名前が"Specification Lint" と "Secure Programming Lint"の略としてSplintに変更されました。

2

 メタ表記「item,+」はカンマ区切りのリストアイテムを表記するのに使用されます。例えば、
/*@access mstring, intSet@*/
は、mstringintSetの両方の実表現へのアクセスを許可します。

3

 このsectionは主に[Evans96]に基づいています。 メモリ管理のチェックを説明するために必要な用語の一部を半正式に定義します。 もし、これらの用語の直感的な理解が十分であれば、このsectionは飛ばしてかまいません。

4

 そのオブジェクトが型定義されている(typed)ことを除き、LISP記憶領域モデルと同じです。

5

 sizeof演算子を除き、引数を必要としません。

6

 記憶領域が参照へ割り当てられていない場合、内部参照が記憶領域を追跡するために生成されます。

7

 freeの宣言は、引数がNULLでも良いことを示すために引数にnullアノテーションが付きます。 [ISO, 7.20.3.2]によると、NULLは何の動作なしにfreeへ渡されてもかまいません。 一部のUNIXプラットフォームでは、NULLが渡されることにより、プログラムのクラッシュを引き起こします。 そのため、標準ライブラリのUNIX版は引数にnullアノテーションなしでfreeを指定しています。 割り当てられたオブジェクトが完全に破棄される(例えば、構造体内部の共有されていない 全てのオブジェクトが構造体が開放される前に解放される)ことをチェックするために、Splintは out only void *として渡されるどんな引数も、生きていて、共有されていないオブジェクトへの参照が含まれていない ことをチェックします。 これは、理にかなっています。なぜなら、このような引数は記憶領域を破棄する以外のどのような方法によっても 理にかなった方法で使用することが出来ないためです。

8

 3.0以前のSplintのバージョンでは、noreturnアノテーションは、exitsと名付けられていました。 noreturnアノテーションは同じ事を意味していますが、 より適切な名前です。 昔のコードのため、Splintはまだ、exits アノテーションをサポートしています。 同様に、maynotreturnアノテーションは mayexitから取って代えられ、 noreturnwhentrueアノテーションはtruexitから取って代えられ、そして、 noreturnwhenfalseアノテーションはfalseexitから取って代えられます。

9

 sefアノテーションは 副作用が無い引数を示します(Section 11.2.1参照)。 我々は、引数が真偽値でも数値でも良いことを示すために それの型としてbool /*@alt int@*/を使用します。

10

 Peter van der Lindenはデフォルトのフォールスルーは97%の頻度で間違った動作であると推定している。 [vdL95, p. 37]

11

 “Software Glitch Cripples AT&T Network”,Telephony, 1990年1月22日。
訳注:1990年1月15日に起きた、米AT&T社のネットワーク停止のことを言っています。原因はbreak文の漏れです。

12

 チェックの内部側面の情報については[Larochelle01]を参照してください。

13

 このsectionは主に[Evans02]に基づいています。

14

 C. Cowan氏ら, FormatGuard: Automatic Protection from printf Format String Vulnerabilities(書式防御:printfの書式文字列脆弱性からの自動保護) 10th Usenix Security Symposium, 2001.

15

 完全に正しいことは、全てのマクロ引数は、マクロが何からの副作用を持つ前に評価されるべきです。Splintはこのチェックは行いません。

16

 同じ引数で呼び出されるたびに同じ結果を生じない関数は、internalStateを変更することを宣言すべきです。なぜなら、それらがsef引数として渡された場合、エラーの原因になるためです。

17

 最も有名なC言語の命名規則は、チャールズ・シモニー(Charles Simonyi) [Simonyi, Charles, and Martin Heller. “The Hungarian Revolution.” BYTE, August 1991, p. 131-38]によって導入されたハンガリアン命名規則です。 Splintの命名規則の名前は、命名規則に対するニーモニック(記憶術)として、 使用している中央ヨーロッパの国民の習慣に従います。 Splintの規則は、戻り値の宣言の型の代わりに、アクセス可能な抽象型 の名前を符号化することを除き、名前の中の型情報を符号化する点では ハンガリアン命名規則と同じです。 ハンガリアン命名規則で使用されているプレフィックス(接頭辞)は、 Splintではサポートされていません。

18

 もちろん、名前空間のプレフィックス(接頭辞)は、実際には 正規表現によって宣言されるべきです。 もし、十分な関心がある場合(つまり、それをプログラムするための ボランティアがいる場合)、Splintの将来のバージョンにて 正規表現がサポートされるでしょう。

19

 POSIXライブラリはJens Schweikhardt氏によって寄贈されました。

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