0

让我们考虑下面给出的代码，我可以知道为什么 CBMC 在我们假设 io 的初始值大于 2 的情况下展开超过上限。 

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

CBMC 输出：

 CBMC version 5.8 64-bit x86_64 linux
Parsing /tmp/in1_1524461553_1936466587.c
Converting
Type-checking in1_1524461553_1936466587
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Partial Inlining
Generic Property Instrumentation
Starting Bounded Model Checking
Unwinding loop main.0 iteration 1 file /tmp/in1_1524461553_1936466587.c line 9 function main thread 0
Unwinding loop main.0 iteration 2 file /tmp/in1_1524461553_1936466587.c line 9 function main thread 0
Unwinding loop main.0 iteration 3 file /tmp/in1_1524461553_1936466587.c line 9 function main thread 0
Unwinding loop main.0 iteration 4 file /tmp/in1_1524461553_1936466587.c line 9 function main thread 0
Unwinding loop main.0 iteration 5 file /tmp/in1_1524461553_1936466587.c line 9 function main thread 0
Unwinding loop main.0 iteration 6 file /tmp/in1_1524461553_1936466587.c line 9 function main thread 0
Unwinding loop main.0 iteration 7 file /tmp/in1_1524461553_1936466587.c line 9 function main thread 0
Unwinding loop main.0 iteration 8 file /tmp/in1_1524461553_1936466587.c line 9 function main thread 0
Unwinding loop main.0 iteration 9 file /tmp/in1_1524461553_1936466587.c line 9 function main thread 0
Unwinding loop main.0 iteration 10 file /tmp/in1_1524461553_1936466587.c line 9 function main thread 0
Unwinding loop main.0 iteration 11 file /tmp/in1_1524461553_1936466587.c line 9 function main thread 0
Unwinding loop main.0 iteration 12 file /tmp/in1_1524461553_1936466587.c line 9 function main thread 0
Unwinding loop main.0 iteration 13 file /tmp/in1_1524461553_1936466587.c
4

1 回答 1

2

我猜 symex 还不够聪明，无法看到循环上的条件在某个迭代之后总是为假。它会尝试在进行过程中稍微简化表达式，但不是那么简单。当它被转换为公式并传递给 SAT 求解器时，SAT 求解器将很快发现循环的这些迭代的条件永远无法满足并丢弃公式的这些部分，因此它不应该影响正确性（尽管当然这可能意味着 CBMC 需要很长时间才能运行）。

于 2018-08-07T09:16:52.023 回答