初期化されていない戻り値チェックのレビューと修正

このトピックでは、Polyspace^® Code Prover™ で [初期化されていない戻り値] チェックの結果を体系的にレビューする方法を説明します。

[初期化されていない戻り値] チェックの修正を判断するまでこれらの手順の 1 つ以上に従います。このチェックを修正する方法は複数あります。チェックおよびコードの例については、初期化されていない戻り値を参照してください。

特にオレンジチェックに対して、チェックが実際のエラーを表すのではなく、コードに該当しない Polyspace 前提条件を表していると判定できます。前提条件を緩和するのに解析オプションを使用できる場合、そのオプションを使用して検証を再実行します。それ以外の場合は、結果またはコードにコメントおよび正当化情報を追加できます。

すべてのチェックに適用される一般的なワークフローについては、Polyspace デスクトップユーザーインターフェイスでの Code Prover の結果の解釈またはPolyspace Access Web インターフェイスでの Code Prover の結果の解釈 (Polyspace Access)を参照してください。

手順 1: チェック情報の解釈

[結果のリスト] ペインで、チェックを選択します。[結果の詳細] ペインで、チェックに関する詳細を確認します。

[結果の詳細] ペインに表示されている場合、考えられるチェックの原因を確認します。

前述の例では、スタブ関数 inputRep が考えられる原因として識別されています。

考えられる解決方法: チェックを回避するために、inputRep の引数または戻り値を制約します。たとえば、inputRep が 1..10 などの特定の範囲内で値を返すよう指定します。詳細については、スタブ関数に関する Code Prover の仮定を参照してください。

手順 2: チェックの根本原因の判定

関数本体内でチェックの根本原因を判定します。以下の手順は、Polyspace ユーザーインターフェイスでのみ実行できます。

関数定義に移動します。
チェックを含む関数呼び出しを右クリックします。オプションが存在する場合、[定義に移動] を選択します。
関数本体内で return ステートメントが関数の右中かっこの前で発生しているかどうかをチェックします。
return ステートメントが存在しない場合、次の手順に従います。
1. [検索] ペインで return という語を検索するか、関数本体を手動でスクロールして return ステートメントを検索します。
2. return ステートメントごとに、ステートメントが関数スコープより小さいスコープで表示されるかどうかを特定します。
  たとえば、return ステートメントは if-else ステートメントの 1 つの分岐でのみ発生するとします。
考えられる解決方法: return ステートメントを関数本体の最後に置けるかどうかを確認します。たとえば、次のコード
```
int func(int ch) {
    switch(ch) {
        case 1: return 1;
        break;
        case 2: return 2;
        break;
    }
}
```
を、以下のコードで置き換えます。
```
int func(int ch) {
    int temp;
    switch(ch) {
        case 1: temp = 1;
        break;
        case 2: temp = 2;
        break;
    }
    return temp;
}
```
これを実行する方法についての詳細は、Return ステートメントの数を参照してください。

手順 3: チェックの一般的な原因の検索

[初期化されていない戻り値] チェックの一般的な原因を確認します。

return ステートメントが if-else、for または while ブロックに表示されるかどうかを確認します。関数がブロックに入らないときに、条件を特定します。
たとえば、特定の関数入力について関数が while ブロックに入らない場合があるとします。
考えられる解決方法:
- return ステートメントを関数本体の最後に置けるかどうかを確認します。
- それ以外の場合は、関数がブロックに入らないときに条件を回避する方法を特定します。
  たとえば、関数が特定の入力に対してブロックに入らない場合、別の入力を渡す必要があるかどうかを確認します。
通常の制御フローに割り込む goto などのコードの構成要素があるかどうかを確認します。これらのコードの構成要素が理由で関数内の return ステートメントが到達できない条件があるかどうかを確認します。
考えられる解決方法:
- goto ステートメントを回避します。これを実行する方法についての詳細は、Goto ステートメントの数を参照してください。
- それ以外の場合は、関数内の return ステートメントが到達できない条件を回避する方法を特定します。

手順 4: Polyspace の前提条件へのチェックをトレース

コードの前方で発生する Polyspace 前提条件にオレンジチェックをトレースできるかどうかを確認します。前提条件があてはまらない場合、結果またはコードにコメントまたは正当化情報を追加します。Polyspace ユーザーインターフェイスでのバグ修正または正当化による結果への対処またはPolyspace Access でのバグ修正または正当化による結果への対処 (Polyspace Access)を参照してください。

たとえば、 return ステートメントが if-elseif ブロックの分岐にはありますが、最後の else ブロックがないとします。if-elseif ブロックでテストしている条件には未定義の関数から取得した変数が含まれています。ここで、次のようにします。

Polyspace では、これらの変数の特定の値はどの if-elseif ブロックにも入らないと仮定します。
したがって、return ステートメントに到達しない可能性があります。
変数のこれらの値が発生しないことがわかっている場合、コメントおよび正当化情報を追加し、コードを変更しなかった理由を説明します。

詳細については、Code Prover 解析の前提条件を参照してください。

このチェックを無効にする

このチェックは無効にできます。このチェックを無効にすると、Polyspace では、関数に return ステートメントがない場合に、その関数の戻り値について、次のように仮定します。

戻り値が非ポインター変数である場合、その型で許容される全範囲の値を取ります。
戻り値がポインターである場合、NULL 値を取るか、メモリブロックを不明なオフセットで指します。

詳細については、未初期化のチェックを無効にする (-disable-initialization-checks)を参照してください。