-allow-negative-operand-in-shift)Позвольте операции сдвига влево на отрицательном числе
Эта опция влияет на анализ Code Prover только.
Укажите, что верификация должна позволить операции сдвига влево на отрицательном числе.
Пользовательский интерфейс (только десктопные решения): В вашей настройке проекта опция находится на узле Check Behavior.
Командная строка и файл опций: Используйте опцию -allow-negative-operand-in-shift. Смотрите информацию о командной строке.
Согласно стандарту C99 (секунда 6.5.7), результат операции сдвига влево на отрицательном числе не определен. В соответствии со стандартом, верификация производит красную проверку на сдвигах влево отрицательных чисел.
Если ваш компилятор имеет четко определенное поведение для сдвигов влево отрицательных чисел, установите эту опцию. Обратите внимание на то, что разрешение сдвигов влево отрицательных чисел может уменьшать мобильность кросс-компилятора вашего кода.
OnВерификация позволяет операции сдвига на отрицательном числе, например, -2 << 2.
От (значения по умолчанию)Если операция сдвига выполняется на отрицательном числе, верификация генерирует ошибку.
Параметр: -allow-negative-operand-in-shift |
| Значение по умолчанию: Off |
Пример (Code Prover):
Polyspace Code Prover - источники |
Пример (Сервер Code Prover):
сервер программы автоматического доказательства полипробела кода - источники |