c - cbmc 如何与 c 标头一起使用？

Question

如果我有一个包含多个函数的 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' 没有声明

Answer 1

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

---

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

    else
    {
        return 1;
    }
}