Выполните один или несколько из этих шагов до тех пор, пока не будет определено исправление для проверки недопустимых операций смены. Существует несколько способов исправления чека. Описание проверки и примеры кода см. в разделе Invalid shift operations.
Иногда, особенно для оранжевой проверки, можно определить, что проверка представляет собой не реальную ошибку, а предположение Polyspace ®, которое не соответствует вашему коду. Если для смягчения предположения можно использовать опцию анализа, повторно запустите проверку с помощью этой опции. В противном случае в результат или код можно добавить комментарий и обоснование.
Общий рабочий процесс, применяемый ко всем проверкам, см. в разделе Интерпретация результатов проверки кода в пользовательском интерфейсе Polyspace Desktop.
Установите красный или оранжевый флажок Недопустимые операции смены. Получите следующую информацию на панели Сведения о результате (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 (Polyspace Constraint Specification), если у вас нет определения getShiftAmount. Дополнительные сведения см. в разделе Допущения о упорных функциях.
Если левый операнд операции левого сдвига может быть отрицательным, отслеживайте поток данных для переменной левого операнда. Определите подходящую точку, в которой можно ограничить переменную левого операнда.
В следующем примере выполните трассировку потока данных для shiftAmount.
void func(int shiftAmount) {
int val = getVal();
int res = val << shiftAmount;
}getVal возвращает полный диапазон значений.Возможное исправление:
Выполнять смену только в том случае, если val является положительным.
Ограничение возвращаемого значения getVal, в теле getVal или через интерфейс спецификации ограничений Polyspace (Polyspace Constraint Specification), если у вас нет определения getVal. Дополнительные сведения см. в разделе Допущения о упорных функциях.
Если необходимо разрешить операцию в Polyspace, используйте опцию анализа Разрешить отрицательный операнд для левых смен. Посмотрите Allow negative operand for left shifts (-allow-negative-operand-in-shift).
Чтобы отследить поток данных, выберите проверку и запишите информацию на панели Сведения о результате (Result Details).
Если на панели Сведения о результате (Result Details) отображается последовательность инструкций, которые приводят к проверке, выберите каждую инструкцию.
Если на панели Сведения о результате (Result Details) отображается номер строки вероятной причины проверки, щелкните правой кнопкой мыши панель Источник (Source). Выберите «Перейти к строке».
В противном случае:
Найдите предыдущую операцию записи для переменной, которую требуется отследить.
При предыдущей операции записи определите новую переменную для обратной трассировки.
Установите курсор на переменные, участвующие в операции записи, чтобы увидеть их значения. Значения помогают выбрать переменную для трассировки.
Найдите предыдущую операцию записи для новой переменной. Таким образом можно продолжить трассировку до тех пор, пока не будет определена точка для задания ограничения.
В зависимости от переменной используйте следующие сочетания клавиш навигации для поиска предыдущих экземпляров. В интерфейсе пользователя Polyspace можно выполнить только следующие действия.
| Переменная | Поиск предыдущих экземпляров переменной |
|---|---|
Локальная переменная | Используйте один из следующих методов.
|
Глобальная переменная Щелкните правой кнопкой мыши переменную. Если отображается опция Показать в представлении доступа к переменной, переменная является глобальной переменной. |
|
Возвращаемое значение функции
ret=func(); |
|
Можно также определить, связаны ли переменные в какой-либо операции с какой-либо предыдущей операцией. См. раздел Поиск связей между переменными в коде.
Найдите общие причины проверки недопустимых операций смены.
Проверьте, указан ли нужный тип целевого процессора. Целевой тип процессора определяет количество битов, разрешенных для определенного типа переменной.
Чтобы определить допустимое количество битов:
Перейдите к определению переменной. Обратите внимание на тип переменной.
Щелкните правой кнопкой мыши переменную и выберите «Перейти к определению», если опция существует.
См. количество битов, разрешенных для данного типа.
В конфигурации, используемой для результатов, выберите узел Target & Compiler. Нажмите кнопку Edit рядом со списком Target processor type.
Для левых смен с отрицательным операндом см., если вы намереваетесь выполнить правую смену.
Проверьте, можно ли отследить оранжевый чек по предположению Polyspace, которое встречается ранее в коде. Если предположение не соответствует действительности в вашем случае, добавьте комментарий или обоснование в результат или код. См. раздел Результаты анализа пространства адресов с помощью исправлений ошибок или обоснований.
Например, можно получить переменную из неопределенной функции и выполнить для нее сдвиг влево. Затем:
Polyspace предполагает, что функция может возвращать отрицательное значение.
Операция сдвига влево может выполняться при отрицательном значении, и поэтому операция проверяется оранжевым цветом.
Если известно, что функция возвращает положительное значение, добавьте комментарий и обоснование, описывающие, почему код не был изменен.
Дополнительные сведения см. в разделе Допущения анализа проверки кода.
