Boolean 変数に関する Code Prover の仮定

Boolean 変数の定義には、C では _Bool キーワード (または stdbool.h で定義された bool マクロ) が使用され、C++ では bool キーワードが使用されます。C 標準 (C99、第 6.3.1.2 節) では、スカラー値が _Bool に変換される場合、その値が 0 に等しければ結果は 0 になり、そうでなければ結果は 1 になります。

不明な値の Boolean 変数に関する Code Prover の仮定

Code Prover では、Boolean 変数に関する C 標準の仕様に従っています。たとえば、不明なソースからの Boolean 変数への明示的な書き込みに従い、解析では Boolean 変数の値は 0 または 1 になると仮定されます。

たとえば以下の例では、getFlag() の定義は不明です。関数 getFlag() による変数 flag への明示的な代入に従い、この変数の値は 0 または 1 になると仮定されます。

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

Boolean 変数の値が 0 または 1 以外になる場合

場合によっては、Code Prover で Boolean 変数の値が 0 または 1 であると仮定されないことがあります。代わりに、解析では、変数は基となる型 (ほとんどの場合は unsigned char) で許容される全範囲の値を取る可能性があると仮定されます。

次に例を示します。

• Boolean 変数が volatile の場合、たとえばメモリマッピング済み周辺装置を使用して、この変数を変更できます。Code Prover では、Boolean 変数 volatile の値が 0 または 1 であると仮定されません。

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

• Boolean 変数が共用体の一部となっている場合、たとえば共用体の他のメンバーを変更して、この変数を変更することが可能です。Code Prover では、共用体のメンバーである Boolean の値が 0 または 1 であると仮定されません。

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