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.

• 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).

• 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.

• 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).