CBMC 玩具示例

Question

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

cbmc binsearch.c --function binsearch --unwind 4 --bounds-check --unwinding-assertions

它返回以下内容：

** Results:
[binsearch.unwind.0] unwinding assertion loop 0: FAILURE
prog.c function binsearch
[binsearch.array_bounds.1] line 7 array `a' lower bound in a[(signed long int)middle]: SUCCESS
[binsearch.array_bounds.2] line 7 array `a' upper bound in a[(signed long int)middle]: SUCCESS
[binsearch.array_bounds.3] line 9 array `a' lower bound in a[(signed long int)middle]: SUCCESS
[binsearch.array_bounds.4] line 9 array `a' upper bound in a[(signed long int)middle]: SUCCESS

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

Answer 1

基于--unwinding-assertion 属性，它检查以下内容：

检查--unwind 是否足够大以覆盖所有程序路径。如果参数太小，CBMC 将检测到未完成足够的展开，并报告展开断言失败。

我会说这是对没有足够的循环迭代以确保函数不会访问边界之外的数组的可能性的警告。这意味着虽然该函数没有违反 4 的任何属性，但我们需要检查所有路径才能确定它是安全的。