Exponenta Banner

Энергозависимые переменные в Polyspace Bug Finder

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

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

    • Если вы объявляете глобальную энергозависимую переменную как const, Polyspace использует значение инициализации переменной или области значений инициализации, если вы используете PERMANENT Init Mode, чтобы ограничить область значений переменной внешне. Polyspace использует значение инициализации или область значений для каждого чтения переменной. Смотрите Внешние Ограничения для Анализа 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 обнаруживает дефект Integer division by zero для volatile_var поскольку это инициализируется, чтобы обнулить. Polyspace обнаруживает Integer division by zero для volatile_var_drs потому что это внешне ограничивается к области значений [-5.. 5]. Все чтения volatile_var_10 не вызовите дефект.

    • Для non-const глобальные энергозависимые переменные, Polyspace игнорирует значение инициализации переменной, и затем считает вход неизвестным для каждого чтения переменной. Если вы используете PERMANENT Init Mode, чтобы ограничить область значений переменной внешне, Polyspace использует эту область значений для каждого чтения переменной. Смотрите Внешние Ограничения для Анализа 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 обнаруживает дефект Integer division by zero для 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 обнаруживает дополнительные дефекты Integer division by zero на линиях, помеченных комментарием // No defect, включая для локального энергозависимого переменного примера.

Смотрите также

|

Документация Polyspace Bug Finder

Поддержка