Tool Predator-HP 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*
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: 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]
Date of execution 2017-12-01 21:45:44 CET 2017-12-01 22:31:23 CET 2017-12-01 22:35:27 CET 2017-12-01 22:38:24 CET 2017-12-01 22:34:17 CET
Run set predatorhp.sv-comp18.MemSafety-LinkedLists cpa-seq-validate-violation-witnesses-predatorhp.sv-comp18-violation-witness.MemSafety-LinkedLists uautomizer-validate-violation-witnesses-predatorhp.sv-comp18-violation-witness.MemSafety-LinkedLists fshell-witness2test-validate-violation-witnesses-predatorhp.sv-comp18-violation-witness.MemSafety-LinkedLists uautomizer-validate-correctness-witnesses-predatorhp.sv-comp18-correctness-witness.MemSafety-LinkedLists
Options --witness error-witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/predatorhp.2017-12-01_2145.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/predatorhp.2017-12-01_2145.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/predatorhp.2017-12-01_2145.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/predatorhp.2017-12-01_2145.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 true 2 wit inspect 1.5  49 18   - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 4.4   200  
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 2.5  59 29   - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 4.4   200  
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 1.6  67 18   - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 4.3   200  
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 2.2  71 21   - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 3.5   200  
heap-manipulation/tree_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect 2.1  25 22   false(valid-deref) 1 wit inspect 4.4 250 true -32 wit inspect 6.3 260 true -32 wit inspect .82 18 - wit inspect
heap-manipulation/tree_false-valid-deref.i false(valid-deref) 1 wit inspect .16 25 2.0 false(valid-deref) 1 wit inspect 4.4 260 true -32 wit inspect 6.9 290 false(valid-deref) 1 wit inspect .86 19 - wit inspect
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .16 25 1.9 false(valid-memtrack) 1 wit inspect 4.5 260 true -32 wit inspect 7.1 340 true -32 wit inspect .81 18 - wit inspect
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .17 23 1.9 false(valid-memtrack) 1 wit inspect 4.5 260 true -32 wit inspect 7.5 250 true -32 wit inspect .85 18 - wit inspect
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .14 23 2.0 false(valid-memtrack) 1 wit inspect 4.2 250 true -32 wit inspect 35   510 false(valid-deref) -16 wit inspect .70 18 - wit inspect
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .16 23 1.7 false(valid-memtrack) 1 wit inspect 2.5 250 timeout 0 wit inspect 97   730 false(valid-deref) -16 wit inspect .85 18 - wit inspect
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    2000 9700   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .025 4.8
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .16 23 1.7 timeout 0 wit inspect 92   2500 unknown 0 wit inspect 11   270 false(valid-deref) -16 wit inspect .87 18 - wit inspect
list-properties/list_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .15 24 1.8 false(valid-memtrack) 1 wit inspect 4.3 250 unknown 0 wit inspect 12   280 false(valid-deref) -16 wit inspect .86 18 - wit inspect
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .17 23 1.8 timeout 0 wit inspect 92   2800 unknown 0 wit inspect 14   280 true -32 wit inspect .88 18 - wit inspect
list-properties/simple_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .15 23 1.9 false(valid-memtrack) 1 wit inspect 3.9 250 unknown 0 wit inspect 22   320 true -32 wit inspect .83 18 - wit inspect
list-properties/splice_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .16 24 1.7 false(valid-memtrack) 1 wit inspect 4.0 250 unknown 0 wit inspect 12   280 true -32 wit inspect .84 18 - wit inspect
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i true 2 wit inspect .60 53 5.2 - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 4.5   200  
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i true 2 wit inspect .57 51 5.1 - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 3.6   200  
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i true 2 wit inspect .54 52 5.1 - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 4.7   200  
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .48 52 5.1 true -32 wit inspect 7.0 290 true -32 wit inspect 17   470 true -32 wit inspect 1.6  18 - wit inspect
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .52 52 4.9 true -32 wit inspect 4.3 290 true -32 wit inspect 18   480 true -32 wit inspect 1.3  18 - wit inspect
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .53 52 4.4 true -32 wit inspect 9.1 290 true -32 wit inspect 15   460 true -32 wit inspect 1.5  18 - wit inspect
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .50 52 5.0 true -32 wit inspect 8.2 270 true -32 wit inspect 10   480 true -32 wit inspect 1.5  18 - wit inspect
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .53 52 4.7 true -32 wit inspect 8.1 290 true -32 wit inspect 20   470 true -32 wit inspect 1.5  18 - wit inspect
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .50 52 5.6 true -32 wit inspect 8.6 300 true -32 wit inspect 11   480 true -32 wit inspect 1.6  18 - wit inspect
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .52 52 4.7 true -32 wit inspect 7.9 290 true -32 wit inspect 14   470 true -32 wit inspect 1.6  18 - wit inspect
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .52 51 5.0 true -32 wit inspect 7.9 290 true -32 wit inspect 19   470 true -32 wit inspect 1.3  18 - wit inspect
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .52 52 5.1 true -32 wit inspect 8.4 270 true -32 wit inspect 15   470 true -32 wit inspect 1.5  18 - wit inspect
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .48 52 4.9 true -32 wit inspect 4.3 290 true -32 wit inspect 17   480 true -32 wit inspect 1.6  18 - wit inspect
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 2.2  32 27   - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 3.6   200  
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 2.3  38 24   - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 3.2   200  
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    890 7200   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 2.1  25 21   - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 4.2   200  
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    3900 6000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .025 4.8
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    3500 6300   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .029 4.8
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 2.2  33 23   - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 4.1   200  
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 2.2  38 24   - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 2.6   200  
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 1.8  32 19   - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 4.4   200  
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    280 9500   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.9
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 2.3  39 23   - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 3.4   200  
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 2.3  38 21   - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 5.1   200  
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    700 7400   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .025 4.8
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 2.2  25 23   - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 4.3   200  
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    3300 6200   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.9
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    3300 5400   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .025 5.0
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 2.2  29 24   - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 4.3   200  
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 2.2  37 24   - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 3.6   200  
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 2.1  32 22   - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 4.8   200  
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect .17 24 2.4 false(valid-deref) 1 wit inspect 4.5 250 true -32 wit inspect 31   640 true -32 wit inspect .71 18 - wit inspect
forester-heap/sll-01_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect .13 25 2.1 false(valid-deref) 1 wit inspect 4.8 250 true -32 wit inspect 12   320 false(valid-deref) 1 wit inspect .70 18 - wit inspect
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect .20 23 2.1 false(valid-deref) 1 wit inspect 4.5 250 false(valid-deref) 1 wit inspect 31   620 true -32 wit inspect .88 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 50 7300   20000 58000 24 -308 310 11000 24 -543 460 10000 24 -638 26   440 27 0 77 3800
    correct results 31 50 39   1100 420 12 12 50 3000 1 1 31 620 2 2 1.6 37 0
        correct true 19 38 36   800 380 0 0 0 0
        correct false 12 12 3.9 290 44 12 12 50 3000 1 1 31 620 2 2 1.6 37 0
    correct-unconfimed results 12 0 5.4 560 53 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0
        correct-unconfirmed false 12 0 5.4 560 53 0 0 0 0
    incorrect results 0 10 -320 74 2800 17 -544 260 7400 22 -640 25   400 0
        incorrect true 0 10 -320 74 2800 17 -544 260 7400 18 -576 22   330 0
        incorrect false 0 0 0 4 -64 3.3 74 0
score (51 tasks, max score: 78) 50 -308 -543 -638 0
Run set predatorhp.sv-comp18.MemSafety-LinkedLists cpa-seq-validate-violation-witnesses-predatorhp.sv-comp18-violation-witness.MemSafety-LinkedLists uautomizer-validate-violation-witnesses-predatorhp.sv-comp18-violation-witness.MemSafety-LinkedLists fshell-witness2test-validate-violation-witnesses-predatorhp.sv-comp18-violation-witness.MemSafety-LinkedLists uautomizer-validate-correctness-witnesses-predatorhp.sv-comp18-correctness-witness.MemSafety-LinkedLists