Skip to content

Instantly share code, notes, and snippets.

@jepler

jepler/cbmc-out.txt

Created March 23, 2017 00:41
Show Gist options
  • Save jepler/d78e5afce991bd3020ae5600efce1642 to your computer and use it in GitHub Desktop.
Save jepler/d78e5afce991bd3020ae5600efce1642 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
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
Raw
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;
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment