Выполните один или несколько из этих шагов, пока вы не определите фиксацию для проверки Invalid shift operations. Существует несколько способов зафиксировать проверку. Для описания проверки и примеров кода, смотрите Invalid shift operations.
Иногда, специально для оранжевой проверки, можно решить, что проверка не представляет действительную ошибку, но предположение Polyspace®, которое не верно для кода. Если можно использовать аналитическую опцию, чтобы ослабить предположение, повторно выполнить верификацию с помощью той опции. В противном случае можно добавить комментарий и выравнивание в результате или коде.
Для общего рабочего процесса, который применяется ко всем проверкам, смотрите, Интерпретируют Результаты Polyspace Code Prover.
Выберите красную или оранжевую проверку Invalid shift operations. Получите следующую информацию из панели Result Details:
Причина проверки, являющейся красным или оранжевым. Возможные причины:
Сумма сдвига может быть внешними позволенными границами.
Программное обеспечение также утверждает позволенную область значений для суммы сдвига.
Оставленный операнд сдвига влево может быть отрицательным.
В примере ниже, происходит красная ошибка, потому что сумма сдвига является внешними позволенными границами. Позволенная область значений для суммы сдвига от 0 до 31.
Возможная фиксация: Чтобы избежать красной или оранжевой проверки, выполните операцию сдвига, только если сумма сдвига в границах.
if(shiftAmount < (sizeof(int) * 8)) /* Perform the shift */ else /* Error handling */
Вероятная первопричина для проверки, если программное обеспечение предоставляет эту информацию.
В предыдущем примере программное обеспечение идентифицирует заблокированную функцию, getVal как вероятная причина.
Возможная фиксация: Чтобы избежать оранжевой проверки, ограничьте возвращаемое значение getVal. Например, укажите, что getVal возвращает значения в определенной области значений, например, 0..10. Для получения дополнительной информации смотрите Заблокированные Функции.
Если сумма сдвига является внешними границами, проследите поток данных для переменной сдвига. Идентифицируйте подходящую точку, где можно ограничить переменную сдвига.
В следующем примере проследите поток данных для shiftAmount.
void func(int val) {
int shiftAmount = getShiftAmount();
int res = val >> shiftAmount;
}getShiftAmount возвращает полный диапазон значений.Возможная фиксация:
Выполните операцию сдвига, только если shiftAmount между 0 и (sizeof(int))*8 - 1.
Ограничьте возвращаемое значение getShiftAmount в теле getShiftAmount или через интерфейс Polyspace Constraint Specification, если у вас нет определения getShiftAmount. Для получения дополнительной информации смотрите Заблокированные Функции.
Если левый операнд операции сдвига влево может быть отрицательным, проследите поток данных для левой переменной операнда. Идентифицируйте подходящую точку, где можно ограничить левую переменную операнда.
В следующем примере проследите поток данных для shiftAmount.
void func(int shiftAmount) {
int val = getVal();
int res = val << shiftAmount;
}getVal возвращает полный диапазон значений.Возможная фиксация:
Выполните операцию сдвига, только если val положителен.
Ограничьте возвращаемое значение getVal в теле getVal или через интерфейс Polyspace Constraint Specification, если у вас нет определения getVal. Для получения дополнительной информации смотрите Заблокированные Функции.
Если вы хотите, чтобы Polyspace позволил операцию, используйте аналитическую опцию Allow negative operand for left shifts. Смотрите Allow negative operand for left shifts (-allow-negative-operand-in-shift).
Чтобы проследить поток данных, выберите проверку и отметьте информацию о панели Result Details.
Если панель Result Details показывает последовательность инструкций, которые приводят к проверке, выбирают каждую инструкцию.
Если панель Result Details показывает номер строки вероятной причины для проверки, щелкните правой кнопкой по панели Source. Выберите Go To Line.
В противном случае:
Найдите предыдущую операцию записи на переменной, которую вы хотите проследить.
При предыдущей операции записи идентифицируйте новую переменную, чтобы проследить.
Установите свой курсор на переменные, вовлеченные в операцию записи, чтобы видеть их значения. Значения помогают вам решить который переменная проследить.
Найдите предыдущую операцию записи на новой переменной. Продолжите прослеживать таким образом, пока вы не идентифицируете точку, чтобы задать ваше ограничение.
В зависимости от переменной используйте следующие ярлыки навигации, чтобы найти предыдущие экземпляры. Можно выполнить следующие шаги в пользовательском интерфейсе Polyspace только.
| Переменная | Как найти предыдущие экземпляры переменной |
|---|---|
Локальная переменная | Используйте один из следующих методов:
|
Глобальная переменная Щелкните правой кнопкой по переменной. Если опция, Show In Variable Access View появляется, переменная, является глобальной переменной. |
|
Функциональное возвращаемое значение
ret=func(); |
|
Можно также определить, связаны ли переменные в какой-либо операции от некоторой предыдущей операции. Смотрите Находят Отношения Между Переменными в Коде.
Ищите частые причины проверки Invalid Shift Operations.
Смотрите, задали ли вы правильный тип целевого процессора. Тип целевого процессора решает, что количество битов допускало определенный тип переменной.
Определить количество позволенных битов:
Перейдите к определению переменной. Отметьте тип переменной.
Щелкните правой кнопкой по переменной и выберите Go To Definition, если опция существует.
Смотрите, что количество битов допускало тип.
В настройке, используемой для ваших результатов, выберите узел Target & Compiler. Нажмите кнопку Edit рядом со списком Target processor type.
Для сдвигов влево с отрицательным операндом смотрите, намеревались ли вы выполнить сдвиг вправо вместо этого.
Смотрите, можно ли проследить оранжевую проверку до предположения Polyspace, которое происходит ранее в коде. Если предположение не сохраняется в вашем случае, добавьте комментарий или выравнивание в вашем результате или коде. Смотрите Результаты Polyspace Адреса Через Исправления ошибок или Комментарии.
Например, вы получаете переменную из неопределенной функции и выполняете сдвиг влево на нем. Затем:
Polyspace принимает, что функция может возвратить отрицательное значение.
Операция сдвига влево может произойти на отрицательной величине и поэтому на операции существует оранжевая проверка.
Если вы знаете, что функция возвращает положительное значение, добавьте комментарий и выравнивание, описывающее, почему вы не изменили свой код.
Для получения дополнительной информации смотрите Аналитические Предположения Программы автоматического доказательства Кода.
