CBMC教程 (2) - unwind loop
在上一篇文章中,我们介绍了 cbmc 的架构,还有 cbmc 处理程序的步骤。
cbmc 的处理步骤
- 前端处理,获得程序的 cfg
- 展开 unwind cfg,获得路径的公式
- 利用 SAT/SMT 求解公式
这篇文章,将探讨 cbmc 如何处理循环程序。
Iteration-based Unwinding
1 | int main(int argc, char **argv) { |
对于上述的循环,展开其实很简单,假设我们展开五次,就可以得到下面的程序👇:
1 | int main(int argc, char **argv) { |
在很多情况下,cbmc 可以自己决定展开的上限,即使程序中循环可能可能执行的次数并不是一个常量。
1 | _Bool f(); |