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

解开断言因为没有足够的迭代而失败的事实是不是一件坏事？从我的角度来看，这个例子似乎没有bug，因为代码没有访问它不应该访问的内存部分，但我不确定基于解开断言失败的原因。有谁对安全性有什么想法吗？那次失败有关系吗？

Answer 1

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

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

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