Assumptions About Volatile Variables

The values of volatile variables can change without explicit write operations.

For local volatile variables:

• Polyspace^® assumes that the variable has a full range of values allowed by its type.

• Unless you explicitly initialize the variable, when you read the variable, Polyspace produces an orange Non-initialized local variable check.

In this example, Polyspace assumes that val1 is potentially noninitialized but val2 is initialized. Polyspace considers that the + operation can cause an overflow because it assumes both variables to have all possible values allowed by their data types.

int func (void)
{
    volatile int val1, val2=0;
    return( val1 + val2);
}

For global volatile variables:

• Polyspace assumes that the variable has a full range of values allowed by its type.

  You can constrain the range externally. See Constrain Global Variable Range in the documentation for Polyspace Code Prover™ or Polyspace Code Prover Server™.

• Even if you do not explicitly initialize the variable, when you read the variable, Polyspace produces a green Non-initialized variable check.

If the root cause of an orange check is a local volatile variable, you cannot override the default assumptions and constrain the values of the volatile variables. Try one of the following:

• If the volatile variable represents hardware-supplied data, see if you can use a function call to model this data retrieval. For example, replace volatile int port_A with int port_A = read_location(). You do not have to define the function. Polyspace stubs the undefined functions. You can then specify constraints on the function return values using the option Constraint setup (-data-range-specifications). For more information on analysis options, see the documentation for Polyspace Code Prover or Polyspace Code Prover Server.

• See if you can copy the contents of the volatile variable to a global nonvolatile variable. You can then constrain the global variable values throughout your code. See Constrain Global Variable Range in the documentation for Polyspace Code Prover or Polyspace Code Prover Server.

• Replace the volatile variable with a stubbed function, but only for verification. Before verification, specify constraints on the stubbed functions.

  1. Write a Perl script that replaces each volatile variable declaration with a nonvolatile declaration where you obtain the variable value from a function call.

     For example, if your code contains the line volatile s8 PORT_A, your Perl script can contain this substitution:

     $line=~ s/^\s*volatile\s*s8\s*PORT_A;/s8 PORT_A = random_s8();/g;

  2. Specify the location of this Perl script for the analysis option Command/script to apply to preprocessed files (-post-preprocessing-command).

  3. In an include file, provide the function declaration. For example, for a function random_s8, the include file can contain the following declaration:

     #ifndef POLYSPACE_H
     #define POLYSPACE_H
     signed char random_s8(void);
     #endif
     

  4. Insert a #include directive for your include file in the relevant source files

     Instead of a manual insertion, specify the location of your include file for the analysis option Include (-include).

  For more information on analysis options, see the documentation for Polyspace Code Prover or Polyspace Code Prover Server.