Tool DepthK DepthK version 3.0 - Fri Jan 6 18:14:20 AMT 2017 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741 CProver witness2test 0.1 ULTIMATE Automizer 0.1.23-3204b741
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* [apollon023; apollon077; apollon078; apollon117; apollon126] [apollon077; apollon078; apollon101; apollon157] [apollon045; apollon077; apollon078; apollon158] [apollon007; apollon009; apollon077; apollon078; apollon119]
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [4; 8], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33554 MB; 33553 MB] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-12-01 09:05:19 CET 2017-12-01 09:58:48 CET 2017-12-01 10:19:41 CET 2017-12-01 10:22:00 CET 2017-12-01 10:02:39 CET
Run set depthk.sv-comp18.MemSafety-LinkedLists cpa-seq-validate-violation-witnesses-depthk.sv-comp18-violation-witness.MemSafety-LinkedLists uautomizer-validate-violation-witnesses-depthk.sv-comp18-violation-witness.MemSafety-LinkedLists fshell-witness2test-validate-violation-witnesses-depthk.sv-comp18-violation-witness.MemSafety-LinkedLists uautomizer-validate-correctness-witnesses-depthk.sv-comp18-correctness-witness.MemSafety-LinkedLists
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/depthk.2017-12-01_0905.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -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 --full-output --validate ../../results-verified/depthk.2017-12-01_0905.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/depthk.2017-12-01_0905.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/depthk.2017-12-01_0905.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 900    1300 10000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    360 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    850 12000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .017 4.9
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    310 9800   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
heap-manipulation/tree_false-unreach-call_false-valid-deref.i false(valid-deref) 0 wit inspect 1.4  29 17   timeout 0 wit inspect 92    2900 true -32 wit inspect 4.3   260   true -32 wit inspect .66   18    - wit inspect
heap-manipulation/tree_false-valid-deref.i false(valid-deref) 1 wit inspect .39 29 4.6 timeout 0 wit inspect 92    2200 true -32 wit inspect 6.7   300   false(valid-deref) 1 wit inspect .66   18    - wit inspect
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 1.2  29 12   error (recursion) 0 wit inspect 4.0  260 true -32 wit inspect 5.0   280   true -32 wit inspect .69   18    - wit inspect
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 1.8  38 20   false(valid-memtrack) 1 wit inspect 4.5  260 true -32 wit inspect 6.8   290   true -32 wit inspect .66   18    - wit inspect
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 1.4  32 18   timeout 0 wit inspect 96    2800 true -32 wit inspect 4.2   250   false(valid-deref) -16 wit inspect .65   18    - wit inspect
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 1.3  29 17   timeout 0 wit inspect 92    2800 true -32 wit inspect 5.4   250   false(valid-deref) -16 wit inspect .65   18    - wit inspect
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    190 8500   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .47 28 5.0 timeout 0 wit inspect 92    3200 true -32 wit inspect 4.9   290   false(valid-deref) -16 wit inspect .65   18    - wit inspect
list-properties/list_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .45 28 5.4 false(valid-memtrack) 1 wit inspect 4.1  260 true -32 wit inspect 4.3   270   false(valid-deref) -16 wit inspect .65   18    - wit inspect
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 1.0  28 13   timeout 0 wit inspect 91    3000 true -32 wit inspect 5.1   260   true -32 wit inspect .63   18    - wit inspect
list-properties/simple_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 1.0  29 15   timeout (exception) 0 wit inspect 91    3700 true -32 wit inspect 4.7   230   true -32 wit inspect .64   18    - wit inspect
list-properties/splice_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .46 29 5.0 timeout 0 wit inspect 92    3000 true -32 wit inspect 5.9   270   true -32 wit inspect .65   18    - wit inspect
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 900    1100 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    990 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    1200 10000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .066 4.9
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 890    990 11000   error (invalid witness file) 0 wit inspect .40 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0015 .28 - wit inspect
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 890    970 12000   error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0011 .28 - wit inspect
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 890    970 10000   error (invalid witness file) 0 wit inspect .59 44 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 890    1000 9600   error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0011 .35 - wit inspect
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 890    1000 9900   error (invalid witness file) 0 wit inspect .58 44 error (2) 0 wit inspect .031 4.9 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 890    1200 9500   error (invalid witness file) 0 wit inspect .40 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .0011 .29 - wit inspect
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 890    1100 9100   error (invalid witness file) 0 wit inspect .40 44 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .0037 .28 - wit inspect
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 890    1100 10000   error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 890    1000 8500   error (invalid witness file) 0 wit inspect .41 43 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 890    1200 10000   error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .045 4.8 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    220 9000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    490 9900   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .046 5.0
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    260 9300   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .046 4.9
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    200 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    330 9800   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    280 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    170 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    160 10000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .017 4.8
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    200 9600   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    230 9500   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    340 8300   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .047 4.9
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    540 10000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    240 9400   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    200 9100   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.9
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    410 9700   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    360 9900   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    170 12000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    190 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .017 4.9
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    200 9900   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(valid-deref) 0 wit inspect 1.5  36 17   timeout 0 wit inspect 92    2500 true -32 wit inspect 4.4   280   true -32 wit inspect .65   18    - wit inspect
forester-heap/sll-01_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect .60 29 7.2 timeout (exception) 0 wit inspect 93    2700 true -32 wit inspect 6.1   260   false(valid-deref) 1 wit inspect .68   18    - wit inspect
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(valid-deref) 0 wit inspect 1.4  30 18   timeout 0 wit inspect 92    2400 true -32 wit inspect 4.4   290   true -32 wit inspect .68   18    - wit inspect
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
total 51 4 33000   23000 370000 24 2 1000   32000 24 -448 72 3800 24 -318 9.2 260 27 0 .63 130
    correct results 4 4 3.2 120 37 2 2 8.7 520 0 2 2 1.3 37 0
        correct true 0 0 0 0 0
        correct false 4 4 3.2 120 37 2 2 8.7 520 0 2 2 1.3 37 0
    correct-unconfimed results 10 0 11   300 140 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0
        correct-unconfirmed false 10 0 11   300 140 0 0 0 0
    incorrect results 0 0 14 -448 72 3800 12 -320 7.9 220 0
        incorrect true 0 0 14 -448 72 3800 8 -256 5.3 150 0
        incorrect false 0 0 0 4 -64 2.6 74 0
score (51 tasks, max score: 78) 4 2 -448 -318 0
Run set depthk.sv-comp18.MemSafety-LinkedLists cpa-seq-validate-violation-witnesses-depthk.sv-comp18-violation-witness.MemSafety-LinkedLists uautomizer-validate-violation-witnesses-depthk.sv-comp18-violation-witness.MemSafety-LinkedLists fshell-witness2test-validate-violation-witnesses-depthk.sv-comp18-violation-witness.MemSafety-LinkedLists uautomizer-validate-correctness-witnesses-depthk.sv-comp18-correctness-witness.MemSafety-LinkedLists