Tool 2LS 0.6.0 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]
Date of execution 2017-12-01 08:19:20 CET 2017-12-01 08:41:15 CET 2017-12-01 08:58:15 CET 2017-12-01 08:59:36 CET 2017-12-01 08:42:37 CET
Run set 2ls.sv-comp18.MemSafety-LinkedLists cpa-seq-validate-violation-witnesses-2ls.sv-comp18-violation-witness.MemSafety-LinkedLists uautomizer-validate-violation-witnesses-2ls.sv-comp18-violation-witness.MemSafety-LinkedLists fshell-witness2test-validate-violation-witnesses-2ls.sv-comp18-violation-witness.MemSafety-LinkedLists uautomizer-validate-correctness-witnesses-2ls.sv-comp18-correctness-witness.MemSafety-LinkedLists
Options --graphml-witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/2ls.2017-12-01_0819.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/2ls.2017-12-01_0819.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/2ls.2017-12-01_0819.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/2ls.2017-12-01_0819.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 error (134) 0 wit inspect .27 29 2.5 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i error (5) 0 wit inspect .38 27 4.4 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i error (5) 0 wit inspect .49 38 5.1 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 13    15000 150   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .031 4.8
heap-manipulation/tree_false-unreach-call_false-valid-deref.i error (5) 0 wit inspect .40 31 3.7 error (invalid witness file) 0 wit inspect .65 41 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect
heap-manipulation/tree_false-valid-deref.i false(valid-deref) 1 wit inspect .41 31 4.2 false(valid-deref) 1 wit inspect 3.8  270 false(valid-deref) 1 wit inspect 6.8   280   false(valid-deref) 1 wit inspect .66   18    - wit inspect
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i error (5) 0 wit inspect .17 26 1.6 error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .0013 .28 - wit inspect
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i error (5) 0 wit inspect .35 29 3.5 error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .0014 .34 - wit inspect
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i witness invalid (false(valid-memtrack)) 0 wit inspect .53 34 5.5 timeout 0 wit inspect 91    2600 true -32 wit inspect 5.9   260   error (invalid witness file) 0 wit inspect .61   18    - wit inspect
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i witness invalid (false(valid-memtrack)) 0 wit inspect .42 33 4.1 timeout 0 wit inspect 91    2600 true -32 wit inspect 5.8   260   error (invalid witness file) 0 wit inspect .60   18    - wit inspect
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i error (5) 0 wit inspect .38 30 3.4 - 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 witness invalid (false(valid-memtrack)) 0 wit inspect .26 27 2.4 timeout 0 wit inspect 92    2900 true -32 wit inspect 5.7   250   error (invalid witness file) 0 wit inspect .59   18    - wit inspect
list-properties/list_true-unreach-call_false-valid-memtrack.i witness invalid (false(valid-memtrack)) 0 wit inspect .45 32 4.7 timeout 0 wit inspect 93    2500 true -32 wit inspect 5.2   240   error (invalid witness file) 0 wit inspect .59   19    - wit inspect
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i error (5) 0 wit inspect .23 27 1.8 error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .022 5.0 error (invalid witness file) 0 wit inspect .0014 .29 - wit inspect
list-properties/simple_true-unreach-call_false-valid-memtrack.i error (5) 0 wit inspect .26 27 2.3 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0012 .34 - wit inspect
list-properties/splice_true-unreach-call_false-valid-memtrack.i witness invalid (false(valid-memtrack)) 0 wit inspect .45 32 5.8 timeout 0 wit inspect 98    3500 true -32 wit inspect 5.5   240   error (invalid witness file) 0 wit inspect .59   18    - wit inspect
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i error (134) 0 wit inspect .93 40 12   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i error (134) 0 wit inspect .93 40 9.3 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i error (134) 0 wit inspect 1.0  40 8.5 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i error (134) 0 wit inspect .95 40 11   error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .0011 .32 - wit inspect
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i error (134) 0 wit inspect .93 40 11   error (invalid witness file) 0 wit inspect .58 42 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i error (134) 0 wit inspect .94 40 9.2 error (invalid witness file) 0 wit inspect .52 42 error (2) 0 wit inspect .020 5.0 error (invalid witness file) 0 wit inspect .0017 .29 - wit inspect
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i error (134) 0 wit inspect .95 40 11   error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0012 .34 - wit inspect
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i error (134) 0 wit inspect .92 40 10   error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .0015 .26 - wit inspect
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i error (134) 0 wit inspect .94 40 9.2 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0011 .34 - wit inspect
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i error (134) 0 wit inspect .98 40 8.4 error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect .0012 .34 - wit inspect
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i error (134) 0 wit inspect .94 42 10   error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .0012 .34 - wit inspect
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i error (134) 0 wit inspect .94 40 10   error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect .0037 .27 - wit inspect
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i error (134) 0 wit inspect .95 40 9.1 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .0015 .30 - wit inspect
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i error (5) 0 wit inspect .44 31 5.4 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .050 5.0
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i error (5) 0 wit inspect .40 32 5.9 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .051 4.9
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i error (5) 0 wit inspect .40 30 3.9 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .040 4.9
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i error (5) 0 wit inspect .47 33 4.6 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .046 4.8
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i error (5) 0 wit inspect .37 30 4.0 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .051 4.9
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i error (5) 0 wit inspect .36 31 3.9 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 91    15000 1100   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .034 4.9
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i error (5) 0 wit inspect .54 35 6.9 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    7900 8500   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i error (5) 0 wit inspect .35 30 3.5 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i error (5) 0 wit inspect .36 30 3.9 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .051 4.8
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i error (5) 0 wit inspect .44 32 4.0 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .049 4.9
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i error (5) 0 wit inspect .38 30 3.6 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i error (5) 0 wit inspect .47 32 4.9 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .051 4.9
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i error (5) 0 wit inspect .32 29 2.8 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i error (5) 0 wit inspect .34 30 3.4 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .051 4.8
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i error (5) 0 wit inspect .43 32 4.7 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i error (5) 0 wit inspect .55 33 5.6 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    8100 8200   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i out of memory 0 wit inspect 34    15000 270   error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .0014 .28 - wit inspect
forester-heap/sll-01_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect .37 30 3.3 false(valid-deref) 1 wit inspect 3.8  260 false(valid-deref) 1 wit inspect 9.6   330   error (1) 0 wit inspect .60   18    - wit inspect
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i error (5) 0 wit inspect .30 28 2.8 error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .0013 .30 - 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 2 2000    62000 18000   24 2 480   15000 24 -158 45 1900 24 1 4.3  130 27 0 .81 130
    correct results 2 2 .77 61 7.5 2 2 7.6 530 2 2 16 610 1 1 .66 18 0
        correct true 0 0 0 0 0
        correct false 2 2 .77 61 7.5 2 2 7.6 530 2 2 16 610 1 1 .66 18 0
    incorrect results 0 0 5 -160 28 1200 0 0
        incorrect true 0 0 5 -160 28 1200 0 0
        incorrect false 0 0 0 0 0
score (51 tasks, max score: 78) 2 2 -158 1 0
Run set 2ls.sv-comp18.MemSafety-LinkedLists cpa-seq-validate-violation-witnesses-2ls.sv-comp18-violation-witness.MemSafety-LinkedLists uautomizer-validate-violation-witnesses-2ls.sv-comp18-violation-witness.MemSafety-LinkedLists fshell-witness2test-validate-violation-witnesses-2ls.sv-comp18-violation-witness.MemSafety-LinkedLists uautomizer-validate-correctness-witnesses-2ls.sv-comp18-correctness-witness.MemSafety-LinkedLists