Polyspace Access Web インターフェイスでの Code Prover の結果の解釈

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

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

• ツールストリップにあるフィルターを使用してリストを絞り込みます。たとえば、影響度の高い欠陥にフォーカスできます。

• [結果のリスト] の列ヘッダーをクリックし、その列の内容に基づいてリストを並べ替えます。たとえば、[グループ] または [ファイル] で並べ替えることができます。

  Code Prover 実行時チェックの結果は以前のチェックの結果によって異なるため、実行時チェックの調査は関数の最初から最後に向かって行うと便利です。

Polyspace Access Web インターフェイスでの結果のフィルタリングと並べ替えも参照してください。リストを絞り込んだら、個別の結果のレビューを開始できます。このトピックでは、結果のレビュー方法を説明します。

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

結果の解釈

メッセージの解釈

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

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

• 次のチェックの色およびアイコン。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 の実行時チェックのレビュー (Polyspace Code Prover)を参照してください。

[ソース コード] ペインで現在選択している結果から移動した後に、[ソース コード] ペインでのその結果の場所に戻るには、[結果の詳細] ペインで アイコンをクリックします。

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

[ソース コード] ペインでのナビゲーションと Polyspace アクションの保存

Polyspace の [ナビゲーション履歴] ペインには、特定のレビュー ワークフロー アクションが表示されます。

[ナビゲーション履歴] ペインでアクションをクリックすると、[結果の詳細] ペインにそのアクションに関連する結果が表示されます。次に [ソース コード] ペイン内で、そのアクションに関連付けられているコードの場所に移動します。結果のレビュー プロセスを進める際、[ナビゲーション履歴] ペインを使用して以前の結果を再び参照し、[ソース コード] ペインで関連するコードを見つけます。

Polyspace が記録するアクションには以下が含まれます。

• [結果のリスト] ペインでの結果の選択

• [ソース コード] ペインの右クリック メニューからの [ナビゲーション履歴で位置を保持] の選択

• [エラー呼び出しグラフ] や [変数アクセス グラフ] などのグラフ内でのノードの選択

• [コード検索]、[呼び出し階層]、[グローバル変数の使用]、または [グローバル変数アクセス] ペインでの行の選択

[ナビゲーション履歴] ペインで重要なアクションにフラグを設定するには、そのアクションの行番号をクリックします。

アイコンをクリックすると、[ナビゲーション履歴] ペインからすべてのアクションが削除されます。

参考

トピック

• Polyspace Access Web インターフェイスでの結果のフィルタリングと並べ替え
• Polyspace Access でのバグ修正または正当化による結果への対処