`main` 関数に関する Code Prover の仮定

完全な実行可能ファイルにコンパイルされる C/C++ プログラムには main 関数が含まれます。Code Prover 解析では、main 関数が他の関数とは異なる方法で扱われます。

呼び出し階層の最上位としての `main` 関数

Code Prover は、main 関数を検証の開始点と見なします。自分で main 関数を提供しない場合、たとえばライブラリを検証する際には、検証によってこの関数が一つ生成されます。既定では、生成された main は、他の場所では呼び出されない関数を呼び出します。

その上で、検証は main 関数から開始して、呼び出し階層の下位に向かって処理されていき、main から呼び出される関数などが検証されます。

検証の時間または精度を調整するには、次のようにします。

生成される main の内容は、解析オプションを使用して変更できます。
ライブラリの検証の構成を参照してください。
検証対象として指定する関数のみを呼び出す、独自の main を記述できます。

`main` 関数の引数

main 関数は、次の 3 つの形式のいずれかにすることができます。

引数を取らない形式:
```
int main() {}
```
2 つの引数を取る形式:
```
int main(int argc, char* argv[]) {}
```
その他の処理系定義の形式

C/C++ 標準の仕様に従い、検証では main 関数の引数について特定の仮定が行われます。main 関数で取る引数のデータ型が 2 番目の形式と一致する場合、Code Prover はこの形式を前提として、対応する制約を引数に適用します。特に以下に注意してください。

main 関数の 1 番目の引数が整数 (または整数に対する typdef) の場合、検証ではこの引数が非負の整数であると仮定されます。この引数は、外部環境からプログラムに渡される追加の引数の数を示します。
この仮定は、main 関数がこの 1 つの引数のみを取る場合にも適用されます。
1 番目の引数が整数で、2 番目の引数がポインターへのポインター (またはポインターへのポインターに対する typedef) である場合、検証では最初の引数 argc とサイズが等しいバッファーが 2 番目の引数に割り当てられていると仮定されます。バッファーの各要素 (argv[0]、argv[1]、…、argv[argc-1]) も初期化済みポインターであると仮定されます。この引数には、外部環境からプログラムに渡される追加の引数が格納されます。

参考

トピック

ライブラリの検証の構成