Polyspace Code Prover 解析結果のレビュー

Polyspace^® Code Prover™ では、C/C++ コードを網羅的にチェックし、特定のタイプのランタイム エラーがないことを証明します (静的解析または検証)。解析の実行に使用する方法に関係なく、結果は後で Polyspace ユーザー インターフェイスで開きます。

例のファイル

このチュートリアルの手順に従うには、デスクトップでの PolyspaceCode Prover の実行の手順を使用して Polyspace を実行します。または、Polyspace ユーザー インターフェイスで、[ヘルプ] 、 [例] 、 [Code_Prover_Example.psprj] を使用して結果の例を開きます。以前に結果の例を読み込んでいくつかの変更を加えたことがある場合、新しいコピーを読み込むために、[ヘルプ] 、 [例] 、 [既定の例を復元] を選択します。

結果の解釈

各 Polyspace 結果をレビューします。問題の根本原因を見つけます。

[結果のリスト] ペインにある結果のリストから開始します。

• [結果のリスト] ペインがウィンドウ全体に表示されている場合は、[ウィンドウ] 、 [レイアウトのリセット] 、 [結果のレビュー] を選択します。

• 結果のフラット リストが表示されておらず、代わりに結果がグループ化されて表示されている場合は、 リストから [なし] を選択します。

[ファミリ] 列ヘッダーをクリックし、重要性に基づいて結果を並べ替えます。ファイル example.c のレッドの [不適切にデリファレンスされたポインター] チェックを選択します。レッド チェックは、解析で考慮されるすべての実行パスでそのエラーが発生することを示します。

[ソース] ペインにソース コードが表示され、[結果の詳細] ペインに結果についての詳細情報が表示されます。

[不適切にデリファレンスされたポインター] の結果に関する [結果の詳細] ペインのメッセージは、ポインター p が 400 バイトの許容されるバッファーを持つことを示します。これは、バッファーの先頭から 400 バイトの位置から始まる場所を指しており、4 バイトのデータ型を指しています。

問題をさらに調査して根本原因を見つけるには、[ソース] ペインの変数 p を右クリックして、[すべての参照を検索] を選択します。各検索結果をクリックして、ソース コードの対応する場所に移動します。各場所で、変数 p の上にカーソルを置き、コード内のその時点における変数の値を説明するツールヒントを確認します。

ポインター変数 p が 100 要素の int 配列に初期化されていることがわかります。ポインターは、100 回反復する for ループで配列を走査し、配列の終わりを指します。レッドの [不適切にデリファレンスされたポインター] チェックの付いた行でこのポインターはデリファレンスされ、配列外のメモリ位置のデリファレンスが発生します。

その他の情報

詳細は、以下を参照してください。

• Polyspace デスクトップ ユーザー インターフェイスでの Code Prover の結果の解釈

• Code Prover の結果とソース コードの色

• Polyspace Code Prover のすべての結果のリスト

バグ修正またはコメントによる結果への対処

Polyspace 検出の根本原因を理解したら、コードを修正できます。そうしない場合は、Polyspace の結果にコメントを追加して、後でコードを修正するか、結果を正当化します。コメントを使用して、レビュー進行状況を追跡できます。

[ソース] ペインの変数 p を右クリックします。[エディターを開く] を選択します。テキスト エディターでコードを開きます。問題を修正します。たとえば、for ループの後に、ポインターが配列の先頭を指すようにすることができます。コードの変更は以下で強調表示されています。

...
int i, *p = array;

for (i = 0; i < 100; i++) {
    *p = 0;
     p++;
}

p = array;

if (get_bus_status() > 0)
...

解析を再実行すると、レッドの [不適切にデリファレンスされたポインター] チェックは表示されません。

または、欠陥をすぐに修正しないなら、ステータス [To investigate] を結果に割り当てます。必要に応じて、詳細な説明を含むコメントを追加します。

ステータス [No action planned] を割り当てた場合、同じプロジェクトに対する以降の実行では結果が表示されません。

その他の情報

詳細は、以下を参照してください。

• Polyspace ユーザー インターフェイスでのバグ修正または正当化による結果への対処

• コードへの注釈付けと既知の結果または許容可能な結果の非表示

結果の管理

Code Prover 解析の結果を開くと、実行時チェック、コーディング ルール違反などの結果のリストが表示されます。レビューを整理するには、リストを絞り込むか、ファイルまたは結果のタイプ別に結果をグループ化します。

たとえば、次のようにします。

• レッド チェックおよび重要なオレンジ チェックのみをレビューします。

  [ファミリ] 列ヘッダーをクリックして、チェックを色で並べ替えます。または、レッドおよびオレンジ チェック以外の結果を除外できます。フィルター処理を開始するには、列ヘッダー上の アイコンをクリックします。

  

  パス関連のオレンジ チェックは重要性が高い可能性があるため、パス関連のオレンジ チェックのみをレビューできます。その他のチェックを除外するには、[情報] 列のフィルターを使用します。[すべて] フィルターをオフにし、[出発点: パス関連の問題] というフィルターを選択します。

• 前回の解析以降に見つかった新しい結果のみをレビューする。

  [結果のリスト] ペインのツール バーで [新規] ボタンをクリックします。

• 特定のファイルまたは関数の結果をレビューする。

  [結果のリスト] ペインのツール バーで、 リストから [ファイル] を選択します。

その他の情報

詳細は、以下を参照してください。

• Polyspace デスクトップ ユーザー インターフェイスでの結果のフィルター処理とグループ化

• チェック レビューの優先順位