スタブ関数に関する Code Prover の仮定

検証では、ソースコードで定義されていない関数、またはスタブ化することを選択した関数がスタブ化されます。スタブ関数の場合、以下が行われます。

検証では、関数の戻り値と関数のその他の二次的影響について特定の仮定が行われます。
このような仮定は、制約を指定することで微調整できます。
検証では、関数本体が存在しても無視されます。関数本体内の演算のランタイムエラーはチェックされません。

関数本体の検証精度が低く、その関数を呼び出すと多くのオレンジチェックが表示される場合、その関数をスタブ化することを選択できます。オレンジチェックの数を減らすには、その関数をスタブ化し、その後関数の戻り値を制約して、他の二次的影響を指定します。

関数をスタブ化する場合、以下のオプションを使用できます。

スタブを生成する関数 (-functions-to-stub):スタブ化する関数を指定します。
Embedded Coder ルックアップテーブル用スタブの生成 (-stub-embedded-coder-lookup-table-functions):Embedded Coder^® を使用してモデルから生成されたルックアップテーブルをコードに含む関数をスタブ化します。
-code-behavior-specifications:Polyspace^® が認識する標準関数に対応する関数をスタブ化します。

関数をスタブ化する際に最初のオプションを使用する場合、制約を指定することで、関数の戻り値を制約し、他の二次的影響をモデル化します。Polyspace の制約指定インターフェイスを使って指定できる制約よりも細かく制約を指定する場合、独自のスタブを定義します。関数をスタブ化する際にその他のオプションを使用する場合、本ソフトウェア自体によって関数の戻り値が制約され、その二次的影響が適切にモデル化されます。制約指定の詳細については、以下を参照してください。

検証では、スタブ関数の引数について以下の仮定が行われます。

関数の戻り値

仮定

検証では、以下の仮定が行われます。

その関数から返される変数は、そのデータ型で許容される全範囲の値を取るものとします。
関数が enum 変数を返す場合、変数は enum 型の範囲内の値を取ります。たとえば、enum 型が値 {0,5,-1,32} を取り、スタブ関数がこの型の戻り値を返す場合、検証では関数の戻り値が範囲 -1 ～ 32 の値を取ると仮定されます。
関数がポインターを返す場合、そのポインターは NULL にはならず、デリファレンスに対して安全であるものとします。ポインターが動的に割り当てられるメモリを指す場合はありますが、コード内の別の変数と同じメモリ位置を指すことはできません。
(C++ のみ) 演算子 new は割り当て済みのメモリを返します。演算子 operator=、operator+=、operator-- (接頭辞付きバージョン) または operator<< は以下を返します。
- 演算子がクラス定義の一部の場合、*this への参照。
  たとえば、演算子が以下のように定義されるとします。
```
class X {
  X& operator=(const X& arg) ;
};
```
  この場合、*this (この演算子を呼び出すオブジェクト) への参照を返します。この演算子を呼び出すオブジェクトまたはそのデータメンバーは、その型で許容される全範囲の値を取ります。
- 演算子がクラス定義の一部ではない場合、最初の引数。
  たとえば、演算子が以下のように定義されるとします。
```
X& operator+=(X& arg1, const X& arg2) ;
```
  この場合、arg1 を返します。arg1 が参照するオブジェクトまたはそのデータメンバーは、その型で許容される全範囲の値を取ります。
(C++ のみ) __declspec(no_return) (Visual Studio^®) または __attribute__ ((noreturn)) (GCC) により宣言された関数は返されません。コードにこのような関数が含まれている場合、関数呼び出しにはツールヒントと赤の破線の下線が表示されます。たとえば、この例では fatal() の呼び出しに赤の破線の下線が表示されます。
```
void fatal(int) __attribute__ ((noreturn));
          
void main() {
    int x = 0;
    fatal(x);
    x++;
}
```

仮定の変更方法

関数の戻り値に関する既定の仮定は変更することができます。

関数が非ポインター変数を返す場合、その範囲を制約できます。オプション [制約の設定] (-data-range-specifications) を使用します。
制約指定インターフェイスを使用して、絶対範囲 [min..max] を指定できます。もっと複雑な制約を指定する場合は、関数スタブを作成します。
たとえば、未定義の関数のプロトタイプが次のようになっているとします。
```
int func(int ll, int ul);
```
ここで、この関数が最初の引数と 2 番目の引数の間に含まれる値を返すことがわかっているとします。ただし、この関数が定義されていないため、本ソフトウェアでは戻り値が全範囲を取り得ると仮定されます。必要な動作をモデル化して、不正確さによるオレンジチェックを減らすには、関数スタブを次のように作成します。
```
int func(int ll, int ul) {
     int ret;
     assert(ret>=ll && ret <=ul);
     return ret;
}
```
この関数スタブは検証用に別のファイルに用意します。検証では、このスタブが関数定義として使用されます。
func の定義がコード内に存在しても、関数本体の検証が不正確になるためこの定義をオーバーライドする場合は、次のように実際の定義とスタブを #ifdef ステートメントに含めます。
```
#ifdef POLYSPACE
int func(int ll, int ul) {
     int ret;
     assert(ret>=ll && ret <=ul);
     return ret;
}
#else
int func(int ll, int ul) {
    /*Your function body */ 
}
#endif
```
マクロ POLYSPACE は、オプションプリプロセッサ定義 (-D)を使用して定義します。検証では、実際の関数定義の代わりにスタブが使用されます。
関数がポインター変数を返す場合、そのポインターが NULL になる可能性があることを指定できます。
- すべてのスタブ関数に対してこの仮定を指定するには、オプション環境ポインターが安全でないことを考慮する (-stubbed-pointers-are-unsafe)を使用します。
- 特定のスタブ関数にこの仮定を指定するには、オプション [制約の設定] (-data-range-specifications) を使用します。

関数のポインター引数

仮定

検証では、以下の仮定が行われます。

引数がポインターの場合、関数は、ポインターが指すオブジェクトに、任意の値を書き込む可能性があるものとします。値の範囲は、引数のデータ型によってのみ制約されます。
たとえば、以下の例の検証では、スタブ関数 stubbedFunc が val に可能性のあるすべての値を書き込むと仮定されます。したがって、アサーションはオレンジになります。
```
void stubbedFunc(int*);

void main() {
    int val=0, *ptr=&val;
    stubbedFunc(ptr);
    assert(val==0);
}
```
引数が構造体へのポインターの場合、関数は、構造体フィールドに任意の値を書き込む可能性があるものとします。値の範囲は、フィールドのデータ型によってのみ制約されます。
C++ コードでは、構造体の最初のレベルのデータメンバーのみを構造体へのポインターを介して書き込むことができます。たとえば、以下の例では、pb->j が指す内容は解析で認識されますが、pb->pa->i が指す内容は認識されません。このため、Foo を呼び出した後、b.j は初期化されたものとして表示されますが、a.i は初期化されません。
```
struct A {
   int i;
};
 
struct B {
   A* pa;
   int j;
};
 
void Foo(B*);
 
void main() {
    A a;
    B b;
    b.pa = &a;
    Foo(&b); 
    int var1 = b.j;
    int var2 = a.i;
}
```
引数が別のポインターへのポインターの場合、関数は、2 番目のポインターが指すオブジェクトに、任意の値を書き込む可能性があるものとします (C コードのみ)。この仮定は、ポインター階層の深さが何段階になっても引き継がれます。
たとえば、ポインター **pp は別のポインター *p を指します。この別のポインターが int 型の変数 var を指すとします。スタブ関数が引数として **p を受け取る場合、検証では、関数呼び出しに伴い、var は int 型が取り得るすべての値になると仮定されます。*p は割り当て済みメモリの任意の場所、つまり var を指す可能性はありますが、コード内の別の変数を指すことはありません。
引数が関数ポインターの場合、そのポインターが指す関数が呼び出されるものとします (C コードのみ)。
たとえば、以下の例のスタブ関数 stubbedFunc は、引数として関数ポインター funcPtr を受け取ります。この funcPtr は func を指し、stubbedFunc を呼び出すと、この関数が呼び出されます。
```
typedef int (*typeFuncPtr) (int);

int func(int x){
  	return x;
}

int stubbedFunc(typeFuncPtr);

void main() {
    typeFuncPtr funcPtr = (typeFuncPtr)(&func);
    int result = stubbedFunc(funcPtr);
}
```
関数ポインターが引数として別の関数ポインターを受け取る場合、2 番目の関数ポインターが指す関数がスタブ化されます。

仮定の変更方法

参照渡しされる引数の範囲を制約することができます。オプション [制約の設定] (-data-range-specifications) を使用します。

制約指定インターフェイスを使用して、絶対範囲 [min..max] を指定できます。もっと複雑な制約を指定する場合は、関数スタブを作成します。

たとえば、未定義の関数のプロトタイプが次のようになっているとします。

void func(int *x, int ll, int ul);

ここで、x に書き込まれる値が 2 番目の引数と 3 番目の引数の間に含まれることがわかっているとします。ただし、この関数が定義されていないため、本ソフトウェアでは *x の値が全範囲を取り得ると仮定されます。必要な動作をモデル化して、不正確さによるオレンジチェックを減らすには、関数スタブを次のように作成します。

void func(int *x, int ll, int ul) {
     assert(*x>=ll && *x <=ul);
}

この関数スタブは検証用に別のファイルに用意します。検証では、このスタブが関数定義として使用されます。

func の定義がコード内に存在しても、関数本体の検証が不正確になるためこの定義をオーバーライドする場合は、次のように実際の定義とスタブを #ifdef ステートメントに含めます。

#ifdef POLYSPACE
void func(int *x, int ll, int ul) {
     assert(*x>=ll && *x <=ul);
}
#else
void func(int *x, int ll, int ul) {
     /* Your function body */
}
#endif

マクロ POLYSPACE は、オプションプリプロセッサ定義 (-D)を使用して定義します。検証では、実際の関数定義の代わりにスタブが使用されます。

グローバル変数

仮定

検証では、関数スタブはグローバル変数を変更しないと仮定されます。

仮定の変更方法

グローバル変数への書き込み操作をモデル化するには、関数スタブを作成します。

たとえば、未定義の関数のプロトタイプが次のようになっているとします。

void func(void);

ここで、関数がグローバル変数 glob に値 0 または 1 を書き込むことがわかっているとします。必要な動作をモデル化するには、関数スタブを次のように作成します。

void func(void) {
     volatile int randomVal;
     if(randomVal)
          glob = 0;
     else
          glob = 1;
}

この関数スタブは検証用に別のファイルに用意します。検証では、このスタブが関数定義として使用されます。

#ifdef POLYSPACE
void func(void) {
     volatile int randomVal;
     if(randomVal)
          glob = 0;
     else
          glob = 1;
}
#else
void func(void) {
     /* Your function body */
}
#endif

マクロ POLYSPACE は、オプションプリプロセッサ定義 (-D)を使用し定義します。検証では、実際の関数定義の代わりにスタブが使用されます。