Exponenta Banner

Signed right shift (-logical-signed-right-shift)

Задайте, как лечить знаковый бит от логических сдвигов вправо на переменных со знаком

Описание

Выберите между арифметическим и логическим сдвигом для операций сдвига вправо на отрицательных величинах.

Эта опция не изменяет выражения времени компиляции. Для получения дополнительной информации смотрите Ограничение.

Установите опцию

Пользовательский интерфейс (только десктопные решения): В вашей настройке проекта опция находится на узле Target & Compiler.

Командная строка и файл опций: Используйте опцию -logical-signed-right-shift. Смотрите информацию о командной строке.

Почему использование эта опция

Стандарт C99 (секунда 6.5.7) утверждает это для операции x1>>x2 сдвига вправо, если x1 подписывается и имеет отрицательные величины, поведение задано реализацией. Различные компиляторы выбирают между арифметическим и логическим сдвигом. Используйте эту опцию, чтобы эмулировать ваш компилятор.

Настройки

Значение по умолчанию: Arithmetical

Arithmetical

Знаковый бит остается:

(-4) >> 1 = -2
(-7) >> 1 = -4
  7  >> 1 = 3
Logical

0 замен знаковый бит:

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

Ограничение

В выражениях времени компиляции эта опция Polyspace® не изменяет стандартное поведение для сдвигов вправо.

Например, рассмотрите это выражение сдвига вправо:

int arr[ ((-4) >> 20) ];
Компилятор вычисляет размеры массивов, таким образом, выражение (-4) >> 20 оценен во время компиляции. Логически, это выражение эквивалентно 4 095. Однако арифметически результат-1. Этот оператор вызывает ошибку компиляции (массивы не могут иметь отрицательного размера), потому что стандартное поведение сдвига вправо для целых чисел со знаком является арифметикой.

Информация о командной строке

При использовании командной строки арифметика является режимом расчета по умолчанию. Когда эта опция установлена, логический расчет выполняется.

Параметр: -logical-signed-right-shift
Значение по умолчанию: Арифметика подписала сдвиги вправо
Пример (Bug Finder): polyspace-bug-finder -logical-signed-right-shift
Пример (программа автоматического доказательства кода): polyspace-code-prover -logical-signed-right-shift
Пример (сервер Bug Finder): polyspace-bug-finder-server -logical-signed-right-shift
Пример (сервер программы автоматического доказательства кода): polyspace-code-prover-server -logical-signed-right-shift

Смотрите также

Темы

Документация Polyspace Bug Finder

Поддержка