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

Polyspace® Bug Finder™ と Polyspace Code Prover™ は、それぞれ異なる目的を持つ各種静的解析を実行します。Code Prover は、一連のランタイム エラーがないことを数学的に証明しようとします。Bug Finder はさまざまなコーディング ルール違反とコーディングの欠陥を検出します。

Bug Finder と Code Prover の両方がある場合は、これらの製品をソフトウェア開発ワークフローのさまざまなステップで統合します。次に例を示します。

  • 組織内のすべての開発者が、新しく開発したコードに対して Bug Finder を実行できます。組織全体で標準を維持するために、特定のタイプの欠陥のみを検出する共通の構成を展開できます。

    Code Prover は単体テスト スイートの一部として展開できます。

  • Code Prover をプロジェクトの重要なコンポーネントに対してのみ実行し、Bug Finder をプロジェクト全体に対して実行することができます。

  • Code Prover を単体テスト レベルでコードのモジュールに対して実行し、Bug Finder をモジュールの統合時に実行することができます。

    単体テストの前に Code Prover を実行できます。Code Prover は、網羅的にコードをチェックし、エラーの有無を証明しようとします。その後、コード全体の単体テストを作成するのではなく、未証明のコードに対してのみテストを作成できます。単体テストの前に Code Prover を使用すると、テスト作業が大幅に削減されます。

ソフトウェア開発ワークフローの性質および使用可能なリソースに応じて、この他にもさまざまな方法で 2 種類の解析を組み込むことができます。開発中またはリモート サーバーで自動テストの一環として、デスクトップで両製品を実行できます。開発に近いほど、バグの解釈や修正が容易になります。両製品を開発プロセスの早期に展開し、頻繁に使用すると、両製品の使用によるメリットが得られます。

Bug Finder と Code Prover の両方を同じコードに対して実行する場合は、2 つの重要な事項を考慮する必要があります。

Code Prover はコンパイルやリンク作成エラーについてより厳格であるため、Code Prover 検証を実行する際は、より多くの既定のオプションを変更しなければならない場合があります。