cbmc是如何使用c头的？

Question

如果我有一个包含多个函数的c文件，并且我想在预处理版本的程序(使用gcc)上运行带有z3求解器的cbmc，并且在header部分有一些其他文件(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’未声明

Answer 1

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

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

    else
    {
        return 1;
    }
}