Exponenta Banner
exponenta event banner

Изменчивые переменные в поисковике ошибок Polyspace

Вы используете volatile ключевое слово, информирующее компилятор о том, что значение переменной может изменяться в любое время без явной операции записи. При выполнении анализа Polyspace ® Bug Finder™ делает следующие предположения относительно изменчивых переменных:

  • Глобальные изменчивые переменные

    • При объявлении глобальной изменчивой переменной как const, Polyspace использует значение инициализации переменной или диапазон инициализации, если используется PERMANENT Чтобы ограничить диапазон переменной внешне, введите режим. Polyspace использует значение инициализации или диапазон для каждого чтения переменной. См. раздел Внешние ограничения для анализа в пространстве.

      Например, в этом коде:

      const volatile volatile_var; // Global variable initialized to 0
const volatile volatile_var_10=10;
const volatile volatile_var_drs=3; // Variable constrained to range [-5 .. 5]

int func(void){
    int i= 10 % volatile_var; // Defect
    int j= 10 % volatile_var_10; // No defect
    int k= 10 % volatile_var_drs; // Defect
    return i+j+k;
}
      Polyspace обнаруживает целое деление на ноль дефекта для volatile_var так как он инициализирован как ноль. Polyspace обнаруживает целочисленное деление на ноль для volatile_var_drs потому что он внешне ограничен диапазоном [-5.. 5]. Все чтения volatile_var_10 не вызвать дефекта.

    • Для не-const глобальные энергозависимые переменные, Polyspace игнорирует значение инициализации переменной, а затем рассматривает вход неизвестным для каждого чтения переменной. Если вы используете PERMANENT Init Mode для ограничения диапазона переменной извне, Polyspace использует этот диапазон для каждого чтения переменной. См. раздел Внешние ограничения для анализа в пространстве.

      Например, в этом коде:

      volatile volatile_var; // Global variable initialized to 0
volatile volatile_var_drs=3; // Variable constrained to range [-5 .. 5]

int func(void){
    int i= 10 % volatile_var; // No defect
    int j= 10 % volatile_var_drs; // Defect
    return i+j;
}

    Polyspace обнаруживает целое деление на ноль дефекта для volatile_var_drs потому что он внешне ограничен диапазоном [-5.. 5]. Все чтения volatile_var не вызвать дефекта.

  • Локальные изменчивые переменные

    Polyspace игнорирует значение инициализации локальных переменных, а затем считает, что входные данные неизвестны для каждого чтения переменной. Например, в этом коде:

    int foo(void){
    volatile var=0;
    return 1/var; // No defect
}
    Polyspace не обнаруживает дефектов. Нельзя использовать внешние ограничения для ограничения диапазона локальных переменных.

За счет возможно более длительного времени выполнения можно выполнить более исчерпывающий анализ, в котором Polyspace рассматривает все значения для каждого чтения изменчивой переменной. Посмотрите Run stricter checks considering all values of system inputs (-checks-using-system-input-values). При использовании этой опции для анализа всех предыдущих примеров кода Polyspace обнаруживает дополнительные целочисленные деления на ноль дефектов в строках, помеченных комментарием // No defect, в том числе для примера локальной изменчивой переменной.

См. также

|

Документация для поиска ошибок Polyspace

Поддержка