Code Prover Assumptions About Volatile Variables

A Polyspace^® analysis assumes that values of volatile variables can change without explicit write operations.

Global Volatile Variables

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 for Polyspace Analysis.

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

Local Volatile Variables

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);
}

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 for Polyspace Analysis.

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

Volatile Parameters

A volatile qualifier on a pass-by-copy function parameter is ignored because the copied parameters cannot be memory-mapped to I/O registers and are not likely to change their values without explicit write operations in the code. The volatile qualifier continues to apply on pass-by-reference parameters.

In this example, the argument x is passed by copy and y by reference. The analysis does not apply the volatile assumption of full-range values to the first parameter but continues to apply them to the variable that the second parameter points to.

void foo(volatile int x, volatile int *y_ptr) {
    x = 1;
    assert(x==1); 
    *y_ptr = 1;
    assert(*y_ptr==1); 
}

void foo_caller(void) {
    volatile int x;
    volatile int y;
    
    x = 1;
    assert(x==1); 
    
    y = 1;
    assert(y==1); 
    
    foo(x, &y);
}