Tool ULTIMATE Kojak 0.1.23-3204b741 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* [apollon037; apollon054; apollon077; apollon078; apollon115] 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-03 04:40:15 CET 2017-12-03 05:43:12 CET 2017-12-03 06:07:12 CET 2017-12-03 06:08:25 CET 2017-12-03 05:47:35 CET
Run set ukojak.sv-comp18.MemSafety-LinkedLists cpa-seq-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.MemSafety-LinkedLists uautomizer-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.MemSafety-LinkedLists fshell-witness2test-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.MemSafety-LinkedLists uautomizer-validate-correctness-witnesses-ukojak.sv-comp18-correctness-witness.MemSafety-LinkedLists
Options --full-output -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/ukojak.2017-12-03_0440.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/ukojak.2017-12-03_0440.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/ukojak.2017-12-03_0440.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/ukojak.2017-12-03_0440.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 timeout 0 wit inspect 900   1600 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.8
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   1500 10000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   1600 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   5300 13000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
heap-manipulation/tree_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect 490   1900 7600 timeout 0 wit inspect 93    2900 false(valid-deref) 1 wit inspect 8.8   320   true -32 wit inspect .65   19    - wit inspect
heap-manipulation/tree_false-valid-deref.i false(valid-deref) 1 wit inspect 6.9 350 57 timeout 0 wit inspect 93    2600 true -32 wit inspect 6.8   290   false(valid-deref) 1 wit inspect .66   18    - wit inspect
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   1400 12000 error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i error (7) 0 wit inspect 230   2100 3300 error (invalid witness file) 0 wit inspect .60 41 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   2100 12000 error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   2000 14000 error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0042 .26 - wit inspect
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   1800 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.9
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 43   720 460 error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0011 .28 - wit inspect
list-properties/list_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 69   870 990 error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .021 5.0 error (invalid witness file) 0 wit inspect .0013 .32 - wit inspect
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 40   700 470 error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0012 .29 - wit inspect
list-properties/simple_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 69   950 760 error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0011 .31 - wit inspect
list-properties/splice_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 19   530 170 error (invalid witness file) 0 wit inspect .40 41 error (2) 0 wit inspect .047 4.8 error (invalid witness file) 0 wit inspect .0036 .34 - wit inspect
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   5400 14000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   5300 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   5300 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   4900 13000 error (invalid witness file) 0 wit inspect .56 45 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .0011 .34 - wit inspect
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   5300 14000 error (invalid witness file) 0 wit inspect .80 44 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0039 .34 - wit inspect
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   5300 14000 error (invalid witness file) 0 wit inspect .57 45 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   5200 13000 error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .0011 .29 - wit inspect
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   5300 12000 error (invalid witness file) 0 wit inspect .71 41 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .0012 .27 - wit inspect
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   5100 13000 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .0038 .28 - wit inspect
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   5100 14000 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   5400 12000 error (invalid witness file) 0 wit inspect .58 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0037 .26 - wit inspect
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   5000 11000 error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0035 .29 - wit inspect
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   5100 12000 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0036 .26 - wit inspect
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   2200 14000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .029 5.0
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   1700 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .040 4.8
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   3100 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .028 4.8
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   1900 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   3200 14000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   2600 14000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   2200 13000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   2400 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   2200 13000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.8
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 910   1900 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   2000 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   1800 14000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   2900 13000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.8
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   2500 14000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.8
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   1700 13000 - 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 timeout 0 wit inspect 900   1900 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   2200 13000 - 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 timeout 0 wit inspect 900   2300 13000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.8
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   1900 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i timeout 0 wit inspect 900   2000 12000 error (invalid witness file) 0 wit inspect .72 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0013 .29 - wit inspect
forester-heap/sll-01_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect 510   1700 6800 timeout 0 wit inspect 91    2700 true -32 wit inspect 6.5   320   false(valid-deref) 1 wit inspect .66   18    - wit inspect
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect 480   1300 8100 timeout 0 wit inspect 94    2700 false(valid-deref) 1 wit inspect 6.8   300   true -32 wit inspect .65   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 39000 140000 550000 24 0 380 12000 24 -62 29 1300 24 -62 2.7 80 27 0 .57 130
    correct results 4 4 1500 5300 22000 0 2 2 16 620 2 2 1.3 37 0
        correct true 0 0 0 0 0
        correct false 4 4 1500 5300 22000 0 2 2 16 620 2 2 1.3 37 0
    incorrect results 0 0 2 -64 13 610 2 -64 1.3 37 0
        incorrect true 0 0 2 -64 13 610 2 -64 1.3 37 0
        incorrect false 0 0 0 0 0
score (51 tasks, max score: 78) 4 0 -62 -62 0
Run set ukojak.sv-comp18.MemSafety-LinkedLists cpa-seq-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.MemSafety-LinkedLists uautomizer-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.MemSafety-LinkedLists fshell-witness2test-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.MemSafety-LinkedLists uautomizer-validate-correctness-witnesses-ukojak.sv-comp18-correctness-witness.MemSafety-LinkedLists