问题标签 [cbmc]

Is there a way that I can call CBMC from Python or is there any wrapper or API for it available?

My Problem is the following. I want to create a C function automatically in Python (this works quite well) and sent them to CBMC from Python for checking and get feedback if the function is OK or not.

是否可以在没有 Visual Express 的情况下独立运行 CBMC？我需要重新编译它还是可能有其他技巧？

我只需要定期使用CBMC将一个函数翻译成CNF，所以我想用函数名调用它，将cnf文件写入磁盘并重新开始。我不想使用 Visual Studio。

我试图约束表b[4][4]，使得只有那些具有i>=j并满足条件(stored[i] & stored[j]) == stored[i]为 1 的地方，其余为 0。

为什么这不起作用？

CProver 假设试图获得b[i][j] == 1应该暗示的效果stored[i]& stored[j] == stored[i]。但是输出没有这个效果。有什么问题？我是 CBMC 和 C 的新手。

我正在努力想出一个更好的解决方案来声明 CBMC（C 有界模型检查器）中的“恰好一次”属性。我的意思是一行中的一个元素位置应该具有值 1（或任何可以检查为布尔值 true 的正数），其余的必须全为零。

对于 M = 4

对于比这更大的 M，这是一个巨大的问题。可以说 M = 8 我必须做类似的事情：

检查一次的违规很容易，但说明它看起来很重要。我可能还有一个选择：将二维数组问题表述为一维位向量问题，然后进行一些智能异或。但我目前不确定。

有人对这个问题有更好的解决方案吗？

CBMC 在以下行中检测到可能的无符号加法溢出：

我同意第一行有溢出的可能性，但我正在处理 CBMC 无法查看的下一行中的进位。如果出现溢出，我将设置进位 1。因此，由于我知道这一点，这就是我希望我的代码工作的方式，我想继续验证过程。那么，我是如何告诉 CBMC 忽略这个错误并继续前进的呢？

我正在编写程序但收到此警告！有人可以在这方面帮助我。

我知道当编译器在函数使用之前没有看到声明时会出现此警告。但是我已经声明了 setWeight 函数并且看起来类型太匹配了。请帮帮我，从昨晚开始我就被困在这里了。谢谢

我只是想得到一个具有哈密顿路径的总节点 6 的图表。这适用于上面的代码。但是，当我尝试使用 len 即总边缘数时，我在 cbmc run 中得到了无限展开。

上面的代码运行良好，除非我使用 len 进行迭代。cbmc 运行进入无限展开？？谁能解释一下。

我正在尝试在 Ubuntu 中将CBMC Bounded Model Checker 用于 C 和 C++ 程序。我已经下载了 gcc (4.9 v) 和 g++ (4.9 v) 编译器，并通过终端安装了 CBMC。

我能够使用以下过程验证 C 程序并且没有出现任何问题：

具有名称的 .c 文件file2.c：

在终端类型中：

输出：

当我尝试执行以下 .cpp 文件时出现错误。

sum_num.cpp文件：

输入终端：

输出 - 错误：

我有以下代码片段。

在这段代码中，我将 1 个字节的内存分配给一个指针。然后我正在访问分配内存后 20 个单位的内存位置。当我取消引用该指针时，我预计会收到内存访问冲突错误或分段错误或类似的东西。我没有收到任何此类错误。

让我们假设这是一个未定义行为的情况。所以我尝试使用CBMC验证这个程序，CBMC是一个使用以下命令的著名模型检查器。

CBMC 报告该程序是安全的。是 CBMC 的问题还是我遗漏了什么？

我正在尝试在来自 GitHub 的开源 C 项目上使用 CBMC（C 有界模型检查： https ://www.cprover.org/cbmc/）。对于这个问题，让我们考虑以下项目：https ://github.com/reubenhwk/radvd

当我用 gcc 编译项目时出现问题。我能够获得调用 cbmc 之类的可执行文件

但我收到以下错误消息：

原因应该是我使用 gcc 而不是 goto-cc （如此处所述：http ://www.cprover.org/cprover-manual/goto-cc.html ），所以它可能无法识别该文件。我还尝试使用 goto-cc，如上一个链接和一些示例中所述，例如http://www.cprover.org/goto-cc/examples/nanosat.html。但是，由于它们是有指导的示例，因此使 cbmc 工作似乎很容易。当我对其他项目执行相同的过程时，例如链接的项目（radvd）并使用 goto-cc 而不是 gcc 我在运行make CC=goto-cc命令时收到以下消息：

我目前在虚拟 Linux 机器（Ubuntu 17.10）上使用 5.8 版的 cbmc。

你知道如何让它工作吗？

谢谢