除算での負方向への丸め (-div-round-down)
負の数値の除算の商またはモジュラスの切り上げではなく切り捨て
説明
負の数値の除算の商またはモジュラスを切り上げるか、切り捨てるかを指定します。
メモ
a = (a / b) * b + a % b は常に真です。
オプションの設定
以下のいずれかの方法を使用してオプションを設定します。
Polyspace® ユーザー インターフェイス (デスクトップ製品のみ): プロジェクト構成で [ターゲットおよびコンパイラ] ノードを選択してから、このオプションを選択します。
Polyspace Platform ユーザー インターフェイス (デスクトップ製品のみ):
負の整数除算結果の負方向への丸めを参照してください。コマンド ラインとオプション ファイル: オプション
-div-round-downを使用します。コマンド ライン情報を参照してください。
このオプションを使用する理由
このオプションは、コンパイラをエミュレートするために使用します。
このオプションに関連するのは、C90 規格 (ISO/IEC 9899:1990) に従うコンパイラのみです。この規格では、"/ または % のいずれかのオペランドが負の場合、/ 演算子の結果が代数的商以下の最大の整数になるのか商以上の最小の整数になるのかは処理系定義で決まり、% 演算子の符号も同様である" と規定されています。この規格では、コンパイラが独自の実装を選択できます。
C99 規格 (ISO/IEC 9899:1999) に従うコンパイラには、このオプションは不要です。この規格は、除算をゼロ方向へ丸めるようにします (セクション 6.5.5)。
設定
オン/または%のオペランドが負の場合、"/" 演算子の結果は代数的商以下の最大の整数となります。%演算子の結果は、a % b = a - (a / b) * bから導かれます。例:
assert(-5/3 == -2 && -5%3 == 1);は true です。
オフ (既定の設定)/または%のオペランドが負の場合、/演算子の結果は代数的商以上の最小の整数となります。%演算子の結果は、a % b = a - (a / b) * bから導かれます。この動作はゼロ方向への丸めともいいます。
例:
assert(-5/3 == -1 && -5%3 == -2);は true です。
コマンド ライン情報
パラメーター: -div-round-down |
| 既定値: オフ |
例 (Bug Finder): polyspace-bug-finder -div-round-down |
例 (Code Prover): polyspace-code-prover -div-round-down |
例 (Bug Finder Server): polyspace-bug-finder-server -div-round-down |
例 (Code Prover Server): polyspace-code-prover-server -div-round-down |