Volatile Variables in Polyspace Bug Finder

You use the volatile keyword to inform the compiler that the value of a variable might change at any time without an explicit write operation. When you run an analysis, Polyspace^® Bug Finder™ makes these assumptions about volatile variables:

• Global volatile variables

  • If you declare a global volatile variable as const, Polyspace uses the initialization value of the variable or the initialization range if you use the PERMANENT Init Mode to constrain the range of the variable externally. Polyspace uses the initialization value or range for every read of the variable. See External Constraints for Polyspace Analysis.

    For instance, in this code:

    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 detects an Integer division by zero defect for volatile_var since it is initialized to zero. Polyspace detects an Integer division by zero for volatile_var_drs because it is externally constrained to the range [-5 .. 5]. All reads of volatile_var_10 cause no defect.

  • For non-const global volatile variables, Polyspace ignores the initialization value of the variable, and then considers the input unknown for each read of the variable. If you use the PERMANENT Init Mode to constrain the range of the variable externally, Polyspace uses this range for every read of the variable. See External Constraints for Polyspace Analysis.

    For instance, in this code:

    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 detects an Integer division by zero defect for volatile_var_drs because it is externally constrained to the range [-5 .. 5]. All reads of volatile_var cause no defect.

• Local volatile variables

  Polyspace ignores the initialization value of local volatile variables, and then considers the input unknown for each read of the variable. For example, in this code:

  int foo(void){
      volatile var=0;
      return 1/var; // No defect
  }

  Polyspace detects no defect. You cannot use external constraints to constrain the range of local variables.

At the cost of a possibly longer runtime, you can perform a more exhaustive analysis where Polyspace considers all values for each read of a volatile variable. See Run stricter checks considering all values of system inputs (-checks-using-system-input-values). When you use this option to analyze all the preceding code examples, Polyspace detects additional Integer division by zero defects on the lines labeled with comment // No defect, including for the local volatile variable example.