Tool ESBMC version 6.0.0 64-bit x86_64 linux CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a CPA-witness2test 1.7-svn 29852 CProver witness2test 0.1 ULTIMATE Automizer 0.1.23-635dfa2a
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon* [apollon004; apollon069; apollon137; apollon154] apollon*
OS Linux 4.15.0-42-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB
Date of execution 2018-12-06 11:03:31 CET 2018-12-08 04:49:09 CET 2018-12-08 07:45:10 CET 2018-12-08 09:00:44 CET 2018-12-12 20:28:15 CET 2018-12-08 05:09:23 CET
Run set esbmc-kind.sv-comp19_prop-memsafety.MemSafety-Other cpa-seq-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-memsafety.MemSafety-Other uautomizer-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-memsafety.MemSafety-Other cpa-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-memsafety.MemSafety-Other fshell-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-memsafety.MemSafety-Other uautomizer-validate-correctness-witnesses-esbmc-kind.sv-comp19_prop-memsafety.MemSafety-Other
Options -s kinduction -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const -witness ../../results-verified/esbmc-kind.2018-12-06_1103.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/esbmc-kind.2018-12-06_1103.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true -witness ../../results-verified/esbmc-kind.2018-12-06_1103.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/esbmc-kind.2018-12-06_1103.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/esbmc-kind.2018-12-06_1103.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
loops/invert_string_false-valid-deref.c false(valid-deref) 1 wit inspect .11  .11  26 .86 1.0  0   false(valid-deref) 1 wit inspect 3.8  2.2  250 0   0   true -32 --- inspect 13     8.0   420   .62 0   false(valid-deref) 1 --- inspect 3.9  2.3  240 0   0      true -32 --- inspect .60   .60   20    .070 0      - --- inspect
loop-acceleration/array3_false-valid-deref.i false(valid-deref) 1 wit inspect 19     18     370 280    1.0  0   timeout 0 wit inspect 97    81    1200 0   0   timeout 0 --- inspect 97     66     6200   1.4  0   timeout 0 --- inspect 92    80    2000 0   0      false(valid-deref) 1 --- inspect .91   .91   25    .078 0      - --- inspect
ntdrivers/floppy_false-valid-deref.i.cil.c timeout 0 --- inspect 900     900     750 12000    .86 0   error (invalid witness file) 0 --- inspect .61 .37 40 0   0   error (2) 0 --- inspect .023 .026 5.6 0    0   error (invalid witness file) 0 --- inspect .93 .60 47 0   0      error (invalid witness file) 0 --- inspect .0017 .0019 .40 0     0      - --- inspect
ntdrivers/kbfiltr_false-valid-deref.i.cil.c false(valid-deref) 0 wit inspect 9.0   9.0   380 110    .85 0   true -32 wit inspect 6.5  3.4  270 0   0   true -32 --- inspect 29     17     660   .62 0   unknown 0 --- inspect 6.6  3.6  270 0   0      error (2) 0 --- inspect .97   .97   21    .62  0      - --- inspect
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .54  .54  42 6.6  1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 15   8.4 370 .66 0  
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .54  .54  42 8.3  1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 16   9.0 370 .66 0  
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .38  .38  31 4.5  1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 10   5.6 330 .62 0  
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .21  .21  31 2.3  .85 0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 9.8 5.8 310 .66 0  
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .20  .20  31 2.3  .85 0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 10   5.6 320 .66 0  
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .31  .31  33 3.8  .85 0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 13   7.7 340 .66 0  
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .31  .31  33 4.0  .85 0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 11   6.4 340 .66 0  
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .12  .12  28 1.3  1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.0 4.9 310 .66 0  
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .16  .16  30 1.9  1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 11   6.1 310 .66 0  
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .15  .15  30 2.0  1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 9.8 5.7 320 .66 0  
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .12  .12  27 1.5  1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.8 5.2 300 .66 0  
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .12  .12  27 1.6  1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 9.1 5.4 300 .66 0  
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .16  .16  27 1.4  1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.4 4.1 300 .62 0  
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .14  .14  27 1.7  .85 0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.9 5.3 300 .66 0  
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .15  .15  27 2.1  1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.4 4.2 300 .62 0  
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .17  .18  27 1.8  1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.8 4.7 310 .66 0  
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .16  .16  27 1.8  1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.7 4.2 300 .66 0  
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .17  .17  27 1.8  .85 0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 9.2 5.4 300 .66 0  
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .097 .097 26 1.0  1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.2 4.8 300 .66 0  
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .098 .098 26 1.2  .85 0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.9 5.2 300 .66 0  
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .11  .11  26 1.3  1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.9 5.2 300 .66 0  
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .12  .12  26 1.2  1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.9 5.2 300 .66 0  
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .13  .14  26 1.3  1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.5 5.0 300 .66 0  
memsafety-ext3/derefAfterFree1_false-valid-deref.c false(valid-deref) 1 wit inspect .084 .085 26 1.0  1.0  0   false(valid-deref) 1 wit inspect 3.6  2.1  240 0   0   true -32 --- inspect 8.3   5.1   310   .62 0   false(valid-deref) 1 --- inspect 3.6  2.1  250 0   0      false(valid-deref) 1 --- inspect .59   .59   20    .049 0      - --- inspect
memsafety-ext3/derefAfterFree2_false-valid-deref.c false(valid-deref) 1 wit inspect .15  .15  26 1.8  1.0  0   false(valid-deref) 1 wit inspect 3.9  2.2  250 0   0   true -32 --- inspect 12     6.7   350   .62 0   false(valid-deref) 1 --- inspect 3.8  2.2  250 0   0      false(valid-deref) 1 --- inspect .59   .59   20    .049 0      - --- inspect
memsafety-ext3/derefInLoop1_false-valid-deref.c true -32 wit inspect .084 .084 26 .83 .85 0   error (1) 0 --- inspect .82 .50 44 0   0   false(valid-deref) 1 --- inspect 8.3   5.1   310   .62 0   unknown 0 --- inspect 1.1  .69 49 0   0      error (1) 0 --- inspect .076  .077  11    0     .0041 - --- inspect
memsafety-ext3/getNumbers1_false-valid-deref.c true -32 wit inspect .19  .19  26 2.1  1.0  0   error (1) 0 --- inspect .77 .48 43 0   0   false(valid-deref) 1 --- inspect 14     8.3   500   .62 0   unknown 0 --- inspect 1.0  .68 50 0   0      error (1) 0 --- inspect .071  .071  11    0     0      - --- inspect
memsafety-ext3/getNumbers2_false-valid-deref.c true -32 wit inspect .091 .091 26 .82 .85 0   error (1) 0 --- inspect .88 .52 44 0   0   false(valid-deref) 1 --- inspect 28     17     610   .62 0   unknown 0 --- inspect .99 .64 48 0   0      error (1) 0 --- inspect .078  .079  11    0     0      - --- inspect
memsafety-ext3/getNumbers4_false-valid-deref.c true -32 wit inspect .21  .21  27 2.4  1.0  0   error (1) 0 --- inspect .80 .49 44 0   0   false(valid-deref) 1 --- inspect 79     59     740   .62 0   unknown 0 --- inspect .99 .64 50 0   0      error (1) 0 --- inspect .075  .075  11    0     0      - --- inspect
memsafety-ext3/naturalNumbers1_false-valid-deref.c false(valid-deref) 1 wit inspect .095 .096 26 1.1  1.0  0   false(valid-deref) 1 wit inspect 4.8  2.7  250 0   0   true -32 --- inspect 11     6.3   340   .62 0   false(valid-deref) 1 --- inspect 3.9  2.3  250 0   .0041 false(valid-deref) 1 --- inspect .59   .59   20    .057 0      - --- inspect
memsafety-ext3/realloc1_false-valid-deref.c false(valid-memtrack) -16 wit inspect .20  .20  26 2.4  1.0  0   true -32 wit inspect 4.0  2.2  250 0   0   true -32 --- inspect 7.1   4.4   310   .66 0   error 0 --- inspect 3.9  2.2  250 0   0      false(valid-deref) 1 --- inspect .63   .63   20    .061 0      - --- inspect
memsafety-ext3/scopes1_false-valid-deref.c true -32 wit inspect .082 .083 26 .84 1.0  0   error (1) 0 --- inspect .88 .53 43 0   0   false(valid-deref) 1 --- inspect 7.0   4.0   310   .62 0   unknown 0 --- inspect 1.0  .67 50 0   0      error (1) 0 --- inspect .071  .072  11    0     0      - --- inspect
memsafety-ext3/scopes2_false-valid-deref.c false(valid-deref) 1 wit inspect .11  .11  26 .96 1.0  0   false(valid-deref) 1 wit inspect 4.4  2.4  250 0   0   true -32 --- inspect 9.2   5.7   310   .66 0   unknown 0 --- inspect 3.9  2.3  250 0   0      false(valid-deref) 1 --- inspect .63   .65   20    .061 0      - --- inspect
memsafety-ext3/scopes3_false-valid-deref.c true -32 wit inspect .11  .11  26 .90 .85 0   error (1) 0 --- inspect .68 .41 43 0   0   false(valid-deref) 1 --- inspect 15     9.0   480   .62 0   unknown 0 --- inspect .96 .61 49 0   0      error (1) 0 --- inspect .072  .071  11    0     0      - --- inspect
memsafety-ext3/scopes4_false-valid-deref.c true -32 wit inspect .078 .079 26 .97 1.0  0   error (1) 0 --- inspect .72 .44 44 0   0   false(valid-deref) 1 --- inspect 8.5   5.1   320   .62 0   unknown 0 --- inspect .98 .63 50 0   0      error (1) 0 --- inspect .074  .073  12    0     0      - --- inspect
memsafety-ext3/scopes5_false-valid-deref.c true -32 wit inspect .081 .083 26 .86 .85 0   error (1) 0 --- inspect .70 .43 44 0   0   false(valid-deref) 1 --- inspect 6.8   3.9   310   .62 0   unknown 0 --- inspect 1.0  .65 50 0   0      error (1) 0 --- inspect .080  .080  11    0     .0041 - --- inspect
memsafety-ext3/freeAlloca_false-valid-free.c false(valid-free) 1 wit inspect .15  .15  26 2.1  1.0  0   false(valid-free) 1 wit inspect 5.1  2.8  250 0   0   true -32 --- inspect 11     6.4   330   .62 0   unknown 0 --- inspect 5.1  3.1  250 0   0      error (2) 0 --- inspect .60   .60   20    .066 0      - --- inspect
memsafety-ext3/getNumbers1_true-valid-memsafety.c true 2 wit inspect .12  .12  26 1.0  1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 14   8.2 470 .66 0  
memsafety-ext3/getNumbers3_true-valid-memsafety.c true 2 wit inspect .085 .085 26 .88 .85 0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 12   7.4 370 .66 0  
memsafety-ext3/getNumbers4_true-valid-memsafety.c true 2 wit inspect .20  .20  27 2.5  1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 79   48   960 .62 0  
memsafety-ext3/scopes4_true-valid-memsafety.c true 2 wit inspect .087 .088 26 .82 1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 13   7.1 350 .66 0  
pthread-memsafety/fillarray1_false-valid-deref.i false(valid-deref) 1 wit inspect .15  .15  27 1.8  1.0  0   error 0 wit inspect 4.9  2.7  250 0   0   error (7) 0 --- inspect 18     10     330   .68 0   error 0 --- inspect 4.6  2.5  260 0   0      false(valid-deref) 1 --- inspect .71   .70   20    .098 .41   - --- inspect
pthread-memsafety/fillarray_false-valid-deref.i false(valid-deref) 1 wit inspect .14  .14  27 1.7  1.0  0   error 0 wit inspect 5.6  3.0  250 0   0   error (7) 0 --- inspect 17     10     330   .68 0   error 0 --- inspect 4.4  2.5  250 0   0      false(valid-deref) 1 --- inspect .71   .69   20    .098 .19   - --- inspect
pthread-memsafety/list1_false-valid-deref.i unknown 0 --- inspect .13  .14  27 1.2  .85 0   error (invalid witness file) 0 --- inspect .63 .39 41 0   0   error (2) 0 --- inspect .023 .024 5.6 0    0   error (invalid witness file) 0 --- inspect .95 .61 48 0   0      error (invalid witness file) 0 --- inspect .0050 .0063 .52 0     0      - --- inspect
sv-benchmarks/c/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
total 48 -209 940    940    2700 12000   46    0   21 -58 150 110   4100 0   0   21 -248 400 260 13000 13   0   21 4 150 110   5000 0   .0041 21 -24 8.1  8.1  320 1.3   .60 27 54 340 200 9400 18 0  
    correct results 36 63 25    24    1400 350   35    0   6 6 26 14   1500 0   0   8 8 170 110 3600 5.0 0   4 4 15 9.0 990 0   .0041 8 8 5.4  5.4  170 .55  .59 27 54 340 200 9400 18 0  
        correct true 27 54 5.2  5.2  780 62   26    0   0 0 0 0 27 54 340 200 9400 18 0  
        correct false 9 9 20    19    580 290   9.1  0   6 6 26 14   1500 0   0   8 8 170 110 3600 5.0 0   4 4 15 9.0 990 0   .0041 8 8 5.4  5.4  170 .55  .59 0
    correct-unconfimed results 1 0 9.0  9.0  380 110   .85 0   0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0
        correct-unconfirmed false 1 0 9.0  9.0  380 110   .85 0   0 0 0 0 0
    incorrect results 9 -272 1.1  1.1  230 12   8.4  0   2 -64 10 5.6 520 0   0   8 -256 100 60 3000 5.0 0   0 1 -32 .60 .60 20 .070 0    0
        incorrect true 8 -256 .92 .92 210 9.7 7.4  0   2 -64 10 5.6 520 0   0   8 -256 100 60 3000 5.0 0   0 1 -32 .60 .60 20 .070 0    0
        incorrect false 1 -16 .20 .20 26 2.4 1.0  0   0 0 0 0 0
score (48 tasks, max score: 75) -209 -58 -248 4 -24 54
Run set esbmc-kind.sv-comp19_prop-memsafety.MemSafety-Other cpa-seq-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-memsafety.MemSafety-Other uautomizer-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-memsafety.MemSafety-Other cpa-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-memsafety.MemSafety-Other fshell-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-memsafety.MemSafety-Other uautomizer-validate-correctness-witnesses-esbmc-kind.sv-comp19_prop-memsafety.MemSafety-Other