Выполните один или несколько из следующих шагов до тех пор, пока вы не определите исправление для проверки Invalid shift operations. Существует несколько способов исправить проверку. Для получения описания примеров проверки и кода смотрите Invalid shift operations.
Иногда, особенно для оранжевого чека, можно определить, что чек представляет не реальную ошибку, а Polyspace® предположение, что не соответствует действительности для вашего кода. Если для ослабления допущения можно использовать опцию анализа, повторите верификацию с помощью этой опции. В противном случае можно добавить комментарий и обоснование в результат или код.
Общий рабочий процесс, который применяется ко всем проверкам, см. в разделе Интерпретация результатов Prover кода в пользовательском интерфейсе рабочего стола Polyspace.
Выберите красный или оранжевый Invalid shift operations проверки. Получите следующую информацию из панели Result Details:
Причина проверки - красный или оранжевый. Возможные причины:
Величина сдвига может быть вне допустимых границ.
Программа также определяет допустимую область значений для величины сдвига.
Левый операнд левого сдвига может быть отрицательным.
В приведенном ниже примере происходит красная ошибка, поскольку величина сдвига находится вне допустимых границ. Допустимая область значений значений сдвига - от 0 до 31.
Возможное исправление: Чтобы избежать проверки красного или оранжевого цвета, выполните операцию сдвига только, если величина сдвига находится в границах.
if(shiftAmount < (sizeof(int) * 8)) /* Perform the shift */ else /* Error handling */
Вероятная первопричина проверки, если программа предоставляет эту информацию.
В предыдущем примере программное обеспечение идентифицирует упорную функцию getVal как вероятная причина.
Возможное исправление: Чтобы избежать оранжевой проверки, ограничьте возврат значение getVal. Для образца задайте, что getVal возвращает значения в определенной области значений, например 0..10. Для получения дополнительной информации смотрите Допущения об упрямых функциях.
Если величина сдвига находится вне границ, проследите поток данных для переменной сдвига. Определите подходящую точку, где можно ограничить переменную shift.
В следующем примере проследите поток данных для 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, которое происходит ранее в коде. Если предположение не имеет значения true в вашем случае, добавьте комментарий или обоснование в свой результат или код. Смотрите Адрес Результаты Polyspace через исправления ошибок или обоснования.
Например, вы получаете переменную из неопределенной функции и выполняете на ней сдвиг влево. Затем:
Polyspace принимает, что функция может вернуть отрицательное значение.
Операция сдвига влево может происходить при отрицательном значении, и поэтому выполняется оранжевая проверка операции.
Если вы знаете, что функция возвращает положительное значение, добавьте комментарий и обоснование, описывающие, почему вы не изменили код.
Для получения дополнительной информации смотрите Допущения анализа Code Prover.
