正確性の条件チェックのレビューと修正

このトピックでは、Polyspace^® Code Prover™ で [正確性の条件] チェックの結果を体系的にレビューする方法を説明します。

[正確性の条件] チェックの修正を判断するまでこれらの手順の 1 つ以上に従います。レッドチェックまたはオレンジチェックを修正する方法は複数あります。チェックおよびコードの例については、正確性の条件を参照してください。

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

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

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

[結果のリスト] ペインで、チェックを選択します。[結果の詳細] ペインで、チェックの原因を確認します。次のリストには、考えられる原因の一部が表示されます。

配列がよりサイズの大きい別の配列に変換されている。
次の例では、配列がよりサイズの大きい別の配列に変換されるためにレッドチェックが発生します。
デリファレンス時に関数ポインターが値 NULL をもつ。
次の例では、デリファレンス時に関数ポインターが値 NULL をもつためにレッドチェックが発生します。
デリファレンス時に関数ポインターが関数を指していない。
次の例では、Polyspace はデリファレンス時に関数ポインターが関数を指しているかどうかを判断できないためオレンジチェックが発生します。この状況は、たとえば絶対アドレスを関数ポインターに割り当てる場合に発生することがあります。
関数ポインターが関数を指しているが、ポインターおよび関数の引数の型が一致しない。以下に例を示します。
```
typedef int (*typeFuncPtr) (complex*);
int func(int* x);
.
.
typeFuncPtr funcPtr = &func;
```
次の例では、レッドチェックが発生します。その理由は次のとおりです。
- 関数ポインターが関数 func を指す。
- func に int 型の引数を想定するが、対応する関数ポインターの引数は構造体である。
関数ポインターは関数を指しているが、ポインターおよび関数の引数の数が一致しない。以下に例を示します。
```
typedef int (*typeFuncPtr) (int, int);
int func(int);
.
.
typeFuncPtr funcPtr = &func;.
```
次の例では、レッドチェックが発生します。その理由は次のとおりです。
- 関数ポインターが関数 func を指す。
- func は 1 つの引数を想定するが、関数ポインターには 2 つの引数がある。
関数ポインターは関数を指すが、ポインターおよび関数の戻り値の型が一致しない。以下に例を示します。
```
typedef double (*typeFuncPtr) (int);
int func(int);
.
.
typeFuncPtr funcPtr = &func;
```
次の例では、レッドチェックが発生します。その理由は次のとおりです。
- 関数ポインターが関数 func を指す。
- func は値 int を返すが、関数ポインターの戻り値の型は double である。
変数の値が [グローバルアサート] モードで指定する範囲外にある。Polyspace 解析のグローバル変数範囲の制約を参照してください。
次の例では、レッドチェックが発生します。その理由は次のとおりです。
- 変数 glob に対して 0...10 の範囲を指定している。
- 変数の値がこの範囲外にある。

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

[結果の詳細] ペインのチェック情報に基づいて、根本原因を特定するために次の手順を実行します。以下の手順は、Polyspace ユーザーインターフェイスでのみ実行できます。

チェック情報根本原因の特定方法

チェック情報	根本原因の特定方法
配列がよりサイズの大きい別の配列に変換されている。	配列サイズを判定するには、各配列変数の定義を参照してください。変数を右クリックし、[定義に移動] を選択します。動的にメモリを配列を割り当てると、そのサイズを定義時に利用できない可能性があります。配列変数のすべてのインスタンスを参照し、メモリを配列に割り当てる場所を検索します。変数を右クリックします。[すべての参照を検索] を選択します。変数のすべてのインスタンスは、現在のインスタンスが強調表示されて [検索] ペインに表示されます。 [検索] ペインで前のインスタンスを選択します。
関数ポインターのデリファレンス時の問題は以下のとおりです。関数ポインターがデリファレンス時に `NULL` 値となる。関数ポインターがデリファレンス時に関数を指さない。関数ポインターは関数を指すが、ポインターおよび関数の引数の型が一致しない。関数ポインターは関数を指すが、ポインターおよび関数の引数の数が一致しない。関数ポインターは関数を指すが、ポインターおよび関数の戻り値の型が一致しない。	関数ポインターを関数に割り当てる場所を検索します。関数ポインターを右クリックします。[すべての参照を検索] を選択します。関数ポインターのすべてのインスタンスは、現在のインスタンスが強調表示されて [検索] ペインに表示されます。 [検索] ペインで前のインスタンスを選択します。引数と関数ポインター型および関数の戻り値の型を決定します。これらの 2 つに不一致があるかどうかを特定します。たとえば、次の例では `typeFuncPtr` および `func` の引数と戻り値の型を決定します。 typeFuncPtr funcPtr = func; 関数ポインター型を右クリックし、[定義に移動] を選択します。関数を右クリックし、[定義に移動] を選択します。定義が存在しない場合、このオプションは関数スタブの定義を代わりに表示します。この場合、関数宣言を検索します。一致するシグネチャをもつ関数への関数ポインターを代入しても、その代入が到達不能になる場合があります。このケースに当てはまるかどうかをチェックします。
変数の値が [グローバルアサート] モードで指定する範囲外にある。	グローバル変数の前のインスタンスをすべて参照します。変数を制約するために適切なポイントを特定します。変数を右クリックします。[変数アクセスビューで表示] を選択します。 [変数アクセス] ペインでは、変数の各インスタンスを選択します。

配列がよりサイズの大きい別の配列に変換されている。

配列サイズを判定するには、各配列変数の定義を参照してください。
変数を右クリックし、[定義に移動] を選択します。
動的にメモリを配列を割り当てると、そのサイズを定義時に利用できない可能性があります。配列変数のすべてのインスタンスを参照し、メモリを配列に割り当てる場所を検索します。
1. 変数を右クリックします。[すべての参照を検索] を選択します。
  変数のすべてのインスタンスは、現在のインスタンスが強調表示されて [検索] ペインに表示されます。
2. [検索] ペインで前のインスタンスを選択します。

関数ポインターのデリファレンス時の問題は以下のとおりです。

関数ポインターがデリファレンス時に NULL 値となる。
関数ポインターがデリファレンス時に関数を指さない。
関数ポインターは関数を指すが、ポインターおよび関数の引数の型が一致しない。
関数ポインターは関数を指すが、ポインターおよび関数の引数の数が一致しない。
関数ポインターは関数を指すが、ポインターおよび関数の戻り値の型が一致しない。

関数ポインターを関数に割り当てる場所を検索します。
1. 関数ポインターを右クリックします。[すべての参照を検索] を選択します。
  関数ポインターのすべてのインスタンスは、現在のインスタンスが強調表示されて [検索] ペインに表示されます。
2. [検索] ペインで前のインスタンスを選択します。
引数と関数ポインター型および関数の戻り値の型を決定します。これらの 2 つに不一致があるかどうかを特定します。たとえば、次の例では typeFuncPtr および func の引数と戻り値の型を決定します。
```
typeFuncPtr funcPtr = func;
```
1. 関数ポインター型を右クリックし、[定義に移動] を選択します。
2. 関数を右クリックし、[定義に移動] を選択します。定義が存在しない場合、このオプションは関数スタブの定義を代わりに表示します。この場合、関数宣言を検索します。
一致するシグネチャをもつ関数への関数ポインターを代入しても、その代入が到達不能になる場合があります。このケースに当てはまるかどうかをチェックします。

変数の値が [グローバルアサート] モードで指定する範囲外にある。

グローバル変数の前のインスタンスをすべて参照します。変数を制約するために適切なポイントを特定します。

変数を右クリックします。[変数アクセスビューで表示] を選択します。
[変数アクセス] ペインでは、変数の各インスタンスを選択します。

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

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