Polyspace Bug Finder と Code Prover のドキュメンテーション

最新のリリースでは、このページがまだ翻訳されていません。このページの最新版は英語でご覧になれます。

Bug Finder

Polyspace^® Bug Finder™ は、C および C++ 組み込みソフトウェアにおけるランタイムエラー、同時実行の問題、セキュリティの脆弱性などの欠陥を特定します。Polyspace Bug Finder では、セマンティクス解析などの静的解析を使用して、ソフトウェア制御、データフロー、および手続き間の動作を解析します。欠陥を検出して直ちに強調表示することにより、開発プロセスの初期段階でバグを重大度により順位付けし、修正を行うことができます。

Polyspace Bug Finder は、MISRA C^®、MISRA^® C++、JSF^®++、カスタム命名規則などのコーディングルール標準への準拠をチェックします。検出したバグやコードルール違反、および循環的複雑度などのコード品質メトリクスから構成されるレポートを生成します。Polyspace Bug Finder は、Eclipse™ IDE と共に使用してビルドシステムに統合できます。

自動生成されたコードについては、Polyspace の検証結果を Simulink^® モデルおよび dSPACE^® TargetLink^® ブロックまでさかのぼって追跡できます。

Bug Finder の全ドキュメンテーション

すべてのワークフローを確認します。たとえば、以下があります。

解析の設定。
検証結果のレビューとレポートの生成。

解析オプション (PolyspaceBug Finder)

解析前に構成するオプションを確認します。たとえば、以下があります。

ターゲットおよびコンパイラオプション。
調査する欠陥。

検証結果 (Polyspace Bug Finder)

解析から取得する検証結果を確認します。たとえば、以下があります。

欠陥。
コーディングルール。

リリースノート (Polyspace Bug Finder)

各リリースの新機能を確認します。

Code Prover

Polyspace Code Prover™ は安定性の高い静的解析ツールで、C および C++ ソースコード内のオーバーフロー、ゼロ除算、配列の範囲外へのアクセスおよびその他特定のランタイムエラーの有無が証明されます。プログラムの実行、コード計測またはテストケースを必要とすることなく、結果が生成されます。Polyspace Code Prover では、セマンティクスの解析および形式的手法に基づく抽象的な解釈が使用され、ソフトウェアの手続き間のフロー、制御フロー、およびデータフローの動作が検証されます。Polyspace Code Prover は、手書きのコード、生成されたコードまたはその 2 つの組み合わせに対して使用できます。各動作は色分けされ、ランタイムエラーなし、エラーと証明、到達不能、または未証明のいずれかであることが示されます。

Polyspace Code Prover では、変数および関数の戻り値の範囲情報も表示され、指定された範囲限界値を超えた変数を証明できます。検証結果をダッシュボードに公開して品質メトリクスを追跡し、ソフトウェア品質目標に確実に適合することができます。Polyspace Code Prover をビルドシステムに統合すると、自動化された検証を実行することができます。