Const volatile scalar mode (-const-volatile-scalar-behavior) - Specify how initialized const volatile scalar variables are treated during analysis

Description

Specify whether initialized const volatile scalar variables are treated as constants or as volatile variables with a full range of values during analysis.

Set Option

Set the option using one of these methods:

Polyspace Platform user interface (desktop products only): In your project configuration, on the Static Analysis tab, select the Run Time Errors > Verification Assumption node and then select this option.
Command line and options file: Use the option -const-volatile-scalar-behavior. See Command-Line Information.
Python^® API: Set the ConstVolatileScalarBehavior property in the static analysis configuration. See polyspace.project.StaticAnalysisConfiguration (Polyspace Test).
TOML configuration file (.toml.pscfg) — Use the key ConstVolatileScalarBehavior in the [CodeProverVerification.VerificationAssumption] table with a value of const or volatile. For example:
```
[CodeProverVerification.VerificationAssumption]
ConstVolatileScalarBehavior = "volatile"
```

Why Use This Option

In many situations, const volatile scalar variables are initialized to a known value and are not expected to change at run time. Because of this, the analysis treats const volatile scalars as constants by default. This default behavior produces more precise results by eliminating spurious code paths that arise from considering the full range of values.

However, if you expect one or more const volatile scalar variables in your code base to change at run time, set the -const-volatile-scalar-behavior analysis option to volatile. This setting instructs the analysis to treat such variables as volatile variables with a full range of allowed values at any point in the code.

Code Prover

When the option is set to const, Polyspace^® Code Prover™ uses the initialization value for const volatile scalars. This reduces the number of orange checks in your analysis. If a const volatile scalar is not initialized, Polyspace Code Prover stops the analysis with an error.

When the option is set to volatile, Polyspace Code Prover assumes that const volatile scalars can have any value allowed by their type at any point in the code.

Bug Finder

When the option is set to const, Polyspace Bug Finder™ uses the initialization value for const volatile scalars. This can reduce false positive defects in your analysis. If a const volatile scalar is not initialized, Polyspace Bug Finder treats it as a volatile variable with a full range of values.

When the option is set to volatile, Polyspace Bug Finder assumes that const volatile scalars can have any value allowed by their type.

Settings

Default: const

const

The analysis treats initialized const volatile scalar variables as constants. The analysis uses the initialization value of the variable.

This behavior applies to scalar types, including integral, floating-point, and enumerated types, as well as arrays of scalars.

In the following example, cvint is treated as having the value 2. The condition cvint == 2 is always true, so the else branch is dead code.

const volatile int cvint = 2;

void func(void) {
    int check;
    if (cvint == 2) {    // Always true
        check = 1;
    } else {             // Unreachable code
        check = 0;
    }
    assert(check == 0);  // Always fails
}

volatile

The analysis treats const volatile scalar variables as volatile. The analysis assumes that the variable can have any value allowed by its type at any point in the code, regardless of the initialization value.

In the following example, cvint is treated as having any possible int value. The condition cvint == 2 may or may not be true, so both branches are reachable.

const volatile int cvint = 2;

void func(void) {
    int check;
    if (cvint == 2) {    // May or may not be true
        check = 1;
    } else {
        check = 0;
    }
    assert(check == 0);  // May or may not fail
}

Tips

This option applies only to scalar types. Pointers, structures, and unions declared as const volatile are not affected by this option and are always treated as volatile.
```
const volatile int *ptr = 0x8000; // Not affected
const volatile struct { int x; } s = { .x = 8 }; // Not affected
```

This option applies to both global and local const volatile scalars, as well as static const volatile scalars.

const volatile int global_cv = 1; // Affected

void func(void) {
    const volatile int local_cv = 2; // Affected
    static const volatile int static_cv = 3; // Affected
}

Arrays of const volatile scalars are also affected by this option. Each element of the array is treated according to the specified mode.
```
const volatile int cvarray[] = {1, 2, 3}; // Each element affected
```
If you specify a range for a const volatile variable using a constraint setup (Data Range Specification), the constraint range takes precedence over the mode selected by this option. The analysis uses the constrained range regardless of whether const or volatile mode is active.
If you use const volatile variables to represent calibration parameters or compile-time constants, use the const mode for more precise analysis results.
If you use const volatile variables to represent hardware-mapped registers whose values can change unpredictably, use the volatile mode to account for all possible values.
If you set the option to const and a const volatile scalar is not initialized, Polyspace Code Prover stops the analysis with an error. Either provide an initializer or use volatile mode for such variables.
If you set the option to const and a const volatile scalar is not initialized, Polyspace Bug Finder treats the variable as a volatile variable with a full range of values.

Command-Line Information

Parameter: -const-volatile-scalar-behavior

Value: const | volatile

Default: const

Example (Bug Finder):

polyspace-bug-finder -sources file_name
                    -const-volatile-scalar-behavior volatile

Example (Code Prover):

polyspace-code-prover -sources file_name
                    -const-volatile-scalar-behavior volatile

Example (Bug Finder Server):

polyspace-bug-finder-server -sources file_name
                    -const-volatile-scalar-behavior volatile

Example (Code Prover Server):

polyspace-code-prover-server -sources file_name
                    -const-volatile-scalar-behavior volatile

Const volatile scalar mode (`-const-volatile-scalar-behavior`)

Description

Set Option

Why Use This Option

Settings

Tips

Command-Line Information

Version History

See Also

Topics