このページの内容は最新ではありません。最新版の英語を参照するには、ここをクリックします。
ユーザー アサーション チェックのレビューと修正
このトピックでは、Polyspace® Code Prover™ で [ユーザー アサーション] チェックの結果を体系的にレビューする方法を説明します。
[ユーザー アサーション] チェックの修正を判断するまでこれらの手順の 1 つ以上に従います。このチェックを修正する方法は複数あります。チェックおよびコードの例については、ユーザー アサーションを参照してください。
特にオレンジ チェックに対して、チェックが実際のエラーを表すのではなく、コードに該当しない Polyspace 前提条件を表していると判定できます。前提条件を緩和するのに解析オプションを使用できる場合、そのオプションを使用して検証を再実行します。それ以外の場合は、結果またはコードにコメントおよび正当化情報を追加できます。
すべてのチェックに適用される一般的なワークフローについては、Polyspace デスクトップ ユーザー インターフェイスでの Code Prover の結果の解釈またはPolyspace Access Web インターフェイスでの Code Prover の結果の解釈 (Polyspace Access)を参照してください。
このチェックの使用方法:通常、デバッグ中に assert ステートメントを使用し、コード内の現在のポイントで条件が満たされているかどうかをチェックします。たとえば、変数 var がコード内の特定のポイントにおいて範囲 [1,10] の値を取ると想定する場合、そのポイントに以下のステートメントを置きます。
assert(var >=1 && var <= 10);
したがって、コードからの要件のテストを行う assert ステートメントを適切に挿入できます。
[ユーザー アサーション] チェックについてのレッドの結果は、明らかに要件が満たされていないことを示します。
[ユーザー アサーション] チェックについてのオレンジの結果は、要件が満たされていない可能性を示します。
手順 1: チェックの根本原因の判定
assert ステートメントに含まれる各変数のデータ フローをトレースします。
次の例では、myArray のデータ フローをトレースします。
int* getArray(int numberOfElements) {
.
.
arrayPtr = (int*) malloc(numberOfElements);
.
.
return arrayPtr;
}
void func() {
int* myArray = getArray(10);
assert(myArray!=NULL);
.
.
}getArray 内では malloc の戻り値は NULL に対してチェックされていない可能性があります。考えられる解決方法: 特定の要件を想定する場合、その要件を実行するテストがあるかどうかを確認します。この例では、getArray が非 NULL 値を返すと想定する場合、getArray 内で malloc の戻り値が NULL であるかをテストします。
データ フローをトレースするには、チェックを選択し、[結果の詳細] ペインの情報を確認します。
[結果の詳細] ペインでチェックにつながる命令の順序が表示される場合、各命令を選択します。
[結果の詳細] ペインでチェックに対して考えられる原因の行番号が表示される場合、[ソース] ペインで右クリックします。[行に移動] を選択します。行番号を入力します。
それ以外の場合、条件に含まれる各変数について、前のインスタンスを検索し、チェックの根本原因へ逆にトレースします。一般的な根本原因についての詳細は、手順 3: チェックの一般的な原因の検索を参照してください。
変数に応じて、以下のナビゲーション ショートカットを使用し、前のインスタンスを検索します。以下の手順は、Polyspace ユーザー インターフェイスでのみ実行できます。
変数 変数の前のインスタンスの検索方法 ローカル変数
次のいずれかの方法を使用してください。
変数の検索。
変数を右クリックします。[すべての参照を検索] を選択します。
変数のすべてのインスタンスは、現在のインスタンスが強調表示されて [検索] ペインに表示されます。
[検索] ペインで前のインスタンスを選択します。
ソース コードの参照。
[ソース] ペインで変数をダブルクリックします。
変数のすべてのインスタンスは強調表示されます。
上にスクロールして前のインスタンスを検索します。
グローバル変数
変数を右クリックします。オプション [変数アクセス ビューで表示] が表示される場合、変数はグローバル変数です。
オプション [変数アクセス ビューで表示] を選択します。
[変数アクセス] ペインでは、変数の現在のインスタンスが表示されます。
このペインで、変数の前のインスタンスを選択します。
変数の書き込み操作は
で示され、読み取り操作は 
で示されます。
関数の戻り値
ret=func();
関数定義を検索します。
[ソース] ペインの
funcを右クリックします。オプションが存在する場合、[定義に移動] を選択します。Polyspace で定義を利用できない場合は、オプションを選択すると関数宣言に移動します。funcの定義では、各returnステートメントを特定します。関数が返す変数が逆にトレースするための新しい変数です。
任意の操作に含まれる変数が前の操作に関連しているかどうかを判断することもできます。コード内の変数間の関係の検出を参照してください。
手順 2: チェックの一般的な原因の検索
チェックがオレンジで、関数内で発生する場合、関数が複数回呼び出されているかどうかを確認します。アサーションが特定の呼び出しでのみ失敗するかどうかを特定します。それらの呼び出しについては、呼び出し元本体に移動し、アサーションの要件を実行するテストがあるかどうかを確認します。
関数の呼び出し元を確認するには、[ソース] ペインで関数名を選択します。すべての呼び出し元は [呼び出し階層] ペインに表示されます。呼び出し元名を選択し、ソース内でそこに移動します。
呼び出しのサブセットによりオレンジ チェックが発生しているかどうかを特定するには、
状況依存性 (-context-sensitivity)オプションを使用します。チュートリアルについては、ランタイム エラーのある関数呼び出しの特定を参照してください。
アサーションの要件を実行するテストがある場合、以下であるかどうかを確認します。
アサーション ステートメントはテストのスコープ内にある。
テストとアサーションの間でテスト用変数を変更している。
たとえば、テスト
if(index < SIZE)は、indexがSIZEより小さくなるように実行されます。ただし、アサーションassert(index < SIZE)は次の場合に失敗する可能性がります。ifブロックの外で発生している。アサーションの前で、
ifブロック内のindexを変更している。
考えられる解決方法: アサーションの要件を満たさなければならないのかどうかを十分に検討してください。これらの要件を満たす必要がある場合、要件を実行するテストを行います。テストの後は、テスト用変数の変更は避けてください。
手順 3: Polyspace の前提条件へのチェックをトレース
コードの前方で発生する Polyspace 前提条件にオレンジ チェックをトレースできるかどうかを確認します。前提条件があてはまらない場合、結果またはコードにコメントまたは正当化情報を追加します。Polyspace ユーザー インターフェイスでのバグ修正または正当化による結果への対処またはPolyspace Access でのバグ修正または正当化による結果への対処 (Polyspace Access)を参照してください。
たとえば、関数呼び出し後、2 つの変数間の関係をアサートするとします。ここで、次のようにします。
関数呼び出しの深さとコードの複雑度に応じて、Polyspace は変数範囲を近似できる場合があります。近似のために、ソフトウェアは関係が適用されるかどうか証明できないため、[ユーザー アサーション] オレンジ チェックを生成します。
オレンジ チェックに動的テストを実行し、アサーションが失敗するかどうかを判定します。
コード複雑度を低減し、検証を再実行してみてください。それ以外の場合は、結果またはコードにコメントおよび正当化情報を追加し、コードを変更しなかった理由について説明します。
詳細は、Code Prover 解析の前提条件を参照してください。
メモ
オレンジ チェックを正当化する前に、コード設計を改善できるかどうかを十分に検討してください。
