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

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 をビルド システムに統合すると、自動化された検証を実行することができます。

Code Prover の全ドキュメンテーション

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

  • 解析の設定。

  • 検証結果のレビューとレポートの生成。

解析オプション (Polyspace Code Prover)

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

  • ターゲットおよびコンパイラ オプション。

  • 検証の前提条件に関連するオプション。

検証結果 (Polyspace Code Prover)

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

  • 実行時チェック。

  • グローバル変数の使用。

リリース ノート (Polyspace Code Prover)

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