Tool DepthK 3.1 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* [apollon001; apollon005; apollon039; apollon053; apollon087; apollon091] [apollon007; apollon009; apollon073; apollon078] 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-05 09:36:33 CET 2018-12-06 10:02:56 CET 2018-12-06 11:08:44 CET 2018-12-06 11:42:46 CET 2018-12-12 19:35:41 CET 2018-12-06 10:24:56 CET
Run set depthk.sv-comp19_prop-memsafety.MemSafety-Other cpa-seq-validate-violation-witnesses-depthk.sv-comp19_prop-memsafety.MemSafety-Other uautomizer-validate-violation-witnesses-depthk.sv-comp19_prop-memsafety.MemSafety-Other cpa-witness2test-validate-violation-witnesses-depthk.sv-comp19_prop-memsafety.MemSafety-Other fshell-witness2test-validate-violation-witnesses-depthk.sv-comp19_prop-memsafety.MemSafety-Other uautomizer-validate-correctness-witnesses-depthk.sv-comp19_prop-memsafety.MemSafety-Other
Options -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/depthk.2018-12-05_0936.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/depthk.2018-12-05_0936.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/depthk.2018-12-05_0936.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/depthk.2018-12-05_0936.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/depthk.2018-12-05_0936.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 unknown 0 wit inspect .15 .15 33 1.6 .85 0      false(valid-deref) 1 wit inspect 4.1  2.4  240 0   0   true -32 --- inspect 12     7.2   420   .66 0   false(valid-deref) 1 --- inspect 3.7  2.2  240 0   .13 true -32 --- inspect .63   .62   20    .070 0    - --- inspect
loop-acceleration/array3_false-valid-deref.i unknown 0 --- inspect 120    120    49 1800   3000    .033  error (invalid witness file) 0 --- inspect .79 .48 41 0   0   error (2) 0 --- inspect .022 .023 5.6 0    0   error (invalid witness file) 0 --- inspect .96 .62 48 0   0    error (invalid witness file) 0 --- inspect .0041 .0047 .40 0     0    - --- inspect
ntdrivers/floppy_false-valid-deref.i.cil.c false(valid-deref) 0 wit inspect 5.7  5.7  390 74   1.0  0      true -32 wit inspect 11    6.3  540 0   0   true -32 --- inspect 80     58     1100   .62 0   unknown 0 --- inspect 11    6.1  530 0   0    timeout 0 --- inspect 96      96      21    .28  0    - --- inspect
ntdrivers/kbfiltr_false-valid-deref.i.cil.c false(valid-memtrack) -16 wit inspect 24    24    380 330   .85 0      true -32 wit inspect 6.8  3.6  270 0   0   true -32 --- inspect 24     14     510   .62 0   unknown 0 --- inspect 5.5  3.0  270 0   0    error (1) 0 --- inspect .78   .78   21    .13  0    - --- inspect
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c unknown 0 wit inspect 1.8  1.6  66 21   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 12   6.8 390 .62 0  
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c unknown 0 wit inspect 1.8  1.6  67 21   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 13   7.3 390 .66 0  
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c unknown 0 wit inspect 1.1  .86 67 13   26    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 9.5 5.3 310 .62 0  
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c unknown 0 wit inspect 1.1  .88 65 14   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 11   5.8 320 .66 0  
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c unknown 0 wit inspect 1.2  .87 66 14   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 9.7 5.4 320 .66 0  
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c unknown 0 wit inspect 1.3  1.1  65 17   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 11   7.0 340 .62 0  
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c unknown 0 wit inspect 1.4  1.1  66 16   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 12   7.2 350 .66 0  
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c unknown 0 wit inspect .88 .63 66 8.9 31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.2 4.7 310 .66 0  
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c unknown 0 wit inspect 1.0  .74 67 12   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 9.2 5.2 310 .66 0  
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c unknown 0 wit inspect 1.0  .73 66 12   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 9.8 5.5 320 .62 0  
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c unknown 0 wit inspect .96 .71 65 10   26    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.2 4.0 300 .62 0  
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c unknown 0 wit inspect 1.0  .74 67 10   26    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.1 4.1 300 .66 0  
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c unknown 0 wit inspect 1.1  .80 66 12   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.7 4.3 300 .62 0  
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c unknown 0 wit inspect 1.1  .82 67 10   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.5 4.2 310 .66 0  
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c unknown 0 wit inspect 1.2  .91 71 13   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.4 4.6 310 .66 0  
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c unknown 0 wit inspect 1.1  .89 67 13   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.7 4.3 320 .66 0  
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c unknown 0 wit inspect 1.2  .94 78 12   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.6 4.7 300 .66 0  
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c unknown 0 wit inspect 1.2  .90 73 15   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.4 4.5 310 .66 0  
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c unknown 0 wit inspect .88 .62 65 10   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.1 4.4 310 .66 0  
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c unknown 0 wit inspect .89 .63 66 11   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.4 4.1 300 .66 0  
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c unknown 0 wit inspect .87 .62 66 11   26    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.3 4.2 300 .66 0  
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c unknown 0 wit inspect .93 .67 65 9.7 31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.3 4.2 300 .62 0  
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c unknown 0 wit inspect .95 .69 65 10   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.1 4.5 300 .66 0  
memsafety-ext3/derefAfterFree1_false-valid-deref.c false(valid-deref) 1 wit inspect .15 .15 33 1.6 .85 0      false(valid-deref) 1 wit inspect 3.5  1.9  250 0   0   true -32 --- inspect 7.6   4.3   300   .62 0   false(valid-deref) 1 --- inspect 3.5  2.1  240 0   0    false(valid-deref) 1 --- inspect .60   .60   20    .049 0    - --- inspect
memsafety-ext3/derefAfterFree2_false-valid-deref.c false(valid-deref) 1 wit inspect 1.6  1.6  36 19   180    .0041 false(valid-deref) 1 wit inspect 3.7  2.1  250 0   0   true -32 --- inspect 12     6.9   360   .62 0   false(valid-deref) 1 --- inspect 3.8  2.2  240 0   0    false(valid-deref) 1 --- inspect .60   .60   20    .049 0    - --- inspect
memsafety-ext3/derefInLoop1_false-valid-deref.c unknown 0 wit inspect .79 .53 66 8.5 31    0      error (1) 0 --- inspect .86 .51 44 0   0   false(valid-deref) 1 --- inspect 8.0   4.6   310   .66 0   unknown 0 --- inspect 1.0  .64 49 0   0    error (1) 0 --- inspect .075  .076  11    0     0    - --- inspect
memsafety-ext3/getNumbers1_false-valid-deref.c unknown 0 wit inspect 3.3  3.0  68 41   300    .0041 error (1) 0 --- inspect .79 .50 43 0   0   false(valid-deref) 1 --- inspect 15     8.5   490   .62 0   unknown 0 --- inspect 1.2  .80 50 0   0    error (1) 0 --- inspect .098  .096  11    0     0    - --- inspect
memsafety-ext3/getNumbers2_false-valid-deref.c unknown 0 wit inspect .79 .54 67 8.2 31    0      error (1) 0 --- inspect .81 .49 44 0   0   false(valid-deref) 1 --- inspect 26     17     610   .66 0   unknown 0 --- inspect .99 .65 50 0   0    error (1) 0 --- inspect .066  .066  11    0     0    - --- inspect
memsafety-ext3/getNumbers4_false-valid-deref.c unknown 0 wit inspect 3.9  3.6  67 56   300    .0041 error (1) 0 --- inspect .72 .45 44 0   0   false(valid-deref) 1 --- inspect 78     57     880   .62 0   unknown 0 --- inspect 1.1  .68 50 0   0    error (1) 0 --- inspect .10   .097  11    0     0    - --- inspect
memsafety-ext3/naturalNumbers1_false-valid-deref.c false(valid-deref) 1 wit inspect .57 .56 35 8.0 62    0      false(valid-deref) 1 wit inspect 3.8  2.2  250 0   0   true -32 --- inspect 10     5.9   340   .66 0   false(valid-deref) 1 --- inspect 3.9  2.3  250 0   0    false(valid-deref) 1 --- inspect .59   .59   20    .057 0    - --- inspect
memsafety-ext3/realloc1_false-valid-deref.c false(valid-memtrack) -16 wit inspect 2.6  2.6  36 31   260    .0082 true -32 wit inspect 3.7  2.1  250 0   0   true -32 --- inspect 7.1   4.1   310   .66 0   error 0 --- inspect 3.8  2.1  240 0   0    false(valid-deref) 1 --- inspect .62   .64   20    .061 0    - --- inspect
memsafety-ext3/scopes1_false-valid-deref.c unknown 0 wit inspect .82 .57 67 8.5 31    0      error (1) 0 --- inspect .70 .42 43 0   0   false(valid-deref) 1 --- inspect 6.9   4.0   310   .62 0   unknown 0 --- inspect 1.0  .66 49 0   0    error (1) 0 --- inspect .073  .073  11    0     0    - --- inspect
memsafety-ext3/scopes2_false-valid-deref.c false(valid-deref) 1 wit inspect .15 .14 34 1.5 1.0  0      false(valid-deref) 1 wit inspect 3.6  2.0  250 0   0   true -32 --- inspect 9.1   5.6   320   .66 0   unknown 0 --- inspect 3.7  2.3  240 0   0    false(valid-deref) 1 --- inspect .61   .61   20    .061 0    - --- inspect
memsafety-ext3/scopes3_false-valid-deref.c unknown 0 wit inspect .79 .52 65 8.2 31    0      error (1) 0 --- inspect .70 .42 45 0   0   false(valid-deref) 1 --- inspect 14     7.9   480   .62 0   unknown 0 --- inspect 1.0  .66 50 0   0    error (1) 0 --- inspect .066  .066  11    0     0    - --- inspect
memsafety-ext3/scopes4_false-valid-deref.c unknown 0 wit inspect .83 .56 67 8.4 31    0      error (1) 0 --- inspect .67 .42 45 0   0   false(valid-deref) 1 --- inspect 7.8   4.4   300   .62 0   unknown 0 --- inspect 1.0  .65 50 0   0    error (1) 0 --- inspect .096  .096  11    0     0    - --- inspect
memsafety-ext3/scopes5_false-valid-deref.c unknown 0 wit inspect .81 .55 67 8.6 31    0      error (1) 0 --- inspect .78 .49 45 0   0   false(valid-deref) 1 --- inspect 6.9   4.4   300   .66 0   unknown 0 --- inspect 1.0  .66 50 0   0    error (1) 0 --- inspect .079  .079  11    0     0    - --- inspect
memsafety-ext3/freeAlloca_false-valid-free.c unknown 0 wit inspect 3.1  2.8  68 37   300    .0041 error (1) 0 --- inspect .86 .52 44 0   0   true -32 --- inspect 15     11     400   .62 0   unknown 0 --- inspect 1.0  .64 49 0   0    error (1) 0 --- inspect .077  .077  11    0     0    - --- inspect
memsafety-ext3/getNumbers1_true-valid-memsafety.c unknown 0 wit inspect 2.7  2.4  68 37   300    .0082 - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 13   7.4 490 .62 0  
memsafety-ext3/getNumbers3_true-valid-memsafety.c unknown 0 wit inspect .80 .54 65 8.6 26    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 11   6.3 380 .62 0  
memsafety-ext3/getNumbers4_true-valid-memsafety.c unknown 0 wit inspect 4.0  3.7  68 57   300    .0041 - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 65   41   1000 .62 0  
memsafety-ext3/scopes4_true-valid-memsafety.c unknown 0 wit inspect .80 .53 66 9.1 31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 12   6.7 350 .62 0  
pthread-memsafety/fillarray1_false-valid-deref.i false(valid-deref) 1 wit inspect .21 .21 35 2.5 1.0  0      error 0 wit inspect 4.8  2.6  250 0   0   error (7) 0 --- inspect 17     10     330   .75 0   error 0 --- inspect 4.6  2.6  260 0   0    false(valid-deref) 1 --- inspect .72   .71   20    .098 .29 - --- inspect
pthread-memsafety/fillarray_false-valid-deref.i false(valid-deref) 1 wit inspect .21 .20 35 2.6 1.0  0      error 0 wit inspect 4.9  2.6  260 0   0   error (7) 0 --- inspect 18     10     330   .68 0   error 0 --- inspect 4.9  2.7  280 0   0    false(valid-deref) 1 --- inspect .71   .71   20    .098 .29 - --- inspect
pthread-memsafety/list1_false-valid-deref.i unknown 0 --- inspect 900    900    5500 9600   780    0      error (invalid witness file) 0 --- inspect .62 .39 42 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect 1.2  .80 48 0   0    error (invalid witness file) 0 --- inspect .0044 .0054 .40 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 -26 1100   1100   9000 12000 6800   .070  21 -91 58 33 3300 0   0   21 -280 380 250 8400 12   0   21 4 60 35   3300 0   .13 21 -25 100    100    300 .95  .58 27 54 300 180 9600 17 0  
    correct results 6 6 2.9 2.8 210 35 250   .0041 5 5 19 11 1200 0   0   8 8 160 110 3700 5.1 0   4 4 15 8.8 980 0   .13 7 7 4.5  4.5  140 .48  .58 27 54 300 180 9600 17 0  
        correct true 0 0 0 0 0 27 54 300 180 9600 17 0  
        correct false 6 6 2.9 2.8 210 35 250   .0041 5 5 19 11 1200 0   0   8 8 160 110 3700 5.1 0   4 4 15 8.8 980 0   .13 7 7 4.5  4.5  140 .48  .58 0
    correct-unconfimed results 1 0 5.7 5.7 390 74 1.0 0      0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0
        correct-unconfirmed false 1 0 5.7 5.7 390 74 1.0 0      0 0 0 0 0
    incorrect results 2 -32 27   27   410 360 260   .0082 3 -96 21 12 1100 0   0   9 -288 180 120 4100 5.7 0   0 1 -32 .63 .62 20 .070 0    0
        incorrect true 0 3 -96 21 12 1100 0   0   9 -288 180 120 4100 5.7 0   0 1 -32 .63 .62 20 .070 0    0
        incorrect false 2 -32 27   27   410 360 260   .0082 0 0 0 0 0
score (48 tasks, max score: 75) -26 -91 -280 4 -25 54
Run set depthk.sv-comp19_prop-memsafety.MemSafety-Other cpa-seq-validate-violation-witnesses-depthk.sv-comp19_prop-memsafety.MemSafety-Other uautomizer-validate-violation-witnesses-depthk.sv-comp19_prop-memsafety.MemSafety-Other cpa-witness2test-validate-violation-witnesses-depthk.sv-comp19_prop-memsafety.MemSafety-Other fshell-witness2test-validate-violation-witnesses-depthk.sv-comp19_prop-memsafety.MemSafety-Other uautomizer-validate-correctness-witnesses-depthk.sv-comp19_prop-memsafety.MemSafety-Other