sec8 - Splint翻訳 Wiki - Splint翻訳

Up: マニュアル

Prev: 7 Function Interfaces（関数インタフェース）

Next: 9 Buffer Sizes（バッファーサイズ）

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

8 Control Flow（制御フロー）

このsectionでは処理フローを制御するのに関係する Splintにより行われるチェックについて述べます。 これらのチェックの多くは、アノテーションが与えられている場合には プログラムについて既知である追加の情報のために著しく品質が良くなります。

8.1 Execution（実行）

確かなエラーを検出し、偽のエラーを回避するために、 呼び出された関数の制御フローの動作について、いくらか知っておくことが重要です。 追加の情報がない場合、Splintは全ての関数は最終的に戻り、実行が呼び出し側では 正常に継続するものとして想定します。

noreturnアノテーションは 決して戻ることがない関数を示すために使用されます^*8。例えば、

extern /*@noreturn@*/ void fatalerror (/*@observer@*/ char *s);

は、fatalerror が決して戻らないことを宣言しています。 これは、Splintが以下のようなコードを正しく分析することを可能にします。

if (x == NULL) fatalerror ("Yikes!");
*x = 3;

他の関数は戻るが、時々（あるいは通常） 正常に戻る場合もありえます。maynotreturn アノテーションは関数が戻ったり・戻らなかったりする場合があることを示します。 これはドキュメントの役に立つかもしれませんが、コードチェック時にSplintは maynotreturnで宣言された関数が 正常に戻ると想定しなければならなくなるため、あまりチェックの助けにはなりません。 alwaysreturnsアノテーションは 関数が常に戻ることを示します（しかしSplintはこれを検証するためのチェックはしません）。

戻らない関数をより正確に記述するために、 noreturnwhentrueと noreturnwhenfalse アノテーションが使用可能です。 nullwhentrueと falsewhennullアノテーション （Section 2.1.1参照）と同様に、 noreturnwhentrueと noreturnwhenfalseは 第一引数の値が真（noreturnwhentrue）あるいは 偽（noreturnwhenfalse）の場合に 関数が戻ることが無いことを意味します。 それらは、第一引数が真偽値である関数でのみ使用されます。

従って、 noreturnwhenwfalseで宣言された関数は その引数の値が偽の場合は決して戻ってはなりません。例えば、 標準ライブラリは以下のようにassertを宣言します^*9。

/*@noreturnwhenfalse@*/ void
assert (/*@sef@*/ bool /*@alt int@*/ pred);

これの使い方は、次のようなコードです。

assert (x != NULL);
*x = 3;

assertに付いているnoreturnwhenwfalseアノテーションが x != NULLが偽である場合、 xの参照先が到達できないことを意味するため、 上記は、偽の場合の警告を出さずにチェックされます。

8.2 Undefined Behavior（未定義の動作）

Cプログラムの中で副作用が起こる順番は コードでは完全に定義されていません。 特定の実行ポイントはsequence points（シーケンス・ポイント） として知られています。
※シーケンス・ポイント：関数呼び出し（引数が評価された後）、 完全な式の最後（初期化子、式文、if、 switch、whileあるいは doの制御式、forのそれぞれの式、 そして、return文の中の式）、と、第一オペランドあるいは &&、||、 ?あるいは,オペランドの後。

シーケンス・ポイントの前の全ての副作用は シーケンス・ポイントの前に完了していなければならず、また、 シーケンス・ポイントの後に評価が行われることはありません。 シーケンス・ポイント間で、副作用と評価はどのような順番で行われてもかまいません。 従って、指揮や引数が評価される順番は指定されていません。 コンパイラは自由に任意の順番で関数の引数と式（シーケンスポイントを含まない）の一部 を評価することが出来ます。 他が使用する前あるいは後で評価する必要のない別の式によって変更された値を使っている場合、 コードの動作は定義されていません。

Splintは定義されていない評価順で定義されていない動作が 生ずる場所を検出します。 もし、変更句とグローバルリストが使用されている場合、 チェックは関数呼び出しを含む式で有効になっています。 評価順序のチェックはeval-orderフラグで制御されます。

order.c

Running Splint

extern int glob;   extern int mystery (void);   extern int modglob (void)    /*@globals glob@*/    /*@modifies glob@*/;   int f (int x, int y[]) { 11 int i = x++ * x;   13 y[i] = i++; 14 i += modglob() * glob; 15 i += mystery() * glob; 16 return i; }

> splint order.c +evalorderuncon order.c:11: Expression has undefined behavior (value of     right operand modified by left operand): x++ * x order.c:13: Expression has undefined behavior (left operand     uses i, modified by right operand): y[i] = i++ order.c:14: Expression has undefined behavior (value of     right operand modified by left operand):     modglob() * glob order.c:15: Expression has undefined behavior     (unconstrained function mystery used in left operand     may set global variable glob used in right operand):     mystery() * glob   modglob の句の変更は globを変更する可能性があることを 示しているので、14行目で警告が報告されています。 変更前、後あるいは中に glob が 評価された場合、我々は知らないため、動作は未定義です。 15行目の警告は +evalorderuncon フラグがない場合は報告されないでしょう。

図 16.  評価順序

変更句とグローバルの情報（Section 7参照）がない場合の システムをチェックする際、評価順序のチェックは 制約が無い関数が関数の引数で呼ばれた場合、エラーを報告する場合があります。 Splintはこれらの関数が変更する可能性があるものを強制するためのアノテーションは 持っていたいため、別の引数が制約の無い関数を呼び出すか、制約の無い関数へ引数から到達できるグローバル変数あるいは 記憶領域を使用する場合、評価順序が定義されることは保障できません。 未定義の動作の可能性を取り除く方法で未定義の関数を強制するために 変更句と修正句を追加することは最も良いことです。 大きい昔のシステムの場合、これは多くの労力が必要となる可能性があります。 代わりに、-eval-order-unconフラグ は制約の無い関数の評価順序のために未定義の動作の報告を抑制するために使用できます。 図16は未定義の動作の検出を示しています。

loop.c

Running Splint

extern int glob1, glob2; extern int f (void)   /*@globals glob1@*/   /*@modifies nothing@*/; extern void g (void)   /*@modifies glob2@*/ ; extern void h (void) ;   void upto (int x) { 14  while (x > f ()) g(); 15  while (f () < 3) h(); }

> splint loop.c +infloopsuncon loop.c:14: Suspected infinite loop.  No value used in     loop test (x, glob1) is modified by test or loop     body. loop.c:15: Suspected infinite loop.  No condition     values modified.  Modification possible through     unconstrained calls: h An error is reported for line 14 since the only value modified by the loop test or body if glob2 and the value of the loop test does not depend on glob2 （訳注：訳せませんでした。とにかく、14行目は、 ループの本体で、ループの制御文で使われる値が更新されないため、 無限ループとなり、エラーが報告されます。）.  15行目のエラーは +infloopsuncon が無い場合は報告されません。

図 17.  無限ループ

8.3 Problematic Control Structures（問題のある制御構造）

いくつかの文法的に正しい制御構造がプログラム内のバグ の可能性を示すことがあります。 Splintは、無限ループの可能性（Section 8.3.1）、 switch文でのフォールスルーとcase文の不足（Section 8.3.2）、 深くネスとされたループやswitch文でのbreak文(Section 8.3.3)、 本体が空あるいは、本体がブロック化されていない単一文になっている if、whileあるいは for文の句(Section 8.3.4) そして、不完全なif-else論理(Section 8.3.5)に伴うエラーを検知することができます。 正しいプログラムにてこれらのどれもが現れる可能性がありますが、 それらが使用されるプログラミングスタイルに依存することは、 検知され、除去されるべき不具合あるいはスタイル違反の可能性を示すかもしれません。

8.3.1 Likely Infinite Loops（無限ループの可能性）

Splintは無限に続くように見えるループを検知した場合、 エラーを報告します。 エラーはループの本体側の条件の中で、あるいはそれ自身の条件確認の中で 使用されているどんな値も変更されないループに対して報告されます。 このチェックは変更句とグローバルリスト（Section 7参照）により質が高まります。 なぜなら、それらは、グローバル変数が条件確認の中で使用される可能性のあることと、 値がループ本体の中での関数呼び出しによって変更される可能性のあることについての より詳しい情報を提供するためです。

図17はSplintによって検出された無限ループの例を 示しています。 エラーは、14行目のループに対して報告されています。 なぜなら、ループの条件（直接的に、xとf関数を通してのglob1） 内で使用されている値のどちらも、ループの本体で変更されていないためです。 g関数の 宣言が変更句にてglob1を含むよう変更された場合は、 エラーは報告されません。 （この例では、我々はアノテーションが正しいと仮定している場合、 プログラムは、恐らく、 ループ本体で間違った関数を呼び出しています。 これは関数名と変数名の酷い選択を考えると、驚くことではありません！）

制約の無い関数がループの本体で呼び出された場合、 Splintはinfloopsunconフラグがオンでなければ、 条件確認にて使用されている値が変更されとして想定し、 無限ループを報告しません。 infloopsunconフラグがオンの場合、 Splintは条件確認で使用されている値の明確な変更がないが、しかし、 制約の無い関数への呼び出しを通して検出できない変更ある可能性のある（例えば図17の12行目（訳注：15行目では？）） ループに対して無限ループのエラーを報告します。

8.3.2 Switches（Switch文）

C言語のswitch文の自動のフォールスルー（通り抜け）は ほとんど意図した動作ではありません。^*10 Splintは次のcaseにフォールスルー する可能性のあるコードを持つcase文を検出します。 casebreakフラグは フォールスルーcaseの報告を制御します。 １つのフォールスルーcaseは、 処理がこのcaseへフォールスルーすることを明確に示すために /*@fallthrough@*/が付いている caseキーワード が前に付くことによってマークされます。

enum型 のswitchに対しては、 switchの本体の中のcaseとして列挙メンバが現れなかった場合（かつ、default caseがなかった場合） に、Splintはエラーを報告します。 （misscaseフラグにより制御されます。）

switch.c	Running Splint
typedef enum {   YES, NO, DEFINITELY,   PROBABLY, MAYBE } ynm; void decide (ynm y) {   switch (y)     {     case PROBABLY:     case NO: printf ("No!"); 10   case MAYBE: printf ("Maybe");          /*@fallthrough@*/     case YES: printf ("Yes!"); 13   } }	> splint switch.c switch.c:10: Fall through case (no preceding break) switch.c:13: Missing case in switch: DEFINITELY   NO caseに対してはフォールスルーエラーは報告されません。 なぜなら、前のcaseに関連付いた文が無いためです。 /*@fallthrough@*/ コメントは、 YES caseへ 処理が生ずることによるメッセージを抑制します。

図 18.  Switch Case

8.3.3 Deep Breaks（深いbreak）

ネストされたループからの脱出に対して、 （goto以外で）C言語では 提供されている構文はありません。 全てのbreakとcontinue 文は最も内側のループあるいはswitch上のみ行います。 プログラマがそうではなくて、外側のループあるいはswitchを 脱出するつもりである場合、これは重大な問題^*11 に繋がりかねません。 Splintは必要に応じてネストされた状況下でのbreak文と continue文に対して 警告を報告します。

4種類のbreakの警告が報告されます：

• ループ（while や for）の中のループの中のbreak。looploopbreakフラグにより制御されます。breakが内側のループの中にあることを示すために、/*@innerbreak@*/をbreakの前に置いてください。
• switch文の中のループの中のbreak。switchloopbreakフラグにより制御されます。ループの脱出としてbreakをマークするために、/*@loopbreak@*/をbreakの前に置いてください。
• ループの中にあるswitchの中のbreak。loopswitchbreakフラグにより制御されます。switchの脱出としてbreakをマークするために、/*@switchbreak@*/をbreakの前に置いてください。
• 別のswitchの中にあるswitchの中のbreak。switchswitchbreakフラグにより制御されます。内側のswitchに対するbreakであることを示すために、/*@innerbreak@*/を使用してください。

continueは、 ループ内でのみ使用可能であるため、警告（looploopcontinueで制御される）は ネストされたループ内のcontinue文に対してのみ 報告されます。 局所的にエラーメッセージを抑制するために、 間違いの無い内側のcontinueの前に /*@innercontinue@*/ が置かれてもかまいません。 deepbreakフラグは 全てのネストされたbreakとcontinueのチェックフラグを設定します。

breakの前に置かれたマーカーが その配置に矛盾している場合、Splintは警告を発します。 innerbreakが 内側のループの脱出ではないbreakの前に置かれている場合、 switchbreakがswitchを脱出しない breakの前に置かれている場合、 あるいは、 loopbreakがループを脱出しない breakの前に置かれている場合、 警告が発せられます。

8.3.4 Loop and If Bodies（ループとifの本体）

if、while、 または、for の後の空文は潜在的なバグがあることを示します。 if、while、 または、forの後の１つの文（すなわち、中括弧（{}）でブロック化されていない） はバグを示しそうではありません。しかし、コードを読んだり、編集したりすることを難しくします。 Splintは空の本体、あるいはブロック化されていない本体があるifやループ文に対して エラーを報告することが出来ます。 異なるフラグがif、while、 または、forに続く文に対するチェックを制御します：

• [if,while,for]empty - 本体が空の場合にエラーを報告します。 (例えば、 if (x > 3); )
• [if,while,for]block - 本体がブロック化されていない場合にエラーを報告します。 (例えば、 if (x > 3)x++;)

if文のチェックは、 elseの本体についても適用されます。 習慣的に良く使われるelse if連鎖を許すため、 elseの本体がif文の場合は ifblock警告は報告されません。

8.3.5 Complete Logic（ロジックを完全にする）

多くの状況下では完全に合理的ではあるかもしれませんが、 最後にelseが付いていない if-elseの連鎖は ロジックが欠落しているか、 エラーの場合をチェックすることを忘れていることを示す場合があります。 elseif-completeフラグがオンの場合 elseの本体 にあるif文が 対応するelseを持たない場合、 Splintは警告を発します。 例えば、コード、

if (x == 0) { return "nil"; }
else if (x == 1) { return "many"; }

は、2つ目のifは対応するelseを持っていないため、 結果的に警告が発せられます。

8.4 Suspicious Statements（怪しい文）

Splintは明らかに効果の無い文（Section 8.4.1）と 呼び出された関数の戻り値を無視している文（Section 8.4.2）を含むエラーを検出します。

8.4.1 Statements with No Effects（効果の無い文）

Splintは効果の無い文に対してエラーを報告することが出来ます。 （no-effectフラグにより制御されます。） 変更句のため、Splintは伝統的なチェッカーよりもエラーを検知することが出来ます。no-effect-unconフラグがオンではない場合、 制約の無い関数は変更を行う可能性があるため、 制約の無い関数への呼び出しを伴う文に対して、エラーは報告されません。 図19はSplintの効果の無い文のチェックの例を示しています。

noeffect.c	Running Splint
extern void   nomodcall (int *x) /*@*/; /*@*/は何も変更しないし、 グローバル変数も使用もしないことの 簡略表記であることを思い出してください。 extern void mysterycall (int *x);   int noeffect (int *x, int y) {   y == *x;   nomodcall (x);   mysterycall (x);   return *x; }	> splint noeffect.c +noeffectuncon noeffect.c:6: Statement has no effect: y == *x noeffect.c:7: Statement has no effect: nomodcall(x) noeffect.c:8: Statement has no effect (possible     undetected modification through call to     unconstrained function mysterycall):     mysterycall(x)   8行目に対する警告は +noeffectuncon フラグがない場合は報告されません。

図 19.  効果の無い文

8.4.2 Ignored Return Values（無視された戻り値）

戻り値を無視している場合、Splintはエラーを報告します。 チェックは戻り値の型に基づいて制御されます： ret-val-intフラグはint型の 戻り値の無視についての報告を制御します。 bool型の戻り値に対しては ret-val-boolフラグ、 その他の全ての型に対しては、ret-val-othersフラグです。 関数文は、このエラーが報告されることを防ぐためにvoidへのキャストが行われても良いです。

代替型(Section 4.4)は 戻り値の型をvoidの代わりとなると宣言することによって 安全に無視されても良い値を返す関数を宣言するために使用可能です。 標準ライブラリのいくつかの関数は、結果を安全に無視できる 標準ライブラリ関数（例えば、strcpy）（Section 14.1参照） に対して戻り値無視のエラーを抑制するためvoidを返すと代えても良い と指定されています。 図20はSplintによって報告された戻り値の無視のエラーの例を示しています。

ignore.c	Running Splint
# include “bool.h” extern int fi (void); extern bool fb (void); extern int /*@alt void@*/   fv (void);   int ignore (void) {   8  fi ();   9  (void) fi (); 10  fb (); 11  fv (); 12  return fv (); }	> splint ignore.c   ignore.c:8: Return value (type int) ignored: fi() ignore.c:10: Return value (type bool) ignored: fb()   8行目に対するメッセージは ‑retvalint フラグが設定されている場合は報告されません。 10行目に対しては、 ‑retvalbool フラグです。     戻り値を void にキャストしているため、9行目に対してはメッセージはありません。 また、 fv関数が戻り値を voidとして良いと宣言されているため、 11行目に対しての メッセージはありません。

図 20.  無視された戻り値

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

Up: マニュアル

Prev: 7 Function Interfaces（関数インタフェース）

Next: 9 Buffer Sizes（バッファーサイズ）