-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 - источники |
Пример (Сервер Программы автоматического доказательства Кода):
сервер программы автоматического доказательства полипробела кода - источники |