CBMC simple loop

counterexample.txt

CBMC version 5.4 64-bit x86_64 macos
Parsing simple.c
Converting
Type-checking simple
Generating GOTO Program
Adding CPROVER library (x86_64)
Function Pointer Removal
Partial Inlining
Generic Property Instrumentation
Starting Bounded Model Checking
Unwinding loop loop.0 iteration 1 file simple.c line 14 function loop thread 0
Unwinding loop loop.1 iteration 1 file simple.c line 22 function loop thread 0
size of program expression: 67 steps
simple slicing removed 5 assignments
Generated 2 VCC(s), 2 remaining after simplification
Passing problem to propositional reduction
converting SSA
Running propositional reduction
Post-processing
Solving with MiniSAT 2.2.1 with simplifier
434 variables, 264 clauses
SAT checker: instance is SATISFIABLE
Runtime decision procedure: 0.002s
Building error trace

Counterexample:

State 18 file simple.c line 11 thread 0
----------------------------------------------------
  A=((unsigned int *)NULL) (0000000000000000000000000000000000000000000000000000000000000000)

State 19 file simple.c line 11 thread 0
----------------------------------------------------
  len=0 (00000000000000000000000000000000)

State 20 file simple.c line 12 function loop thread 0
----------------------------------------------------
  halt_state=FALSE (00000000)

State 21 file simple.c line 12 function loop thread 0
----------------------------------------------------
  halt_state=FALSE (00000000)

State 22 file simple.c line 14 function loop thread 0
----------------------------------------------------
  i=0 (00000000000000000000000000000000)

State 23 file simple.c line 14 function loop thread 0
----------------------------------------------------
  i=0 (00000000000000000000000000000000)

State 25 file simple.c line 15 function loop thread 0
----------------------------------------------------
  x=0 (00000000000000000000000000000000)

State 26 file simple.c line 15 function loop thread 0
----------------------------------------------------
  x=3080388219 (10110111100110101111111001111011)

State 28 file simple.c line 14 function loop thread 0
----------------------------------------------------
  i=1 (00000000000000000000000000000001)

State 31 file simple.c line 22 function loop thread 0
----------------------------------------------------
  i=0 (00000000000000000000000000000000)

State 32 file simple.c line 22 function loop thread 0
----------------------------------------------------
  i=0 (00000000000000000000000000000000)

State 34 file simple.c line 23 function loop thread 0
----------------------------------------------------
  y=0 (00000000000000000000000000000000)

State 35 file simple.c line 23 function loop thread 0
----------------------------------------------------
  y=3735928559 (11011110101011011011111011101111)

Violated property:
  file simple.c line 25 function loop
  assertion
  (signed int)halt_state == 1

VERIFICATION FAILED

simple.c

// cbmc simple.c --function loop

#include <stdbool.h>

#ifdef DYNAMIC_LOOP_BOUND
#define LEN len //< dynamic
#else
#define LEN 1   //< static
#endif

void loop(const unsigned A[], unsigned len) {
  bool halt_state = false;

  for (unsigned i=0; i<LEN; i++) {
    unsigned x = A[i];
    if (x >= 0xdeadbeef) {
      halt_state = true;
    }
  }

  // check: \exists i in [0,len) :: A[i] >= 0xdeadbeef ==> halt_state
  for (unsigned i=0; i<LEN; i++) {
    unsigned y = A[i];
    if (y >= 0xdeadbeef) {
      __CPROVER_assert(halt_state == true, "");
      return;
    }
  }
  __CPROVER_assert(halt_state == false, "");
}