コード制約の構成

グローバル変数、関数の入力、およびスタブ関数などのコードの要素を制約する

Polyspace^® は、変数の範囲やポインターに許容されるバッファーサイズなどの要素について仮定を行います。これらの要素に制約を適用して、関連性のないコードパスを解析から除外し、結果の正確性を向上させることができます。

Polyspace オプション

制約の設定 (-data-range-specifications) グローバル変数、関数の入力およびスタブ関数の戻り値の制約

`スタブを生成する関数 (-functions-to-stub)`	解析時にスタブ化する関数の指定
`Embedded Coder ルックアップテーブルのスタブを生成 (-stub-embedded-coder-lookup-table-functions)`	自動生成されルックアップテーブルを使用する関数のスタブ化と精度の高いモデル化
`使用するライブラリ (-library)`	プログラムで使用するライブラリの指定

unchecked_assert Polyspace 製品での静的解析で変数範囲を制約する

Polyspace Code Prover でのオレンジチェックの削減
検証精度を高めるために、符号化設計を改善したり、検証オプションを調整する。
Polyspace 解析の外的制約の指定

解析精度を上げるために変数の範囲とポインターの指定を制限する。
- Polyspace 解析のグローバル変数範囲の制約
- Polyspace 解析の関数入力の制約
Test Functions and Constrain Polyspace Code Prover Analysis for Ranges of Inputs and Outputs (Polyspace Test)
Test functions over one or more ranges of input and verify if the output is within a valid range using range specification macros. Run static analysis on the function and associated tests using the specified ranges as external constraint.
手動スタブと手動の main() 関数を使用した Polyspace 解析の変数範囲の制約
独自のスタブと main() を使用した Polyspace Code Prover™ 解析の精度を高める。

スタブ関数に関する Code Prover の仮定
検証では、未定義の関数、またはスタブ化することを選択した関数がスタブ化され、その引数と戻り値については特定の仮定が行われる。