Code Prover の結果とソース コードの色
このトピックでは、Polyspace® Code Prover™ 解析の結果表示に使用されるさまざまな色について説明します。
結果の色
Polyspace では、さまざまな結果が特定のアイコンと色で [結果のリスト] ペインと [結果の詳細] ペインに表示されます。
実行時チェック
Polyspace Code Prover は、コードの各演算について特定のランタイム エラーがないかどうかをチェックします。すべてまたは一部の実行パスにおけるランタイム エラーの有無が証明されているかどうかに応じて、演算が色分けされます。
| チェックの色 | 目的 | 例 | アイコン |
|---|---|---|---|
レッド | 演算がすべての実行パスで特定のエラーの原因になることが証明されます。 Polyspace Code Prover 検証では、言語の規格を基準にしてエラーを判定します。一部のエラーは特定のコンパイル環境では許容されますが、言語の規格に違反します。一部の環境依存動作を許可するには、適切な解析オプションを使用します。詳細については、構成を参照してください。 | レッドの [オーバーフロー] チェック: z = x + y;
演算 |  |
| グレー | コードは到達不能です。 | グレーの [到達不能コード] チェック: if(x > 0)
{}
else
{}検証で考慮されるすべての |  |
| オレンジ | 演算が特定の実行パスでエラーの原因になる可能性があります。 詳細については、PolyspaceCode Prover のオレンジ チェックを参照してください。 | オレンジの [オーバーフロー] チェック: z = x + y;
検証では、演算 最も一般的な理由は、検証で考慮される |  |
| ダーク オレンジ | 演算が特定の実行パスでのみ特定のエラーの原因になることが証明されます。 ダーク オレンジ チェックは、オプション ダーク オレンジ チェックは、コンテキストによっては明確なランタイム エラーを含んでいる可能性があるため、最初に確認すべきタイプのオレンジ チェックです。ダーク オレンジ チェックは、[レビュー] ツールストリップの [スポットライト フィルター] セクションで [重要なチェック] フィルターを使用すると、[結果のリスト] に表示されます。 | ダーク オレンジの [ゼロ除算] チェック: void func(int arg) {
int loc_var = 0;
loc_var = 1/arg;
}
void main(void) {
int num = 1;
func(num + 10);
func(num - 1);
}
|  |
| グリーン | 演算がすべての実行パスで特定のエラーの原因にならないことが証明されます。 | グリーンの [オーバーフロー] チェック: z = 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ステートメントなどに現れます。このコードは検証 (または実際の実行時の動作) に影響を与えません。
グローバル変数の色
[グローバル変数の使用] ペインにはグローバル変数およびローカルの静的変数が表示されます。このペインには、各グローバル変数ごとにこの変数に対して読み取り/書き込みアクセスを実行するすべての関数およびタスクが一覧で表示され、これらの属性値である値、読み取り/書き込みアクセス、共有での使用状況なども表示されます。
[結果の詳細] ペインの 
アイコンを使用するか、または [ビュー] 、 [グローバル変数の使用] に移動して、[グローバル変数の使用] ペインを開きます。あるいは、[ソース コード] ペインでグローバル変数を選択し、右クリックして [[グローバル変数の使用] を表示] を選択することでも、[グローバル変数の使用] ペインを開くことができます。
配色は以下のようになります。
変数の色:
黒: グローバル変数。
オレンジ: タスク間で共有されている、同時アクセスに対して保護されていないグローバル変数。
グリーン: タスク間で共有されている、同時アクセスに対して保護されたグローバル変数。
グレー: 宣言されているが、到達可能コードで使用されないグローバル変数。
グローバル変数を参照してください。
操作の色: タスクで特定の操作がグローバル変数で実行されても、当該操作が到達不能コードにある場合、そのタスクの色はグレーになります。
詳細については、Global Variables Usage in Polyspace Platform User Interfaceを参照してください。
