Code Prover Assumptions About Boolean Variables

Boolean variables are defined through the _Bool keyword in C (or the bool macro defined in stdbool.h) and the bool keyword in C++. The C Standard (C99, Section 6.3.1.2) states that when a scalar value is converted to _Bool, the result is 0 if the value is equal to 0; otherwise, the result is 1.

Code Prover Assumptions About Boolean Variables with Unknown Values

Code Prover adheres to the specifications of the C standard regarding Boolean variables. For instance, the analysis assumes that following explicit writes to a Boolean variable from unknown sources, the variable can have a value 0 or 1.

For instance, in this example, the definition of getFlag() is unknown. Following the explicit assignment to the variable flag from the getFlag() function, the variable is assumed to have a value of 0 or 1.

_Bool getFlag();
void main() {
    _Bool flag = getFlag(); //flag is 0 or 1
    //...
}

Cases Where Boolean Variables Can Have Values Other Than 0 or 1

In some cases, Code Prover does not assume a value of 0 or 1 for a Boolean variable. Instead, the analysis assumes that the variable can have the full range of values allowed by the underlying type (in most cases, unsigned char).

For instance:

• If the Boolean variable is volatile, it can be modified, for instance, using memory-mapped peripherals. Code Prover does not assume a value of 0 or 1 for volatile Boolean variables.

  _Bool func() {
      volatile _Bool flag; 
      //...
      return flag; //flag is in 0 .. 255
  }

• If the Boolean variable is part of an union, it can be modified, for instance, by modifying other members of the union. Code Prover does not assume a value of 0 or 1 for Boolean members of a union.

  typedef union U {
      int x;
      _Bool flag;
  } U;
  
  _Bool func() {
     U u;
     u.x = 11;
     return u.flag; //u.flag is in 0 .. 255
  }