Polyspace Client for Ada は、Ada83 および Ada95 ソースコードにオーバーフロー、ゼロ除算、範囲外の配列アクセス、その他特定のランタイムエラーが存在しないことを証明します。プログラムの実行、コードのインストルメンテーション、テストケースの作成を必要とせずに、結果を生成します。Polyspace Client for Ada は、形式的手法に基づく抽象解釈技法を使用してコードを検証します。解析結果はソースコード内に表示されます。各コードステートメントは、ランタイムエラーが存在しない、エラーが証明されている、到達不能である、または未証明であることを示すよう色分けされています。Polyspace Client for Ada は、変数および関数の戻り値の範囲情報を表示し、どの変数が指定された範囲制限を超えているかを証明できます。
Polyspace Client for Ada をデスクトップ上で使用し、コンパイルとテストの前にコード解析を実行およびレビューすることができます。
重大なランタイムエラーが存在しないことを証明
Ada83 または Ada95 コードの演算について、ランタイムの正確性をチェックします。ランタイム条件にかかわらず、ランタイムエラーが決して発生しないステートメントを特定します。ランタイムの脆弱性を解析し、得られた所見に関連するイベントトレース、変数値の範囲、呼び出しツリーをサポートします。Polyspace Client for Ada は、他のテスト手段では検出できないエラーを、形式的手法で検出します。コードを実行せずに、可能性のあるすべての入力に対してすべてのコードパスを解析します。
デスクトップでの対話形式の解析
プロジェクトを整理して構成し、ソフトウェア プロジェクトのサブセットに静的コード解析を実行して、ソース コード リポジトリに送信する前にコードを修正します。Polyspace Client for Ada を使用してレポートを生成し、結果を確認して問題を重大度により順位付けします。デバッガーに似たビューを使用して、ランタイムエラーにつながる各ステートメント内をステップバイステップで移動し、複雑なバグの根本原因を見つけます。
ソフトウェア設計とコードの理解度の向上
ソフトウェア内の制御フローおよびデータフローを検証し、変数や演算子に関連する範囲情報を確認します。
ソフトウェアのパフォーマンスの最適化
ゼロ除算などについて安全かつセキュアな演算を特定することで、防衛的コードを削除します。メモリフットプリントを縮小するために、あらゆる実行パスを介しても到達できないコード分岐と、ロジックおよびプログラム構造のエラーを検出し、それらを削除します。
グローバル変数の使用の解析
タスクやスレッドで共有される変数など、グローバル変数の読み取り/書き込み操作のデバッグに費やす時間を短縮します。同時アクセスグラフを使用して、データレースにつながる制御フローとデータフローを理解します。コードを最適化するために、使用していないグローバル変数を特定します。
静的アプリケーション セキュリティ テスト
メモリアクセス、バッファ オーバーフロー、数値オーバーフローなどの潜在的な脆弱性をもつ Ada ステートメントを徹底的に強調することで、アプリケーションに重大なセキュリティ脆弱性がないことを証明します。20 種類の CWE 脆弱性ルールをサポートします。Polyspace Client for Ada からの解析結果を活用し、ファズテストを補完または置き換えて、代わりに脆弱性が特定された演算に焦点を当てます。
ロバスト性テストおよび機能テストの改善および補完
Polyspace Client for Ada を使用して、ゼロ除算やオーバーフローなどが検出され、安全でないことが証明されたステートメントのテストに焦点を当てることにより、ロバスト性テストを改善します。Polyspace Client for Ada の結果を使用して、制御フローおよびデータフロー解析、関数パラメーターとグローバル変数の計算範囲を活用し、境界テストと分割テストを作成および管理します。
製品リソース:
Polyspace 製品ファミリ
Polyspace 製品は、 開発ライフサイクル全体でソフトウェア品質をテストおよび監視することにより、重要なコードを安全かつセキュアにします。
Polyspace Access
コーディングの欠陥の特定、静的解析結果のレビュー、ソフトウェア品質メトリクスの監視
Polyspace Code Prover Server
ソフトウェアにランタイムエラーが存在しないことを証明
Polyspace Bug Finder
静的解析を使用したソフトウェアのバグの特定
Polyspace Test
組み込みシステムにおける C および C++ コードのテストを開発、管理、実行
Polyspace Bug Finder Server
サーバー コンピューターで実行する静的解析によりソフトウェアの欠陥を特定
Polyspace Client for Ada
ソースコードにランタイムエラーが存在しないことを証明
Polyspace Code Prover
ソフトウェアにランタイムエラーが存在しないことを証明
Polyspace Server for Ada
コンピューター クラスターでコード検証を実行し、メトリクスを公開