入力およびスタブ

グローバル変数と関数の範囲の指定

ローカルの前提条件を指定するには、入力およびスタブのオプションを使用します。たとえば、外部ソースからの変数の範囲を制限できます。また、解析精度が低い一部の関数をスタブ化してより高い精度で解析することも可能です。前提条件により、レビューのフォーカスを絞り込んで、結果をより意義のあるものにすることができます。"すべての" ファイルと関数における特定のコードの構成要素に適用するグローバルな前提条件については、検証の前提条件オプションを使用します。

Polyspace オプション

すべて展開する

入力

`制約の設定 (-data-range-specifications)`	グローバル変数、関数の入力およびスタブ関数の戻り値の制約
`グローバル変数の既定の初期化を無視する (-no-def-init-glob)`	グローバル変数がコード内で明示的に初期化されていない場合、未初期化と見なす

スタブ

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

Polyspace マクロ

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

トピック

Polyspace 解析オプションの指定
Polyspace^® ユーザーインターフェイス、他の IDE、またはスクリプトで Polyspace 解析オプションを設定する。
Polyspace 解析の外的制約の指定

解析精度を上げるために変数の範囲とポインターの指定を制限する。
Polyspace 解析の外的制約

グローバル変数、関数の入力、およびスタブ関数に適用できる制約を確認する。
- Polyspace 解析制約の XML ファイル形式
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.
C コード検証用のコンテキストを設定する
検証の既定の仮定を絞り込むために提供できる外部コンテキストについて学ぶ。
C++ コード検証用のコンテキストを設定する
検証の既定の仮定を絞り込むために提供できる外部コンテキストについて学ぶ。
手動スタブと手動の main() 関数を使用した Polyspace 解析の変数範囲の制約
独自のスタブと main() を使用した Polyspace Code Prover™ 解析の精度を高める。