问题标签 [cbmc]

让我们考虑下面给出的代码，我可以知道为什么 CBMC 在我们假设 io 的初始值大于 2 的情况下展开超过上限。

CBMC 输出：

我使用CBMC来验证我的Pthreads程序，它检测到一些我认为不存在的断言错误。该错误仅在我同时运行两个线程时发生。也就是说，当我将调用线程函数（func或func1）的语句之一放入注释时，CBMC 就可以验证它是否成功。a数组和的赋值有冲突b吗？

CBMC的输出如下：

我是JBMC（有界模型检查器）的新手。我们需要找出在不运行Java程序的情况下可能发生在Java程序中的RunTime Exception的可能性。我们搜索了一些抽象解释框架，发现 JBMC 在这种情况下会有所帮助。

例如 ：

在上面的程序中，当循环在第 6 次迭代期间运行时，我们将得到 ArrayIndexOutOfBoundException。但是如何使用 JBMC 来预测呢？我们找到了提供 JBMC 中命令行选项详细信息的命令表，但我们无法找到命令组合以及如何使用它。是否有可用于 JBMC 的 Java API 或文档？

请推荐！！

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

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

更新：

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

然后通过pycparser解析程序

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

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

我正在尝试在 CBMC 中获取数组的所有排列。对于小情况，例如 [1,2,3]，我想我可以写

但是对于较大的元素，代码会非常混乱。所以我的问题是有没有更好/通用的方式来表达这一点？

我正在尝试在具有一个主中断的大型嵌入式软件堆栈上使用 CBMC。.c 文件解析得很好，但我坚持使用以下代码对中断行为进行建模：

main_interrupt()做了各种各样的事情，比如读取输入、设置输出、安全检查等。我想测试空指针解引用的 ADC 读取功能，这需要main_interrupt()运行。测试看起来像这样：

BMC_intr_0() 中的main_interrupt()调用包含在__CPROVER_atomic_begin ()和__CPROVER_atomic_end()中，因为据我了解，CBMC 将BMC_intr_0()建模为与 ADC_Read_test 并发运行的额外线程。因此，为了防止在BMC_intr_0（中断）运行时执行 ADC_Read_test，它被包装在一个原子块中。问题是 CBMC 向我抛出了这个：

从这个文件：line。

我的问题是，为什么？这个错误是什么意思？我在这方面找到了 0 个文档，我将不胜感激！

我是 CBMC 的新手并正在尝试它。在此链接中，有一个玩具示例，用于使用 CBMC 检查函数 binsearch。我决定运行他们提供的以下命令，只是改变了循环展开的次数：

它返回以下内容：

展开断言失败是因为没有足够的迭代是一件坏事吗？从我的角度来看，这个例子似乎没有错误，因为代码没有访问它不应该访问的内存部分，但我不确定是否基于那个展开断言失败。有人对安全性有任何想法吗？那次失败重要吗？

我看到类似在Linux RCU 测试和用于 CBMC 分析的 pthread 包装器__CPROVER_fence("RRfence", "RWfence");等项目中使用的代码。我查看了在线文档，但在发送到此 CBMC 函数的字符串中没有发现任何文本。

有哪些可用参数__CPROVER_fence？

我的看法是，它是一个注释/函数，用于表示由实际实现执行的障碍/栅栏。即，它是真实功能的分析存根。显然参数表示屏障的类型，但我没有找到实际参数和相应屏障类型的参考。即，“RRFence”是一个读栅栏，这意味着在此点之前的读取将在此点之后的读取之前完成（作为猜测）。