複数の関数を含む ac ファイルがあり、(gcc を使用して) 前処理されたバージョンのプログラムで z3 ソルバーを使用して cbmc を実行したい場合、ヘッダー セクションに他のファイル (c ファイル) がいくつかあります。cbmc はこれらのファイルをどのように認識しますか? 私はそれを実行しようとしましたが、彼はいくつかの変数について、それがどこにあるか宣言されていないというエラーを出しました。実際、それらはヘッダーファイルの1つで宣言されています。
誰かがこれがどのように機能するか説明できますか?
アップデート：
int test(int x) {
for (int i = 2; i < sqrt(x); i++) {
if (x%i == 0)
return 0;
}
まず、gcc を使用してプログラムを前処理します。
次に、pycparser でプログラムを解析します
次に、計器 (4 の後に print ステートメントを追加して、x の値を確認します)
次に、インストルメント化されたバージョンのファイルで cbmc を実行したところ、次のエラーが発生しました: 関数 `sqrt' は宣言されていません