符号付き右シフト (-logical-signed-right-shift)

符号付き変数の論理右シフトの符号ビットをどのように扱うかの指定

説明

負の値での右シフト演算に、論理シフトと算術シフトのどちらを使用するかを選択します。

このオプションはコンパイル時の式を変更しません。詳細は、制限を参照してください。

オプションの設定

以下のいずれかの方法を使用してオプションを設定します。

このオプションを使用する理由

C99 規格 (セクション 6.5.7) では、右シフト演算 x1>>x2 について、x1 が符号付きで負の値の場合は、動作が処理系定義になると規定されています。算術シフトと論理シフトの選択は、コンパイラによって異なります。このオプションは、コンパイラをエミュレートするために使用します。

設定

既定値: Arithmetical

Arithmetical

符号ビットは残ります。

(-4) >> 1 = -2
(-7) >> 1 = -4
  7  >> 1 = 3
論理演算

符号ビットは 0 に置換されます。

(-4) >> 1 = (-4U) >> 1 = 2147483646
(-7) >> 1 = (-7U) >> 1 = 2147483644
  7  >> 1 = 3

制限

コンパイル時の式では、この Polyspace オプションは右シフトの標準動作を変更しません。

たとえば、次の右シフト式について考えます。

int arr[ ((-4) >> 20) ];
コンパイラは配列サイズを計算するので、式 (-4) >> 20 はコンパイル時に評価されます。論理演算では、この式は 4095 と等価になります。しかし、算術演算では、結果は -1 となります。符号付き整数の標準の右シフト動作は算術演算であるため、このステートメントではコンパイル エラーが発生します (配列サイズを負にすることはできません)。

コマンド ライン情報

コマンド ラインを使用する場合、算術演算が既定の計算モードです。次のオプションを設定すると、論理演算が実行されます。

パラメーター: -logical-signed-right-shift
既定値: 算術演算の符号付き右シフト
例 (Bug Finder): polyspace-bug-finder -logical-signed-right-shift
例 (Code Prover): polyspace-code-prover -logical-signed-right-shift
例 (Bug Finder Server): polyspace-bug-finder-server -logical-signed-right-shift
例 (Code Prover Server): polyspace-code-prover-server -logical-signed-right-shift

参考

トピック