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

【问题标题】：How cbmc works with c header?cbmc 如何与 c 标头一起使用？
【发布时间】：2019-06-24 15:53:16
【问题描述】：

如果我有一个包含多个函数的 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解析程序

然后instrument（在4后面加print语句查看x的值）

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

【问题讨论】：

欢迎来到 SO！请提供您尝试解决的问题的minimal, reproducible example，以及您在控制台中收到的错误输出。看到这将有助于人们回答您的问题。
我更新我的帖子，谢谢

标签： c z3 pycparser cbmc

【解决方案1】：

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

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

    else
    {
        return 1;
    }
}

【讨论】：