Почему CBMC раскручивается больше раз?

Question

Давайте рассмотрим код, приведенный ниже, могу ли я знать, почему 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 

Answer 1

Я предполагаю, что symex не был достаточно умен, чтобы видеть, что условие в цикле всегда будет ложным вне определенной итерации. Он пытается немного упростить выражения, но не так сильно. Когда он преобразуется в формулу и передается в решатель SAT, решатель SAT быстро увидит, что условия для этих итераций цикла никогда не будут выполнены, и отбросит эти части формулы, поэтому это не должно влиять на корректность (хотя конечно это может означать, что CBMC требует много времени для запуска).