Polyspace デスクトップ ユーザー インターフェイスでの [ダッシュボード]
このトピックでは、Polyspace® デスクトップ ユーザー インターフェイスに注目します。Polyspace Access™ Web インターフェイスでの同等のペインについては、Polyspace Access Web インターフェイスのダッシュボード (Polyspace Access)を参照してください。
Polyspace ユーザー インターフェイスの [ダッシュボード] ペインには、検証結果に関する統計がグラフ形式で表示されます。
このタブでは、次の 4 つのグラフとチャートを表示できます。
検証でカバーされたコード
この列グラフには次の項目が表示されます。
ランタイム エラーをチェックされたファイル (検証済み) の割合。この割合は、[ファイル] 列に表示されます。
検証済みファイル内でランタイム エラーをチェックされた関数 (検証済み) の割合。この割合は、[関数] 列に表示されます。
検証済みの関数内でランタイム エラーをチェックされた基本操作の割合。この割合は、[コード操作] 列に表示されます。
棒グラフをクリックし、[到達不能関数] ウィンドウを開きます。
このウィンドウには次の項目が表示されます。
Number of unreachable functions/Total number of functions到達不能な関数のリストと、それらの関数が定義されているファイルおよび行番号。関数を選択すると、関数定義が [ソース] ペインに表示されます。
低いカバレッジは、早期のレッド チェックまたは欠落している関数の呼び出しを示している可能性があります。以下のコードについて考えます。
void coverage_eg(void)
{
int x;
x = 1 / x;
x = x + 1;
propagate();
}
x の読み取り操作に対する [未初期化ローカル変数] レッド チェックが 1 つだけ生成されます (5 行目を参照)。次の基本操作のチェックは表示されません。
除算に対する [ゼロ除算] チェック。
除算結果に対する [オーバーフロー] チェック。
加算結果に対する [オーバーフロー] チェック。
xが演算x=x+1で読み取られるときの [未初期化ローカル変数] チェック。
コードに対する 5 つの操作チェックのうちの 1 つしか表示されないため、カバーされる基本操作の割合は 1/5 つまり 20% です。ソフトウェアでは、到達不能関数 propagate() 内のチェックは考慮されません。詳細については、コードがチェックされない理由を参照してください。
チェックの分布
この円グラフには、各色のチェックの数が表示されます。チェックの色については、Code Prover の結果とソース コードの色を参照してください。
この円グラフを使用すると、次の項目の推定値を取得できます。
レビューするチェックの数
検証の選択性 (オレンジでないチェックの割合)
特定の検証オプションを指定して、オレンジ チェックの数を減らすことができます。Polyspace Code Prover でのオレンジ チェックの削減を参照してください。
上位 5 個のオレンジ ソース
オレンジ ソースは、オレンジ チェックにつながる変数または関数です。この棒グラフには、チェックの数に最も影響する 5 つのオレンジ ソースが表示されます。
オレンジ ソースによって、Code Prover で複数のオレンジ チェックが生じる可能性があります。このグラフのオレンジ ソースをクリックすると、[結果のリスト] ペインにはそのソースが原因で生じるオレンジ チェックのみが表示されます。
たとえば、以下のコードでは、未知の値 input によってオーバーフローおよびゼロ除算が発生する可能性があります。変数 input は、2 つのオレンジ チェックの原因となるオレンジ ソースです。
void func (int input) {
int val1;
double val2;
val1 = input++;
val2 = 1.0/input;
}各バーは 1 つのオレンジ ソースを表します。バーは影響を受けるチェックの数の順番に並べられます。バーの高さは、対応するオレンジ ソースの影響を受けるチェックの数を示します。バーの上にカーソルを置くとツールヒントが表示され、ソース名とこのソースの影響を受けるチェックの数を示します。
このグラフを使用すると、次の操作ができます。
チェック数に最も影響を与える 5 つのソースを表示します。対応するオレンジ ソースの詳細をさらに表示するには、[オレンジ ソース] ペインで列を選択します。
オレンジ チェックの結果に優先順位を付けます。多数のオレンジ チェックに影響を与えるソースがある場合、可能であればオレンジ チェックの体系的なレビューを開始する前にそれらのソースに対処します。Code Prover 解析結果からの制約テンプレートの作成を参照してください。
その他のダッシュボード機能
また、このペインから次のアクションを実行できます。
[結果のリスト] ペインの結果をフィルターします。
[ダッシュボード] ペインのグラフをクリックすると、グラフィカル要素によって示されている結果のみを表示するように結果のリストを絞り込めます。たとえば、チェックの分布を示す円グラフのセクションの 1 つをクリックすると、特定の色のチェックのみが表示されます。結果をフィルターするすべての方法については、Polyspace デスクトップ ユーザー インターフェイスでの結果のフィルター処理とグループ化を参照してください。
この結果を取得するために使用された構成を表示します。
[ダッシュボード] ペインで [構成] リンクをクリックすると、構成の読み取り専用フォームが開きます。[構成] ペインのオプションについての詳細は、すべての Polyspace Code Prover 解析オプションのリストを参照してください。
解析中に到達しない関数に関する情報を表示します。
[ダッシュボード] ペインの [到達不能関数] リンクをクリックすると、解析中に検証されなかった関数のリストが表示されます。関数が検証されなかった理由の詳細については、コードがチェックされない理由を参照してください。
結果の背後にある解析の前提条件を表示します。
[ダッシュボード] ペインの [解析の前提条件] リンクをクリックすると、解析中に使用された前提条件のリストが表示されます。[解析の前提条件] ペインに表示される前提条件のほとんどは、解析オプションを使用して変更できます (このペインにもそのことが表示されます)。その他の解析の前提条件を見るには、Code Prover 解析の前提条件を参照してください。
コードのマルチタスキング構成のモデリングを表示します。
[ダッシュボード] ペインの [同時実行モデリング] リンクをクリックすると、プログラムへのすべてのエントリ ポイントが表示されます。[同時実行モデリング] ペインの説明については、同時実行モデリングを参照してください。
