Consider volatile qualifier on fields (-consider-volatile-qualifier-on-fields)

Assume that volatile qualified structure fields can have all possible values at any point in code

Description

This option affects a Code Prover analysis only.

Specify that the verification must take into account the volatile qualifier on fields of a structure.

Set Option

User interface (desktop products only): In your project configuration, the option is available on the Verification Assumptions node.

Command line and options file: Use the option -consider-volatile-qualifier-on-fields. See Command-Line Information.

Why Use This Option

The volatile qualifier on a variable indicates that the variable value can change between successive operations even if you do not explicitly change it in your code. For instance, if var is a volatile variable, the consecutive operations res = var; res =var; can result in two different values of var being read into res.

Use this option so that the verification emulates the volatile qualifier for structure fields. If you select this option, the software assumes that a volatile structure field has a full range of values at any point in the code. The range is determined only by the data type of the structure field.

Settings

On

The verification considers the volatile qualifier on fields of a structure.

In the following example, the verification considers that the field val1 can have all values allowed for the int type at any point in the code.

struct myStruct {
   volatile int val1;
   int val2;
};

Even if you write a specific value to val1 and read the variable in the next operation, the variable read results in any possible value.

struct myStruct myStructInstance;
myStructInstance.val1 = 1;
assert (myStructInstance.val1 == 1); // Assertion can fail

Off (default)

The verification ignores the volatile qualifier on fields of a structure.

In the following example, the verification ignores the qualifier on field val1.

struct myStruct {
   volatile int val1;
   int val2;
};

If you write a specific value to val1 and read the variable in the next operation, the variable read results in that specific value.

struct myStruct myStructInstance;
myStructInstance.val1 = 1;
assert (myStructInstance.val1 == 1); // Assertion passes

Tips

• If your volatile fields do not represent values read from hardware and you do not expect their values to change between successive operations, disable this option. You are using the volatile qualifier for some other reason and the verification does not need to consider full range for the field values.

• If you enable this option, the number of red, gray, and green checks in your code can decrease. The number of orange checks can increase.

  In the following example, a red or green check changes to orange or a gray check goes away when the option is used. Considering the volatile qualifier changes the check color. These examples use the following structure definition:

  struct myStruct {
     volatile int field1;
     int field2;
  };
  
  

  Color Without Option	Result Without Option	Result With Option
  Green	void main(){ struct myStruct structVal; structVal.field1 = 1; assert(structVal.field1 == 1); }	void main(){ struct myStruct structVal; structVal.field1 = 1; assert(structVal.field1 ==1); }
  Red	void main(){ struct myStruct structVal; structVal.field1 = 1; assert(structVal.field1 != 1); }	void main(){ struct myStruct structVal; structVal.field1 = 1; assert(structVal.field1 !=1); }
  Gray	void main(){ struct myStruct structVal; structVal.field1 = 1; if (structVal.field1 != 1) { /* Perform operation */ } }	void main(){ struct myStruct structVal; structVal.field1 = 1; if (structVal.field1 != 1) { /* Perform operation */ } }

• In C++ code, the option also applies to class members.

Command-Line Information

Parameter: -consider-volatile-qualifier-on-fields

Default: Off

Example (Code Prover): polyspace-code-prover -sources file_name -consider-volatile-qualifier-on-fields

Example (Code Prover Server): polyspace-code-prover-server -sources file_name -consider-volatile-qualifier-on-fields