このページの内容は最新ではありません。最新版の英語を参照するには、ここをクリックします。

チェック動作

実行時チェック既定の動作の変更

実行時チェックの既定の動作を変更するには、動作のチェックのオプションを使用します。たとえば、既定の [オーバーフロー] チェックでは、符号付き整数による計算のみでオーバーフローが検出されます。このチェックで符号なし整数による計算のオーバーフローも検出しなければならないことを指定できます。

Polyspace オプション

すべて展開する

左シフトで負のオペランドを許可 (-allow-negative-operand-in-shift)負の数値での左シフト演算の許可
符号付き整数のオーバーフロー モード (-signed-integer-overflows)オーバーフローの結果をラップするか切り捨てるかを指定
符号なし整数のオーバーフロー モード (-unsigned-integer-overflows)オーバーフローの結果をラップするか切り捨てるかを指定
未初期化のチェックを無効にする (-disable-initialization-checks)未初期化変数および未初期化ポインターのチェックの無効化
ウォーム リブート後にグローバル変数が初期化されることをチェック (-check-globals-init)グローバル変数が設計された初期化コードで割り当てられた値であることのチェック
スコープ外のスタック ポインター デリファレンスを検出 (-detect-pointer-escape)関数がそれ自体のローカル変数の 1 つを指すポインターを返すケースを検索
フィールド間のポインター演算を有効にする (-allow-ptr-arith-on-struct)構造体フィールドへのポインターの演算で別のフィールドを指すように許可
構造体の不完全または部分的割り当てを許可する (-size-in-bytes)メモリ バッファーが十分でないポインターが構造体を指すことを許可
関数ポインターの許容呼び出し (-permissive-function-pointer)関数ポインターとそれが指す関数の間で型の不一致を許可
呼び出されない関数の検出 (-uncalled-function-checks)main 関数または別のエントリ ポイント関数から直接または間接的に呼び出されない関数の検出
非有限の浮動小数点を検討 (-allow-non-finite-floats)無限大と NaN を組み込んだ解析モードの有効化
無限大 (-check-infinite)結果が無限大になる浮動小数点演算の処理方法の指定
NaN (-check-nan)結果が NaN になる浮動小数点演算の処理方法の指定
非正規検出モード (-check-subnormal)非正規浮動小数点値になる演算の検出
影響の解析を有効化 (-impact-analysis)Check for presence or absence of impact between program elements designated as sources and sinks (R2023b 以降)
ソースとシンクの指定 (-impact-specifications)Specify XML file that identifies program elements as sources and sinks for impact analysis (R2023b 以降)
影響の解析の結果のみを表示 (-impact-analysis-only)Skip regular Code Prover checks for run-time errors and perform impact analysis only (R2023b 以降)
スタック使用量の計算 (-stack-usage)スタック使用量の推定値の計算と表示 (R2022a 以降)

トピック

実行時チェックの既定の動作の変更

影響の解析の設定