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

このトピックでは,Polyspaceデスクトップ製品のユーザーインターフェイスで公关代码over 検証結果をレビューする方法を説明します。Polyspace Access Web インターフェイスで検証結果をレビューする方法については、を参照してください。

Polyspace^®Code Prover™解析の結果を開くと、[検証結果のリスト]ペインにリストが表示されます。リストは、実行時チェック、コーディングルール違反、コードメトリクスおよびグローバル変数の使用で構成されています。

まず、以下のようにしてレビューのフォーカスを絞り込むことができます。

検証結果リストの列のフィルターを使用します。たとえば、レッドチェックにフォーカスできます。
検証結果をファイルおよび関数別に整理します。リストの上のアイコンを使用します。
Code Prover 実行時チェックの結果は以前のチェックの結果によって異なるため、実行時チェックの調査は関数の最初から最後に向かって行うと便利です。

Polyspace デスクトップユーザーインターフェイスでの検証結果のフィルター処理とグループ化も参照してください。リストを絞り込んだら、個別の検証結果のレビューを開始できます。このトピックでは、検証結果のレビュー方法を説明します。

レビューを開始するには、リスト内の検証結果を選択します。

検証結果の解釈

メッセージの解釈

最初の手順は問題が何かを理解することです。[検証結果の詳細]ペインのメッセージと、[ソース]ペインの関連するコード行を確認します。

この時点で、問題を修正するかどうかの判断ができる可能性があります。

メッセージは次のいくつかの部分で構成されています。

次のチェックの色およびアイコン。Code Prover 検証結果とソースコードの色を参照してください。ランタイムエラーのチェックの場合は以下です。
- :レッドは明確なエラーを示します。
- :オレンジは潜在的なエラーを示します。
- :グレーは到達不能コードを示します。
- :グリーンは特定のエラーが発生しないことを示します。
実行時チェックの説明。
前述の例では、チェックにより、配列インデックスが配列の範囲外になるかどうかが判別されます。
実行時チェックに関連する値。
この例では、メッセージに、配列サイズ (127)、配列範囲 (0..126) およびその時点のコードで配列インデックス変数が取ることのできる値の範囲 (0..555) が示されています。
関連する不正確さの原因 (オレンジチェックの場合)。
この例では、メッセージに、チェックの原因となっている可能性がある 2 つの volatile 変数が示されています。

ソースコードツールヒントでの変数範囲の確認

[ソース]ペインでは、ツールヒントのある変数と演算に下線が付けられます。

この例では、以下に対してツールヒントが表示されます。

s8_ret:+演算の前のデータ型と値の範囲が表示されます。
+ 演算中にデータ型変換が発生する場合、この変換はツールヒントにも表示されます。
+:左オペランドと右オペランドの値、およびその結果が表示されます。
=:代入中に発生するすべてのデータ型変換とその結果が表示されます。

追加のヘルプの表示

場合によって、特定の検証結果に関する追加のヘルプが必要なことがあります。選択した検証結果に関するヘルプページを開くには、アイコンをクリックします。検証結果を示すコード例を確認します。

検証結果の根本原因の検出

場合によって、検証結果が表示された実際の場所から遠い場所に根本原因が存在することがあります。たとえば、初期化が到達不能であるために、読み取る変数が未初期化である場合があります。この欠陥は変数を読み取る際に表示されますが、その根本原因は、常に false となる以前のif条件またはwhile条件である可能性があります。

ソースコードでの移動

[検証結果の詳細]ペインには、検証結果につながるイベントの順序が表示される場合があります。ただし、ほとんどの場合、コード内の独自の移動経路を特定する必要があります。コード内を移動しながら、変数のツールヒントを使用して、変数範囲の伝播をたどります。

int func (int var) { /* Initial range of var */ … var -= get (); /* New range of var */ … set(&var); /* New range of var */ }

ユーザーインターフェイスで、以下の簡単な移動経路を使用します。

変数へのすべての参照を検索して、それらを参照します。
[ソース]ペインで変数名を右クリックし、[すべての参照を検索]を選択します。または、その変数をダブルクリックします。これらのオプションが実行するのは、単なる文字列照合だけではありません。これらのオプションを使用すると、特定の変数のインスタンスのみが表示され、スコープの異なる同名の他の変数は表示されません。
関数呼び出しから定義に移動します。
[ソース]ペインで関数名を右クリックします。[定義に移動]を選択します。
関数からその呼び出し元および呼び出し先に移動します。
[検証結果の詳細]ペインのアイコンをクリックします。検証結果を含む関数とその呼び出し元および呼び出し先が表示されます。呼び出しサイトに移動するには、呼び出し元または呼び出し先の名前をクリックします。定義に移動するには、名前をダブルクリックします。
あるいは、アイコンをクリックして、検証結果につながる呼び出し順序のグラフ表示を確認します。この順序内の関数に移動するには、グラフのノードをクリックします。
関数呼び出しまたはループキーワードから、関数またはループ本体のエラーに移動します。
特定の関数呼び出しまたは特定のループ反復でのみエラーが発生する場合、その関数呼び出しまたはループ反復は赤で強調表示されます。赤の関数呼び出しまたはループキーワードを右クリックします。オプションが利用できる場合、[原因に移動]を選択します。
グローバル変数のすべてのインスタンスに移動します。
[検証結果の詳細]ペインのアイコンをクリックします。検証結果のすべてのグローバル変数およびそれらに対する読み取り/書き込み操作を確認します。

コード内の経路の移動を開始する前に、調査対象を決定し、適切なナビゲーションツールを選択します。次に例を示します。

[未初期化変数]チェックを調べるには、変数がまったく初期化されていないことの確認が必要な場合があります。変数の前のインスタンスを調査し、初期化されているかどうかを確認します。
以下の[MISRA C:2012 Rule 17.7]の違反を調査する場合、
```
The value returned by a function having non-void return type shall be used.
```
関数呼び出しから関数定義への移動が必要なことがあります。

他の調査対象の例については、Code Prover の実行時チェックを参照してください。現在の検証結果から移動した後にその検証結果に戻るには、[検証結果の詳細]ペインのアイコンを使用します。

検証結果が含まれるソースコードのトークンをクリックしても、[検証結果のリスト]における前の検証結果の選択と[検証結果の詳細]ペインの詳細は変更されません。ソースコード内の移動中に、検証結果のリスト内の検証結果とピン留めした検証結果の詳細を維持できます。場合によっては、トークンに関連付けられている検証結果の確認が必要になります。検証結果の選択と詳細を更新するには、Ctrlキーを押しながらトークンをクリックするかトークンを右クリックして、[この位置における結果の選択]を選択します。