appC - Splint翻訳 Wiki - Splint翻訳

Up: マニュアル

Prev: Appendix B Flags（フラグ）

Next: Appendix D Specifications（仕様）

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

Appendix C Annotations（アノテーション）

Suppressing Warnings（警告の抑制）

いくつかのアノテーションがメッセージの抑制のために用意されています。 一般的には、永久に特定のエラーを抑制するために特定のフラグを使用することは通常、良いですが、 しかし、一般的なエラー抑制フラグは、後で修正されるか、あるいは、ドキュメント化されるであろう コードに対するメッセージを直に抑制するのに便利です。

ignore
end

/*@ignore@*/と/*@end@*/で囲まれた 範囲のコードではエラーは報告されません。 これらのコメントは制限が無いメッセージの数を簡単に抑制するために 使用されますが、しかし、エラーが報告されない範囲であるignore…end の領域に本当のエラーがあった場合、危険です。 ignoreと endのコメントは一致している必要があります。 — ファイルが無視する領域で終わっている場合、あるいは、 無視する領域内でignoreが使用された場合、 警告が出力されます。

i

/*@i@*/コメントから行の終わりまで エラーは報告されません。

i<n>

'/*@i<n>@*/'コメント（例えば、 /*@i3@*/） から行の終わりまで、エラーは報告されません。 コメントの場所から行の終わりまで、正確にn個の抑制されるエラーが なかった場合、Splintはエラーを報告します。 これは、予想するエラーの数が存在しない場合、メッセージを生成するため、 iあるいは ignoreより堅牢です。 エラーは、このファイルが処理されるまで必ずしも検知されるとは限らない （例えば、未使用の変数のエラー）ため、 全てのファイルが処理し終わった後で抑制されたエラーの数が報告されます。 ‑supcountsフラグは これらのエラーを抑制するために使用できます。 これは、システム条件が別のフラグの設定で再チェック された場合に役立ちます。

t
t<n>

iと i<n>と同様に、 +tmpcommentsフラグによる 制御を除きます。 これらは、一時的に特定のエラーを抑制するために使用できます。 その後、-tmpcommentsは再度それらを 発見するために設定することが可能です。

Syntactic Annotations（構文アノテーション）

下記の文法は、 構文コメントの文法を示すために、変更された[K&R,A13]からの C構文です。 Splintのアノテーションによってのみ効果が出ることを示します。 アノテーションでは、@ はコメントのマーカ文字を意味します。これは -commentchar によって設定されます（デフォルトは@です）。

Functions（関数）

direct-declarator ⇒

direct-declarator (parameter-type-list_opt) stateClause*_opt globals_opt modifies_opt
| direct-declarator (identifier-list_opt)stateClause*_opt globals_opt modifies_opt

stateClause ⇒ /*@ ( uses | sets | defines | allocates | releases) reference,+ ;_opt @*/

| /*@ ( ensures | requires ) stateTag reference,+ ;_opt @*/ (Section 7.4)

stateTag ⇒ only | shared | owned | dependent | observer | exposed | isnull | notnull

| identifier (メタ状態定義によって定義されたアノテーション, Section 10)

globals ⇒ /*@globals globitem,+ ;_opt @*/ | /*@globalsdeclaration-list_opt ;_opt @*/
globitem ⇒ [ ( undef | killed )* ] identifier | internalState| fileSystem

modifies ⇒ /*@modifies (nothing | (expression | internalState | fileSystem)+ ;_opt) @*/

| /*@*/ (globals と modifies が無いときの省略形。)

Iterators (Section 11.4)（イテレータ）

イテレータは既にコメントであるため、 コメントによって囲まれない点を除き、 イテレータに対するグローバル句と修正句は関数に対するそれらと同様です。

direct-declarator

⇒ /*@iter identifier (parameter-type-list_opt ) iterGlobals_opt iterModifies_opt @*/

iter-globals ⇒ globals declaration-list_opt ;_opt
iter-modifies ⇒ modifies moditem,+;_opt| modifies nothing;_opt

Constants (Section 11.1)（定数）

external-declaration ⇒ /*@constant declaration ;_opt @*/

Alternate Types (Section 4.4)（代替型）

代替型は引数と戻り値の型指定で使用することができます。

extended-type ⇒ type-specifier alt-type _opt
alt-type ⇒ /*@alt basic-type,+ @*/

Declarator Annotations（宣言子アノテーション）

一般的なアノテーションは複数のstorage-class-specifierの後、かつ、 複数のtype-specifierの前に現れます。 複数のアノテーションは任意の順番で使用することが出来ます。 ここでは、アノテーションは周りのコメント無しです。 宣言内で、アノテーションは/*@と@*/によって 囲まれます。グローバルあるいは変更句あるいは、イテレータあるいは定数宣言内で、 コメント内にあるため、囲まれていないコメントが使用されます。

Type Definitions (Section 4.3)（型定義）

型定義はabstractあるいはconcreteの どちらか、mutableあるいはimmutableの どちらか、それから、refcountedが使用可能です。 structのポインタのみ、 refcountedで宣言することが出来ます。 具象型は実際の型から可変性を継承するため、 可変性アノテーションは具象型では使用できません。

abstract

型は抽象型です。 (表現がクライアントから隠されています。)

concrete

型は具象型です。 (表現がクライアントに表示されています。)

immutable

型のインスタンスは値を変更できません。

mutable

型のインスタンスは値を変更可能です。

refcounted

参照がカウントされます (Section 5.4)。

Type Access（型アクセス）

制御コメントは型のアクセス設定を上書きするために も使用できます。

/*@access <type>,+@*/

以下のコードは<type>の表現へアクセスする ことが許可されます。 型のアクセスは、コメントした時点から、ファイルの終端に達するか、あるいは、 この型に対する次のアクセス制御コメントまで適用されます。

/*@noaccess <type>,+@*/

<type>の表現へのアクセスを 制限します。 noaccessコメントの中にある型は 抽象型として宣言されている必要があります。

Global Variables (Section 7.2 )（グローバル変数）

１つのチェックアノテーションがグローバルあるいはファイル静的変数の宣言上で使用可能です。

unchecked

グローバルの使用に対しての最も弱いチェックです。

checkmod

グローバルを使用しないことによる変更をチェックします。

checked

グローバルの使用と変更をチェックします。

checkedstrict

グローバルリストが無い関数でのグローバルの使用をチェックします。

Memory Management (Section 5 )（メモリ管理）

dependent

外部所有された記憶領域への参照です。 (Section 5.2.2 )

keep

呼び出された関数によって保持された引数です。 呼び出し元は呼び出した後に記憶領域を使用することができますが、しかし、 呼び出された関数は確実にそれが解放されていることを確認する責任があります。 (Section 5.2.4 )

killref

refcounted引数です。 この参照は呼び出しによって終了します。 (Section 5.4)

only

unshared参照です。 参照が失われる前に関連するメモリが解放されなければなりません。 (Section 5.2 )

owned

記憶領域は依存する参照によって共有される可能性がありますが、 この参照が失われる前に関連するメモリが解放されなければなりません。 (Section 5.2.2 )

shared

決して解放されることが無い共有された参照です。 (Section 5.2.5 )

temp

一時的な引数です。解放されない場合、そこに新しい別名が作成されない場合があります。 (Section 5.2.2)

Aliasing (Section 6 )（別名化）

両方の別名化アノテーションは引数の宣言で使用することが可能です。

unique

関数への任意の他の参照変数によっても別名化されない引数です。 (Section 6.1.1 )

returned

戻り値によって別名化される可能性のある引数です。 (Section 6.1.2 )

Exposure (Section 6.2 )（暴露）

observer

変更が不可能な参照です。 (Section 6.2.1 )

exposed

別のオブジェクトの中にある記憶領域への暴露された参照です。 (Section 6.2 )

Definition State (Section 3 )（定義状態）

out

参照から到達可能な記憶領域は、定義する必要はありません。

in

参照から到達可能な全ての記憶領域は定義されていなければなりません。

partial

部分的に定義されています。 構造体は未定義のフィールドを持っている可能性があります。 フィールドが使用されている場合、エラーは報告されません。

reldef

定義チェックを緩和します。参照が定義されていない場合、あるいは それが使用されている場合、エラーは報告されません。

Global State (Section 7.2.2)（グローバル状態）

これらのアノテーションはグローバルリストの中でのみ使用することが出来ます。 両方のアノテーションは、 変数が関数呼び出しの前後で未定義であることを意味するために、 同じ変数に対して使用できます。

undef

変数は関数呼び出しの前では定義されていません。

killed

変数は関数呼び出しの後では定義されていません。

Null State (Section 2 )（Null状態）

null

nullの可能性があるポインタです。

notnull

nullではないポインタです。

relnull

nullのチェックを緩和します。 NULLが割り当てられたとき、 あるいはnullではないポインタとして使用されたときにエラーを報告しません。

Null Predicates (Section 2.1.1 )（Nullの判定）

null predicateアノテーションは、第一引数がnullの可能性のあるポインタであり、 Boolean型（真偽値型）を返す関数の戻り値に使用することが出来ます。

nullwhentrue

結果がtrue（真）の場合、第一引数は NULLです。

falsewhennull

結果が TRUEの場合、 第一引数は NULLではありません。

Execution (Section 8.1 )（実行）

noreturn、maynotreturnと alwaysreturnのアノテーションは どの関数に対しても使用することが出来ます。 noreturnwhentrueと noreturnwhenfalseの のアノテーションは第一引数の型がBoolean型（真偽値型）である関数に対してのみ使用可能です。

noreturn

関数は決して戻ることはありません。

maynotreturn

関数は戻り場合と戻らない場合があります。

noreturnwhentrue

第一引数が TRUEの場合、 関数は戻りません。

noreturnwhenfalse

第一引数が FALSEの場合、 関数は戻りません。

alwaysreturn

関数は常に戻ります。

Side Effects (Section 11.2.1)（副作用）

sef

対応する実引数には副作用はありません。

Declarations（宣言）

これらのアノテーションは未使用あるいは未定義エラーの報告を制御するために 宣言上で使用することが出来ます。

unused

識別子は使用される必要はありません （未使用のエラーは報告されません）。 (Section 13.1 )

external

識別子は外部で定義されています （未定義のエラーは報告されません）。 (Section 13.2 )

Switch Statements（Switch文）

fallthrough

breakが無いcaseです。もし、前のcaseから fallthroughの直後のcaseに 処理が移る場合、エラーは報告されません。

Break and Continue Statements (Section 8.3.3)（break文とcontinue文）

これらのアノテーションは break文あるいは continue文 の前で使用することが出来ます。

innerbreak

breakは内部ループあるいはswitchから抜けます。

loopbreak

breakはループから抜けます。

switchbreak

breakはswitchから抜けます。

innercontinue

continueは内部ループを続けます。

Unreachable Code（到達不能コード）

このアノテーションは到達不能コードのエラーを抑制するために 文の前に使用することが出来ます。

notreached

文は到達不可能である可能性があります。

Format String Arguments（書式文字列引数）

これらのアノテーションは関数宣言の直前で使用されます。

printflike

printf ライブラリ関数のような 可変個の引数をチェックします。

scanflike

scanf ライブラリ関数のような 可変個の引数をチェックします。

Use Warnings（使用への警告）

これらのアノテーションは関数、変数、あるいは型宣言の直前で使用されます。

warn <flag-specifier> <message>

この宣言子が使用されている場所で警告を出します （flag-specifierによって制御されます）。

Macro Expansion（マクロ展開）

/*@notfunction@*/

次のマクロ定義は関数であることを意図されておらず、 マクロ関数定義としてチェックされる代わりに行に展開されるべきです。

Arbitrary Integral Types（任意の整数型）

これらのアノテーションは任意の整数型を表すために使用されます。 文法的には、暗黙のint型で置き換えます。

/*@integraltype@*/

任意の整数型です。実際の型はshort、 int、 long、 unsigned short、 unsigned、あるいは、unsigned longのいすれかです。

/*@unsignedintegraltype@*/

任意の符号なしの（0以上の）整数型です。 実際の型はunsigned short、 unsigned、あるいは、 unsigned longのいずれかです。

/*@signedintegraltype@*/

任意の符号ありの整数型です。 実際の型はshort、 int、あるいは、 longのいずれかです。

Traditional Lint Comments（伝統的なlintコメント）

多くの標準UNIX lintによってサポートされている制御コメントの一部は、 レガシーシステムをより簡単にチェック可能とするため、Splintでサポート されています。 これらのコメントはSplintコメントと語彙的に矛盾なく、そして、 それらの意味はあまり正確ではなく（そして、異なるlintプログラム間で変化するかもしれない） 、そのため、我々は、Splintコメントが 標準lintコメントを既に含んでいるレガシーシステムのチェックを除いて、代わりに 使用されることをお勧めします。

これらの標準lintコメントはSplintによってサポートされています:

/*FALLTHROUGH*/ (別のつづり違いに、 /*FALLTHRU*/)

breakが無いcaseに対してのエラーを抑制します。 /*@fallthrough@*/と同じ意味です。

/*NOTREACHED*/

（関数の終わりまで）到達しないコードに関するエラーを抑制します。 /*@notreached@*/と同じ意味です。

/*PRINTFLIKE*/

printfライブラリ関数と同様の 引数です（厳密にこれが何の意味なのかについて、標準lintの中での大した一致は あるように思えません）。Splintは以下をサポートしています：

/*@printflike@*/

関数は任意の型の0個以上の引数、変更されることのないchar *書式文字列引数、そして、 書式文字列によって指示された0個以上の型と数値引数を持ちます。 書式コードはprintf 標準ライブラリ関数と同様に解釈されます。 任意の型の結果を返す可能性があります。 （Splintは/*PRINTFLIKE*/を/*@printflike@*/として解釈します。）

/*@scanflike@*/

書式コードが scanfライブラリ関数 のように解釈されることを除き、printflikeと同様です。

/*ARGSUSED*/

この関数に対する未使用引数のメッセージをオフにします。 制御コメント/*@‑paramuse @*/が 同様の効果のために使用でき、あるいは、/*@unused@*/が 個々の引数宣言で使用可能です。

Splintは-lint-commentsが使用されている場合、 標準lintコメントを無視します。 +warn-lint-commentsが使用されている場合、 Splintは標準lintコメントに対しメッセージを生成し、代わりを提案します。

Metastate Definitions（メタ状態定義）

.mtsファイルの文法を以下に示します。

metastate ⇒ [ global ] attribute identifier clause* end
clause ⇒ contextClause | valuesClause | defaultClause | defaultsClause

| annotationsClause | mergeClause | transfersClause | loserefClause
| preconditionsClause | postconditionsClause

contextClause⇒ context contextSelector
contextSelector ⇒ ( parameter | reference | result | clause | literal | null ) [ type ]
valuesClause⇒ oneof valueChoice,*

defaultClause ⇒ default valueChoide
defaultsClause⇒ defaults ( contextSelector ==> valueChoice )*

annotationsClause⇒ annotations ( identifier [ contextSelector ] ==> valueChoice )*

mergeClause⇒ merge ( mergeItem + mergeItem ==> transferAction )*
mergeItem⇒ valueChoice | *

transfersClause⇒ transfers ( valueChoice as valueChoice==> transferAction )*
loserefClause⇒ losereference ( valueChoice ==> errorAction )*

transferAction⇒ valueChoice | errorAction
errorAction⇒ error [ stringLiteral ]

valueChoice⇒ identifier

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

Up: マニュアル

Prev: Appendix B Flags（フラグ）

Next: Appendix D Specifications（仕様）