Polyspace Bug Finder と Polyspace Code Prover の違い

Polyspace^® Bug Finder™ と Polyspace Code Prover™ では、静的解析によってランタイムエラーを検出します。この 2 つの製品は同様のユーザーインターフェイスを備えており、解析の基礎となる数学演算が同じである場合もありますが、製品の目的は異なります。

Bug Finder はコードをすばやく解析し、さまざまなタイプの欠陥を検出します (Polyspace as You Code も、Bug Finder と同様に単一ファイル解析を実行します)。Code Prover は、コード内の "すべて" の演算において一連の潜在的なランタイムエラーをチェックし、すべての実行パスにエラーがないことを証明しようとします。

メモ

Code Prover は、コード内の各演算について、その演算までの間にエラーのない実行パスすべてを考慮します。その演算より前にエラーのある実行パスは、Code Prover によって考慮されません。レッドチェックおよびオレンジチェック以降の Code Prover 解析 (Polyspace Code Prover)を参照してください。

たとえば、コード内の "すべて" の除算について、Code Prover 解析では分母がゼロにならないことを証明しようとします。Bug Finder ではこのような徹底的な検証は実行されません。たとえば、Bug Finder でもゼロ除算エラーはチェックされますが、エラーの原因となりうるすべての演算を検出できない可能性があります。

目的にこのような違いがあるため、この 2 つの製品の設定、解析および結果のレビューには違いがあります。以下の節では、Bug Finder と Code Prover の解析 (検証とも呼ばれる) の主な違いについて説明します。要件に応じて、ソフトウェア開発ライフサイクルの適切な段階で、いずれかまたは両方の種類の解析を組み込むことができます。

Bug Finder と Code Prover の違いの概要

開発プロセスでは Bug Finder と Code Prover の両方を定期的に使用します。製品は、それぞれ機能の一意のセットを提供し、相互に補完します。製品の併用方法に関しては、Polyspace Bug Finder と Polyspace Code Prover の両方を使用したワークフローを参照してください。

次の表は、製品の相互補完の概要を示しています。詳細は、以降のセクションを参照してください。

機能	Bug Finder	Code Prover
チェッカーの数	300 以上の欠陥のチェッカー	重大なランタイムエラーの 30 項目のチェック、およびグローバル変数の使用の 4 項目のチェック
解析の深さ	高速。次に例を示します。高速解析。容易な設定とレビュー。クリーンなコードに対して少ない回数の実行。リアルタイムでの結果。	網羅。次に例を示します。特定のクリティカルエラーに対するすべての演算の型チェック。データフローと制御フローのより厳密な解析
レポート条件	考えられる欠陥	証明済みの調査結果
バグ検出条件	誤検知の削減	偽陰性の排除

Bug Finder における解析の高速化

Bug Finder で解析がどの程度高速化されるかは、アプリケーションのサイズによって異なります。Bug Finder の解析時間は、アプリケーションのサイズと共に線形に増加します。Code Prover の検証時間は、線形よりも速いペースで増加します。

1 つのワークフローとして、Code Prover を実行してモジュールまたはライブラリの特定のエラーに対するロバスト性を解析し、Bug Finder を統合段階で実行するという方法が挙げられます。大規模なコードベースに対する Bug Finder 解析では、完了までの時間がかなり短くなるほか、[宣言の不一致] や [データレース] などの統合の欠陥を検出できます。

Code Prover におけるより徹底的な検証

Code Prover は、以下がないことを証明しようとします。

"すべて" の除算またはモジュラス演算における [ゼロ除算] エラー
"すべて" の配列アクセスにおける [範囲外の配列インデックス] エラー
"すべて" の変数の読み取りにおける [未初期化変数] エラー
オーバーフローする可能性がある "すべて" の演算における [オーバーフロー] エラー

などが挙げられます。

各演算について、次のようになります。

Code Prover ですべての実行パスにエラーがないことを証明できる場合、演算はグリーンで強調表示されます。
Code Prover ですべての実行パスに明確なエラーがあることを証明できる場合、演算はレッドで強調表示されます。
Code Prover でエラーがないことおよび明確なエラーがあることを証明できない場合、演算はオレンジで強調表示されます。このオレンジチェックは、割合は少ないものですが、目視またはテストによって慎重に確認しなければならない演算を示しています。オレンジチェックは多くの場合、脆弱性が隠れていることを示します。たとえば、この演算は現在のコンテキストでは安全でも、他のコンテキストで再利用するとエラーになる可能性があります。
Polyspace ユーザーインターフェイスで提供される情報を使用してチェックを診断できます。Code Prover におけるデータフローと制御フローのより厳密な解析を参照してください。未証明のコードをさらに削減するために、入力範囲を外部で制約するなど、コンテキスト情報を提供することもできます。

Bug Finder は徹底的な解析を目的としていません。できるだけ多くのバグを検出し、誤検知を削減することを目的としています。重要なソフトウェアコンポーネントの場合は、バグ検出ツールを実行するだけでは不十分です。解析で見つかったすべての欠陥を修正しても、コードの実行時にまだエラーが発生する可能性 (誤検知) があるためです。コードに対して Code Prover を実行し、見つかった問題に対処することで、コードの品質はかなり向上するでしょう。Code Prover における偽陰性の排除を参照してください。

Bug Finder におけるより具体的な欠陥タイプ

Code Prover では、各種のランタイムエラーをチェックして、エラーがないことを数学的に証明できます。Bug Finder では、ないことを数学的に証明できるエラーに加えて、その他の欠陥も検出されます。

たとえば、ステートメント if(a=b) は C 言語の規格によると意味的には正しいのですが、多くの場合、意図しない代入を示しています。Bug Finder は、このような意図しない演算を検出します。Code Prover ではこのような意図しない演算は検出されませんが、意図しない演算によってその他のランタイムエラーが発生するかどうかを検出できます。

Bug Finder では検出されるが Code Prover では検出されない欠陥には、適切な手法の欠陥、リソース管理の欠陥、プログラミングの欠陥、セキュリティの欠陥、C++ オブジェクト指向設計の欠陥などがあります。

詳細は、次を参照してください。

欠陥:Bug Finder で検出できる欠陥のリスト。
実行時チェック (Polyspace Code Prover):Code Prover で検出できるランタイムエラーのリスト。

Bug Finder の容易な設定プロセス

コンパイルツールチェーンでコードが正常にビルドされた場合でも、Code Prover 検証のコンパイル段階では失敗する可能性があります。Code Prover の厳密なコンパイルは、特定のランタイムエラーがないことを証明する機能に関連しています。

コンパイラをエミュレートする解析オプションを明示的に使用する場合を除き、Code Prover は ANSI^® C99 規格に厳密に準拠します。
ANSI C99 規格からの逸脱を許容するには、ターゲットおよびコンパイラオプションを使用しなければなりません。ビルドシステムから Polyspace プロジェクトを作成した場合、このオプションは自動的に設定されます。
Code Prover では、一般的なコンパイラで許容できるリンク作成エラーが許容されません。
コンパイラでコンパイルユニット間の関数シグネチャの不一致などのリンク作成エラーが許容されていても、実行時の予期しない動作を回避するには、エラーを修正しなければなりません。

詳細は、コンパイルおよびリンクのエラーのトラブルシューティング (Polyspace Code Prover)を参照してください。

Bug Finder は、特定のコンパイルエラーについてそれほど厳密ではありません。異なるコンパイルユニットの間で関数シグネチャの不一致などのリンク作成エラーがあると、Code Prover 検証は停止する可能性がありますが、Bug Finder 解析は停止しません。したがって、Bug Finder 解析は設定の手間をあまりかけずに実行できます。Bug Finder では、多くの場合、解析の完了後にリンク作成エラーが欠陥として報告されます。

Bug Finder におけるより少ない実行でのクリーンなコードの確保

特定のランタイムエラーがないことを保証するために、Code Prover は、演算においてランタイムエラーを検出すると厳格な規則に準拠します。ランタイムエラーが発生すると、プログラムの状態が不明確になり、Code Prover はそれ以降のコードにエラーがないことを証明できません。したがって、次のように動作します。

明確なエラーがあることを証明し、レッドチェックを表示した場合、Code Prover は同一ブロックにある残りのコードを検証しません。
[オーバーフロー] などのチェックは例外です。このチェックでは解析は続行され、オーバーフローの結果が切り捨てられるかラップされます。
エラーがあることが疑われ、オレンジチェックを表示した場合、Code Prover はエラーを含むパスを対象から除外します。たとえば、Code Prover で演算 1/x において [ゼロ除算] エラーが検出された場合、そのブロックの x に対するそれ以降の演算で x をゼロにすることはできません。
コードブロックが到達不能であることを検出し、グレーチェックを表示した場合、Code Prover はそのブロックのエラーを検出しません。

詳細は、レッドチェックおよびオレンジチェック以降の Code Prover 解析 (Polyspace Code Prover)を参照してください。

したがって、レッドチェックとグレーチェックを修正して検証を再実行すると、より多くの問題が見つかる可能性があります。完全にクリーンなコードを得るには、検証を複数回実行し、そのたびに問題を修正する必要があります。この状況は動的テストと似ています。動的テストでは、コード内の特定のポイントで不具合を修正したら、それ以降のコードで新しい不具合を検出できます。

Bug Finder では、ブロック内で欠陥が検出された後も、そのブロックの解析全体は停止しません。Bug Finder でも、完全にクリーンなコードを得るために解析を複数回実行しなければならない場合があります。ただし、Code Prover よりも少ない実行回数で済みます。

Bug Finder におけるリアルタイムの結果

Bug Finder では、解析の実行中に一部の解析結果が表示されます。解析が終わるまで待たなくても結果をレビューできます。

Code Prover では、結果は検証の終了後にのみ表示されます。Bug Finder では、欠陥が検出されたらその欠陥を表示できます。Code Prover では、すべての実行パスにエラーがないことを証明しなければなりません。したがって、解析中に結果を表示することはできません。

Code Prover におけるデータフローと制御フローのより厳密な解析

Code Prover は、コード内の各演算について以下を提供します。

演算の各変数の値の範囲を示すツールヒント。
ポインターの場合、ツールヒントは、ポインターが指す変数とその変数値を示します。
演算につながる関数の呼び出し順序のグラフ表示。

この範囲情報と呼び出しグラフを使用すると、関数の呼び出し階層内を簡単に移動でき、変数でエラーの原因となる値がどのように取得されるかを把握できます。たとえば、[範囲外の配列インデックス] エラーの場合、インデックス変数にエラーの原因となる値が最初に割り当てられる場所を見つけることができます。

Bug Finder で結果をレビューする際には、欠陥の根本原因を把握するための補足情報も確認できます。たとえば、Bug Finder によって欠陥が検出された場所からその根本原因へのトレースバックがあります。ただし、Code Prover ではより完全な情報を確認できます。コード内のすべての実行パスを把握するのにこの情報が役立つためです。

Code Prover でのデータフロー解析

Code Prover での制御フロー解析

Bug Finder における偽陽性の削減

Bug Finder は、偽陽性をほぼなくすこと、つまり結果を修正する可能性をほぼなくすことを目的としています。既定では、最も意義がありそうな欠陥のみが表示されます。

また、Bug Finder では、欠陥の重大性と偽陽性率に基づいて、欠陥タイプに影響度という属性が割り当てられます。コードで影響度の高い欠陥のみを解析するように選択できます。レビューしない欠陥を有効または無効にすることもできます。

未初期化に関連する特定の Code Prover 欠陥を無効にすることもできます。

Code Prover における偽陰性の排除

Code Prover は徹底的な解析を目的としています。このソフトウェアでは、特定のタイプのエラーをトリガーする可能性があるすべての演算がチェックされます。コード演算がグリーンの場合は、その演算がソフトウェアによってチェックされたランタイムエラーの原因となることはありません。このように、このソフトウェアは偽陰性をなくすことを目的としています。

Code Prover の結果は、解析オプションによって Code Prover に指定したものと同じ条件下でコードを実行した場合にのみ有効です。

エラーがないことを証明できない場合、疑わしい演算はレッドまたはオレンジで強調表示され、この演算の確認が必要になります。

Bug Finder でのコーディングルールのサポート

Bug Finder では次のような外部のコーディング規約への準拠のチェックがサポートされています。

AUTOSAR C++14。AUTOSAR C++14 ルールを参照してください。
MISRA C:2012。MISRA C:2012 命令およびルールを参照してください。
MISRA C++:2008。MISRA C++:2008 ルールを参照してください。
CERT C。CERT C ルールと推奨事項を参照してください。
CERT C++。CERT C++ ルールを参照してください。

コーディング規約サポートの完全なリストについては、Polyspace でのコーディング規約のサポートを参照してください。

参考

トピック

Polyspace Bug Finder と Polyspace Code Prover の両方を使用したワークフロー (Polyspace Code Prover)