CBMC验证binsearch时unwinding assertion失败是否影响安全判定

循环展开不足导致的unwinding assertion失败是否严重 #

该类失败不属于代码本身的逻辑错误，但属于验证不完整的明确告警，会直接导致验证结果失去全局可信度，需要先修复该问题才能得到有效的验证结论。
--unwinding-assertions的作用是校验你设置的--unwind次数是否能覆盖循环所有可能的执行次数，失败即代表代码运行时循环的实际执行次数可能超过你设置的4次，当前验证仅覆盖了循环运行次数≤4的路径。

数组边界检查全过是否能证明无内存访问安全问题 #

不能。
当前所有数组边界检查项通过，仅能代表循环执行次数不超过4次的所有路径下，代码不存在数组越界类的内存访问问题。循环执行超过4次的路径完全没有被验证，无法确认这些路径下是否存在内存访问违规。

unwinding assertion失败是否会影响安全性判定结果 #

会直接导致安全性判定结果不可信。
只要存在unwinding assertion失败，CBMC输出的所有“检查通过”结论都只对已展开的有限路径有效，不能作为代码全场景下安全的依据。你可以通过两种方法解决该问题：

• 调高--unwind参数的取值，直到可以覆盖循环最大可能的执行次数，比如你验证的binsearch如果处理的数组最大长度为N，设置--unwind为log₂(N)+1即可覆盖所有执行场景
• 为循环编写符合要求的循环不变式，CBMC可以通过不变式推导证明循环全路径的安全性，不需要对循环进行全量展开

内容的提问来源于stack exchange，提问作者UnevenMango