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

このトピックでは、Polyspace^® Code Prover™ 解析の結果表示に使用されるさまざまな色について説明します。

結果の色

Polyspace では、さまざまな結果が特定のアイコンと色で [結果のリスト] ペインと [結果の詳細] ペインに表示されます。

実行時チェック

Polyspace Code Prover は、コードの各演算について特定のランタイム エラーがないかどうかをチェックします。すべてまたは一部の実行パスにおけるランタイム エラーの有無が証明されているかどうかに応じて、演算が色分けされます。

チェックの色	目的	例	アイコン
レッド	すべての実行パスで特定のエラーの原因になることが証明された演算が強調表示されます*。 Polyspace Code Prover 検証では、言語の規格を基準にしてエラーを判定します。一部のエラーは特定のコンパイル環境では許容されますが、言語の規格に違反します。一部の環境依存動作を許可するには、適切な解析オプションを使用します。詳細は、検証の前提条件とチェック動作を参照してください。	レッドの [オーバーフロー]: z = x+y; 演算 + が、その時点において検証で考慮されるすべての x と y の値でオーバーフローします。
グレー	到達不能コードが強調表示されます。	グレーの [到達不能コード] チェック: if(x>0) {} else {} else 分岐が、その時点において検証で考慮されるすべての x の値で到達不能です。
オレンジ	特定の実行パスでエラーの原因になる可能性がある演算が強調表示されます。 詳細については、PolyspaceCode Prover のオレンジ チェックを参照してください。	オレンジの [オーバーフロー]: z = x+y; 解析で、演算 + がオーバーフローするかどうかを証明できません。 最も一般的な理由は、その時点において検証で考慮される x と y の一部の値だけが演算でオーバーフローすることです。検証で考慮される値の範囲は、演算の変数 x および y のツールヒントを使用して確認できます。
グリーン	すべての実行パスで特定のエラーの原因にならないことが証明された演算が強調表示されます*。	グリーンの [オーバーフロー]: z = x+y; 演算 + が、その時点において検証で考慮されるすべての x と y の値でオーバーフローしません。

* 大半のチェックにおいて、本ソフトウェアでは、最初にランタイム エラーが見つかった時点でその実行パスが終了されます。そのため、演算に明確なエラーがある (レッド) かエラーがない (グリーン) と証明された場合、その証明はコードのその時点でまだ終了していない実行パスに対してのみ有効です。レッド チェックおよびオレンジ チェック以降の Code Prover 解析を参照してください。

その他の結果

ランタイム エラーのチェックに加え、Polyspace Code Prover にはコードに関するその他の結果も表示されます。

結果	目的	アイコン
コーディング ルール違反	事前定義のコーディング ルールまたはカスタム コーディング ルールに対する違反を示します。	事前定義のルールについては 、カスタム ルールについては 。
コード メトリクス	コード複雑度メトリクスを示します。	指定した範囲を超えないメトリクスについては 、範囲を超えるメトリクスについては 。
グローバル変数	グローバル変数宣言を示します。	保護されていない可能性のある共有変数については 、使用されていない非共有変数については

ソース コードの色

Polyspace では、コードは [ソース] ペインに次の配色で表示されます。

• チェックのある行:

  [結果のリスト] ペインのすべてのチェックについて、Polyspace によってコードの該当セクションにチェックの色が割り当てられます。

  • マクロを含む行でマクロが折りたたまれている場合、Polyspace によって行全体が行で最も重大なチェックの色になります。重大度は次の順序で低下します: レッド、グレー、オレンジ、グリーン。

    この到達不能 for ループにはマクロ MAX_SIZE が含まれます。行全体はグレーで色付けされます。

    

    マクロを含む行にチェックがなくマクロが折りたたまれている場合は、Polyspace によって行に黒の下線が付けられます。

  • 他のすべての行では、Polyspace によってチェックに関連付けられているキーワードまたは識別子にのみ色が付けられます。

    この割り当てには 3 つのチェックがあります。i と used_global は初期化されますが、配列 tab は範囲外からアクセスできます。[ 演算子はこの問題を示すためにオレンジで色付けされます。

    

• コーディング ルール違反のある行:

  Polyspace では、[結果のリスト] ペインのすべてのコーディング ルール違反について、該当のキーワードまたは識別子に以下が割り当てられます。

  • コーディング ルールが事前定義のルールの場合は (逆向きの三角形) 記号。使用できる事前定義のルールは、MISRA C™、MISRA™ AC AGC、MISRA C++ または JSF^® C++ です。

    この if ステートメントと || 演算は MISRA ルールに違反しています。

    

  • コーディング ルールがカスタム ルールの場合は 記号。

    この関数名はカスタム命名規則に違反しています。

    

• ツールヒントのある行:

  [ソース] ペインでキーワードまたは識別子に対するツールヒントがある場合、Polyspace では次のようになります。

  • チェックに関連付けられているキーワードまたは識別子には実線の下線が付く。

    この行には、input、%、および used_global にチェックとツールヒントの両方があります。

    

  • チェックに関連付けられていないキーワードまたは識別子には破線の下線が付く。

    この行には for と < にツールヒントがありますが、どちらにもチェックはありません。

    

  • 関数本体、またはループ本体に潜在的なランタイム エラーが含まれる関数呼び出しまたはループ コマンドにはレッドの破線の下線が付く。ツールヒントに、エラーの原因となる関数本体またはループ本体の行が示される。

    この function_with_red の呼び出しはランタイム エラーにつながります。

    

• 関数定義:

  関数が定義されている場合、Polyspace は関数名を青色で表示します。

  

• 条件付きコンパイルにより非アクティブとされた行:

  Polyspace では、条件付きコンパイルにより前処理で除外されたコードに明るいグレーが割り当てられます。こうしたコードはたとえば、分岐用のマクロが定義されていない #ifdef ステートメントなどに現れます。このコードは検証 (または実際の実行時の動作) に影響を与えません。

  

グローバル変数の色

[変数アクセス] ペインには、コードに含まれるグローバル変数とその変数に対する読み取り操作および書き込み操作が表示されます。

たとえば、used_global は 4 回アクセスされているグローバル変数です。内訳は、初期化中に 1 回、関数 function_with_red 内に 1 回、および関数 function_with_grey 内で 2 回です。

配色は以下のようになります。

• 変数の色:

  • オレンジ: 保護されていない共有グローバル変数 (マルチタスキング コードにのみ該当)

  • グリーン保護されている共有グローバル変数 (マルチタスキング コードにのみ該当)

  • ブラック: 使用される非共有グローバル変数

  • グレー使用されない非共有グローバル変数

  グローバル変数を参照してください。

• 操作の色: 到達不能コードで操作が発生する場合はグレー、それ以外の場合はブラック。

  前述の例では、関数 function_with_grey 内の操作は 1 つが到達不能で、もう 1 つは到達可能です。

詳細については、Polyspace デスクトップ ユーザー インターフェイスの [変数アクセス]を参照してください。

参考

トピック

• PolyspaceCode Prover のオレンジ チェック
• レッド チェックおよびオレンジ チェック以降の Code Prover 解析