実行時チェックの構成

Polyspace^® の実行時チェックの動作を変更する

Polyspace によるコードの解析方法およびランタイムエラーのチェック方法を構成します。

Polyspace オプション

`左シフトで負のオペランドを許可 (-allow-negative-operand-in-shift)`	負の数値での左シフト演算の許可
`符号付き整数のオーバーフローモード (-signed-integer-overflows)`	オーバーフローの結果をラップするか切り捨てるかを指定
`符号なし整数のオーバーフローモード (-unsigned-integer-overflows)`	オーバーフローの結果をラップするか切り捨てるかを指定
`-show-similar-overflows`	ラップアラウンドモードでのすべてのオーバーフローの表示

`スコープ外のスタックポインターデリファレンスを検出 (-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)`	非正規浮動小数点値になる演算の検出

-code-behavior-specifications コードの要素 (関数など) への動作の関連付け

-check-parameter-of-stubbed-functions Enable checking pointer parameters of stubbed functions

Code Prover の実行時チェックの変更または無効化

Code Prover の実行時チェックのサブセットを無効にする。
- コード動作仕様を使用して Code Prover の実行時チェックを変更する
バッファーサイズ計算でのオーバーフローの検出
オーバーフローをバッファー使用時に後から検出するのではなく、早い段階でのバッファーサイズの計算中に検出する。