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