cbmc-out.txt

$ /tmp/cbmc -D FAIL mycmp.c  --trace 
CBMC version 5.6 64-bit x86_64 linux
Parsing mycmp.c
Converting
Type-checking mycmp
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 mycmp.0 iteration 1 file mycmp.c line 11 function mycmp thread 0
Unwinding loop mycmp.0 iteration 2 file mycmp.c line 11 function mycmp thread 0
Unwinding loop mycmp.0 iteration 3 file mycmp.c line 11 function mycmp thread 0
Unwinding loop mycmp.0 iteration 4 file mycmp.c line 11 function mycmp thread 0
Unwinding loop mycmp.0 iteration 5 file mycmp.c line 11 function mycmp thread 0
Unwinding loop main.0 iteration 1 file mycmp.c line 24 function main thread 0
Unwinding loop main.0 iteration 2 file mycmp.c line 24 function main thread 0
Unwinding loop main.0 iteration 3 file mycmp.c line 24 function main thread 0
Unwinding loop main.0 iteration 4 file mycmp.c line 24 function main thread 0
Unwinding loop main.0 iteration 5 file mycmp.c line 24 function main thread 0
size of program expression: 262 steps
simple slicing removed 0 assignments
Generated 1 VCC(s), 0 remaining after simplification
VERIFICATION SUCCESSFUL
jepler@babs:~$ /tmp/cbmc -D FAIL mycmp.c  --trace 
CBMC version 5.6 64-bit x86_64 linux
Parsing mycmp.c
Converting
Type-checking mycmp
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 mycmp.0 iteration 1 file mycmp.c line 11 function mycmp thread 0
Unwinding loop mycmp.0 iteration 2 file mycmp.c line 11 function mycmp thread 0
Unwinding loop mycmp.0 iteration 3 file mycmp.c line 11 function mycmp thread 0
Unwinding loop mycmp.0 iteration 4 file mycmp.c line 11 function mycmp thread 0
Unwinding loop mycmp.0 iteration 5 file mycmp.c line 11 function mycmp thread 0
Unwinding loop main.0 iteration 1 file mycmp.c line 24 function main thread 0
Unwinding loop main.0 iteration 2 file mycmp.c line 24 function main thread 0
Unwinding loop main.0 iteration 3 file mycmp.c line 24 function main thread 0
Unwinding loop main.0 iteration 4 file mycmp.c line 24 function main thread 0
Unwinding loop main.0 iteration 5 file mycmp.c line 24 function main thread 0
size of program expression: 263 steps
simple slicing removed 0 assignments
Generated 1 VCC(s), 0 remaining after simplification
VERIFICATION SUCCESSFUL
jepler@babs:~$ /tmp/cbmc mycmp.c  --trace --nondet-static
CBMC version 5.6 64-bit x86_64 linux
Parsing mycmp.c
Converting
Type-checking mycmp
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Partial Inlining
Generic Property Instrumentation
Adding nondeterministic initialization of static/global variables
Starting Bounded Model Checking
Unwinding loop mycmp.0 iteration 1 file mycmp.c line 11 function mycmp thread 0
Unwinding loop mycmp.0 iteration 2 file mycmp.c line 11 function mycmp thread 0
Unwinding loop mycmp.0 iteration 3 file mycmp.c line 11 function mycmp thread 0
Unwinding loop mycmp.0 iteration 4 file mycmp.c line 11 function mycmp thread 0
Unwinding loop mycmp.0 iteration 5 file mycmp.c line 11 function mycmp thread 0
Unwinding loop main.0 iteration 1 file mycmp.c line 24 function main thread 0
Unwinding loop main.0 iteration 2 file mycmp.c line 24 function main thread 0
Unwinding loop main.0 iteration 3 file mycmp.c line 24 function main thread 0
Unwinding loop main.0 iteration 4 file mycmp.c line 24 function main thread 0
Unwinding loop main.0 iteration 5 file mycmp.c line 24 function main thread 0
size of program expression: 400 steps
simple slicing removed 5 assignments
Generated 4 VCC(s), 4 remaining after simplification
Passing problem to propositional reduction
converting SSA
Running propositional reduction
Post-processing
Solving with MiniSAT 2.2.1 with simplifier
11187 variables, 18674 clauses
SAT checker: instance is SATISFIABLE
Solving with MiniSAT 2.2.1 with simplifier
11187 variables, 3328 clauses
SAT checker: instance is SATISFIABLE
Solving with MiniSAT 2.2.1 with simplifier
11187 variables, 3328 clauses
SAT checker: instance is UNSATISFIABLE
Runtime decision procedure: 0.033s

** Results:
[main.assertion.1] res2 == 0: SUCCESS
[main.assertion.2] res2 != 0: SUCCESS
[main.assertion.3] res2 < 0: FAILURE
[main.assertion.4] res2 > 0: FAILURE

Trace for main.assertion.3:

State 22 file mycmp.c line 23 function main thread 0
----------------------------------------------------
  res1=0l (0000000000000000000000000000000000000000000000000000000000000000)

State 26 file mycmp.c line 23 function main thread 0
----------------------------------------------------
  cmp1=buf1 (0000001000000000000000000000000000000000000000000000000000000000)

State 27 file mycmp.c line 23 function main thread 0
----------------------------------------------------
  cmp2=buf2 (0000001100000000000000000000000000000000000000000000000000000000)

State 28 file mycmp.c line 23 function main thread 0
----------------------------------------------------
  length=5u (00000000000000000000000000000101)

State 30 file mycmp.c line 6 function mycmp thread 0
----------------------------------------------------
  difference=0 (00000000000000000000000000000000)

State 31 file mycmp.c line 6 function mycmp thread 0
----------------------------------------------------
  difference=-57197 (11111111111111110010000010010011)

State 37 file mycmp.c line 23 function main thread 0
----------------------------------------------------
  res1=-57197l (1111111111111111111111111111111111111111111111110010000010010011)

State 38 file mycmp.c line 24 function main thread 0
----------------------------------------------------
  res2=0l (0000000000000000000000000000000000000000000000000000000000000000)

State 66 file mycmp.c line 24 function main thread 0
----------------------------------------------------
  res2=147l (0000000000000000000000000000000000000000000000000000000010010011)

Violated property:
  file mycmp.c line 29 function main
  res2 < 0
  res2 < (signed long int)0


Trace for main.assertion.4:

State 22 file mycmp.c line 23 function main thread 0
----------------------------------------------------
  res1=0l (0000000000000000000000000000000000000000000000000000000000000000)

State 26 file mycmp.c line 23 function main thread 0
----------------------------------------------------
  cmp1=buf1 (0000001000000000000000000000000000000000000000000000000000000000)

State 27 file mycmp.c line 23 function main thread 0
----------------------------------------------------
  cmp2=buf2 (0000001100000000000000000000000000000000000000000000000000000000)

State 28 file mycmp.c line 23 function main thread 0
----------------------------------------------------
  length=5u (00000000000000000000000000000101)

State 30 file mycmp.c line 6 function mycmp thread 0
----------------------------------------------------
  difference=0 (00000000000000000000000000000000)

State 31 file mycmp.c line 6 function mycmp thread 0
----------------------------------------------------
  difference=1 (00000000000000000000000000000001)

State 37 file mycmp.c line 23 function main thread 0
----------------------------------------------------
  res1=1l (0000000000000000000000000000000000000000000000000000000000000001)

State 38 file mycmp.c line 24 function main thread 0
----------------------------------------------------
  res2=0l (0000000000000000000000000000000000000000000000000000000000000000)

State 66 file mycmp.c line 24 function main thread 0
----------------------------------------------------
  res2=-255l (1111111111111111111111111111111111111111111111111111111100000001)

Violated property:
  file mycmp.c line 30 function main
  res2 > 0
  res2 > (signed long int)0


** 2 of 4 failed (3 iterations)
VERIFICATION FAILED

mycmp.c

#include <string.h>
#include <inttypes.h>

int32_t mycmp(const unsigned char *cmp1, const unsigned char *cmp2, uint32_t length) {
    if(length >= 4) {
        int32_t difference = *(uint32_t *)cmp1 - *(uint32_t *)cmp2;
        if(difference)
            return difference;
    }
    
    return memcmp(cmp1,cmp2,length);
}

#define assume(x) __CPROVER_assume((x))
#define assert(x) __CPROVER_assert((x), #x)
extern char nondet_u8();

#define N 5
char buf1[N], buf2[N];

int main() {

    long res1 = mycmp(buf1, buf2, N);
    long res2 = memcmp(buf1, buf2, N);

    if(res1 == 0) assert(res2 == 0);
    if(res1 != 0) assert(res2 != 0);

    if(res1 < 0) assert(res2 < 0);
    if(res1 > 0) assert(res2 > 0);

    return 0;
}