このページの内容は最新ではありません。最新版の英語を参照するには、ここをクリックします。
範囲外の配列インデックス チェックのレビューと修正
このトピックでは、Polyspace® Code Prover™ で [範囲外の配列インデックス] チェックの結果を体系的にレビューする方法を説明します。
[範囲外の配列インデックス] チェックの修正を判断するまでこれらの手順の 1 つ以上に従います。このチェックを修正する方法は複数あります。チェックおよびコードの例については、範囲外の配列インデックスを参照してください。
特にオレンジ チェックに対して、チェックが実際のエラーを表すのではなく、コードに該当しない Polyspace 前提条件を表していると判定できます。前提条件を緩和するのに解析オプションを使用できる場合、そのオプションを使用して検証を再実行します。それ以外の場合は、結果またはコードにコメントおよび正当化情報を追加できます。
すべてのチェックに適用される一般的なワークフローについては、Polyspace デスクトップ ユーザー インターフェイスでの Code Prover の結果の解釈またはPolyspace Access Web インターフェイスでの Code Prover の結果の解釈 (Polyspace Access)を参照してください。
手順 1: チェック情報の解釈
[ 記号の上にカーソルを置きます。
ツールヒントから次の情報を取得します。
配列サイズ。配列インデックスの許容範囲は 0 から (配列サイズ - 1) です。
配列インデックスの実際の範囲
前述の例の場合、配列のサイズは 10 です。したがって、配列インデックスの許容範囲は 0 ～ 9 です。ただし、実際の範囲は 0 ～ 10 です。
考えられる解決方法: 範囲外の配列インデックスを回避するには、インデックスが 0 と (配列サイズ - 1) の間にある場合のみ配列にアクセスします。
#define SIZE 100 int arr[SIZE]; . . if(i<SIZE) val = arr[i] else /*Error handling */
手順 2: チェックの根本原因の判定
配列サイズを調べる、あるいは変更する場合、配列変数を右クリックし、オプションが存在する場合には [定義に移動] を選択します。それ以外の場合は、配列インデックス変数から開始するデータ フローをトレースします。インデックス変数を制約できるポイントを特定します。
データ フローをトレースするには、チェックを選択し、[結果の詳細] ペインの情報を確認します。
[結果の詳細] ペインでチェックにつながる命令の順序が表示される場合、各命令を選択します。
[結果の詳細] ペインに、そのチェックの考えられる原因の行番号が表示される場合、[ソース] ペインを右クリックします。[行に移動] を選択します。
そうしない場合は、次のようになります。
配列インデックス変数の前のインスタンスを検索します。
それらのインスタンスを参照します。配列インデックス変数を (配列サイズ - 1) に制約するインスタンスを検索します。
考えられる解決方法: インデックス変数を制約するインスタンスが見つからない場合、変数に制約を指定します。以下に例を示します。
if(index<SIZE) read(array[index]);
制約が [範囲外の配列インデックス] エラーが発生するインスタンスに適用されるかどうかを特定します。
たとえば、
for(index=0; index<SIZE; index++)を使用してforループ内のインデックス変数を制約できます。ただし、制約が適用されないループの外側にある配列にアクセスしています。考えられる解決方法: 制約が適用されない理由を調べます。インデックス変数を再度制約しなければならないのかどうかを確認します。
インデックス変数が別の変数から取得されている場合、2 番目の変数のデータ フローをトレースします。2 番目の変数を (配列サイズ - 1) に制約したかどうかを判定します。
変数に応じて、以下のナビゲーション ショートカットを使用し、前のインスタンスを検索します。以下の手順は、Polyspace ユーザー インターフェイスでのみ実行できます。
| 変数 | 変数の前のインスタンスの検索方法 |
|---|---|
ローカル変数 | 次のいずれかの方法を使用してください。
|
グローバル変数 変数を右クリックします。オプション [変数アクセス ビューで表示] が表示される場合、変数はグローバル変数です。 |
|
関数の戻り値
ret=func(); |
|
任意の操作に含まれる変数が前の操作に関連しているかどうかを判断することもできます。コード内の変数間の関係の検出を参照してください。
手順 3: チェックの一般的な原因の検索
[範囲外の配列インデックス] チェックの一般的な原因を確認します。
配列インデックス変数を 0 から開始しているかどうかを確認します。
配列インデックス変数を制約する条件では、
<の使用を意図するときに<=を使用するかどうかを確認します。チェックが
forまたはwhileループ内またはその直後に発生する場合、ループの実行回数を減らさなければならないかどうかを判定します。関数
sizeofを使用して配列を制約する場合、配列サイズを求めるためにsizeof(array)をsizeof(array[0])で除算しているかどうかを確認します。sizeof(array)は配列サイズをバイト単位で返します。
手順 4: Polyspace の前提条件へのチェックをトレース
コードの前方で発生する Polyspace 前提条件にオレンジ チェックをトレースできるかどうかを確認します。前提条件があてはまらない場合、結果またはコードにコメントまたは正当化情報を追加します。Polyspace ユーザー インターフェイスでのバグ修正または正当化による結果への対処またはPolyspace Access でのバグ修正または正当化による結果への対処 (Polyspace Access)を参照してください。
たとえば、定義を指定していない関数を使用して配列インデックスを制約するとします。ここで、次のようにします。
Polyspace では、配列インデックス変数が制約されているかどうか判定できません。
この変数を配列インデックスとして使用すると、[範囲外の配列インデックス] エラーが発生する可能性があります。
変数が配列サイズに制約されていることがわかっている場合、コメントおよび正当化情報を追加し、コードを変更しなかった理由を説明します。
詳細は、Code Prover 解析の前提条件を参照してください。
メモ
オレンジ チェックを正当化する前に、コード設計を改善できるかどうかを十分に検討してください。
たとえば、1 つの関数でグローバル変数を制約し、それを 2 番目の関数で配列インデックスとして使用するのはコードの脆弱性につながります。新しい関数が前の 2 つの関数の間で呼び出され、グローバル変数を変更する場合、制約は適用されなくなります。
