Позвольте отрицательный операнд для сдвигов влево (-allow-negative-operand-in-shift)

Позвольте операции сдвига влево на отрицательном числе

Описание

Эта опция влияет на анализ Программы автоматического доказательства Кода только.

Укажите, что верификация должна позволить операции сдвига влево на отрицательном числе.

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

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

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

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

Согласно стандарту C99 (секунда 6.5.7), результат операции сдвига влево на отрицательном числе не определен. В соответствии со стандартом, верификация производит красную проверку на сдвигах влево отрицательных чисел.

Если ваш компилятор имеет четко определенное поведение для сдвигов влево отрицательных чисел, установите эту опцию. Обратите внимание на то, что разрешение сдвигов влево отрицательных чисел может уменьшать мобильность кросс-компилятора вашего кода.

Настройки

На

Верификация позволяет операции сдвига на отрицательном числе, например, -2 << 2.

От (значения по умолчанию)

Если операция сдвига выполняется на отрицательном числе, верификация генерирует ошибку.

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

Параметр: -allow-negative-operand-in-shift
Значение по умолчанию: 'off'
Пример (программа автоматического доказательства кода): polyspace-code-prover -sources file_name -allow-negative-operand-in-shift
Пример (сервер программы автоматического доказательства кода): polyspace-code-prover-server -sources file_name -allow-negative-operand-in-shift