Exponenta Banner

Волатильные переменные в Polyspace Bug Finder

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

  • Глобальные переменные летучести

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

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

      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 не вызывайте дефекта.

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

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

      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

Поддержка