为何CBMC循环展开次数超出上限？附代码及假设求解析

一、为什么CBMC会进行更多次数的循环展开？ #

CBMC作为符号执行工具，核心目标是覆盖所有可能的执行路径，这也是它会“超额”展开循环的核心原因，具体来说有这几点：

• 符号变量的不确定性：如果循环的终止条件依赖符号化的变量（比如你的代码里i0是未初始化的符号变量，仅通过约束限定范围），CBMC没办法提前计算出循环的精确执行次数——因为符号变量可以取符合约束的任意值，对应循环执行的次数也各不相同。
• 路径覆盖的需求：为了确保没有遗漏任何可能的执行路径，CBMC会尝试展开循环直到覆盖所有潜在的终止场景。默认情况下它有一个循环展开上限（比如10次，可通过--unwind N参数修改），但当它检测到循环在达到上限后仍可能继续执行时，会尝试进一步展开，或者触发“unwinding assertion”来提示可能存在未覆盖的路径。
• 避免假阴性结果：如果CBMC过早停止循环展开，可能会漏掉某些会导致断言失败的路径，所以它会尽可能多展开来保证验证的准确性。

二、给定代码中，已假设i0≥2为何循环展开仍超出上限？ #

先看你的代码片段：

#include<assert.h>
void main() {
 int i0;
 int o1;
 __CPROVER_assume(i0>=2);
 while(i0<=10) {
  i0=i0+1;
 }
 o1=i0+1;
 assert((o1 <= 1));
}

问题出在**i0的取值范围没有被完全限定**：

• 你只通过__CPROVER_assume(i0>=2)设定了下限，但没有限制i0的上限——也就是说i0可以是2到10之间的整数，也可以是11、12……甚至更大的数。
• 当i0>10时，循环直接不执行；当i0在2到10之间时，循环会执行11 - i0次（比如i0=2时执行9次，i0=10时执行1次）。
• CBMC需要覆盖所有这些可能的路径，所以它会展开循环足够多次来覆盖i0从2到10的所有情况。如果你的默认展开上限（比如10次）刚好能覆盖最多的执行次数（9次），但CBMC为了确保没有遗漏，可能会尝试多展开一次来验证循环是否确实会终止——这就会让你觉得展开次数超出了预期。
• 另外，你的最终断言assert(o1 <=1)必然会失败：循环结束后i0要么是>10（循环未执行或执行后退出），所以o1=i0+1至少是12，远大于1。CBMC在验证这个断言时，会遍历所有路径，这也会驱动它充分展开循环来找到这个失败的路径。

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