0

如果我有一个包含多个函数的 ac 文件,并且我想在程序的预处理版本(使用 gcc)上运行带有 z3 求解器的 cbmc,并且标题部分中还有一些其他文件(c 文件)。cbmc 将如何查看这些文件?因为我试图运行它,他给出了一些关于一些变量的错误,因为它们没有在它的位置声明,事实上,它们是在一个头文件中声明的。

谁能解释这是如何工作的?

更新:

int test(int x) {
for (int i = 2; i < sqrt(x); i++) {
    if (x%i == 0)
        return 0;
}

首先,我使用 gcc 对程序进行预处理

然后通过pycparser解析程序

然后仪器(在4后添加打印语句以查看x的值)

然后我在文件的检测版本上运行 cbmc,我得到了这个错误:函数 `sqrt' 没有声明

4

1 回答 1

0

您应该在项目中包含头文件引用的所有文件。如果相关的 .c 文件不可用,仅包含正确的标头是不够的。


您的示例代码还必须包含以下几行:

    else
    {
        return 1;
    }
}
于 2019-06-25T09:00:36.180 回答