Tool ULTIMATE Taipan 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*
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 07:53:44 CET 2017-12-03 08:20:31 CET 2017-12-03 08:37:50 CET 2017-12-03 08:38:58 CET 2017-12-03 08:21:58 CET
Run set utaipan.sv-comp18.MemSafety-LinkedLists cpa-seq-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.MemSafety-LinkedLists uautomizer-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.MemSafety-LinkedLists fshell-witness2test-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.MemSafety-LinkedLists uautomizer-validate-correctness-witnesses-utaipan.sv-comp18-correctness-witness.MemSafety-LinkedLists
Options --full-output -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/utaipan.2017-12-03_0753.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/utaipan.2017-12-03_0753.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/utaipan.2017-12-03_0753.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/utaipan.2017-12-03_0753.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 0 900   840 11000 - - - 0 .035 4.8
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i 0 370   1200 4600 - - - 0 .020 4.9
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i 0 900   1800 12000 - - - 0 .024 4.8
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i 0 900   930 10000 - - - 0 .032 5.0
heap-manipulation/tree_false-unreach-call_false-valid-deref.i 0 140   1200 1500 0 .56 43 0 .049 4.9 0 .0011 .30 -
heap-manipulation/tree_false-valid-deref.i 1 6.3 320 51 0 92    2700 -32 6.6   290   1 .66   18    -
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i 0 900   1200 14000 0 .58 43 0 .018 4.8 0 .0040 .30 -
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i 0 250   1400 3200 0 .57 46 0 .036 4.9 0 .0045 .26 -
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i 0 900   1500 11000 0 .54 43 0 .026 4.8 0 .0040 .34 -
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i 0 900   1500 11000 0 .54 45 0 .044 4.9 0 .0038 .31 -
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i 0 900   1400 11000 - - - 0 .048 4.9
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i 0 24   540 200 0 .56 41 0 .049 4.8 0 .0041 .28 -
list-properties/list_true-unreach-call_false-valid-memtrack.i 0 54   790 530 0 .56 43 0 .020 4.9 0 .0032 .30 -
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i 0 20   600 170 0 .54 44 0 .050 4.8 0 .0043 .30 -
list-properties/simple_true-unreach-call_false-valid-memtrack.i 0 32   710 290 0 .55 43 0 .042 4.8 0 .0048 .26 -
list-properties/splice_true-unreach-call_false-valid-memtrack.i 0 17   420 130 0 .59 44 0 .036 4.8 0 .0041 .28 -
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i 2 230   4900 2600 - - - 2 110     1500  
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i 0 900   6200 11000 - - - 0 .034 5.0
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i 0 900   6400 10000 - - - 0 .018 4.9
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i 0 900   6400 9900 0 .56 43 0 .049 4.8 0 .0011 .34 -
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i 0 900   6400 11000 0 .58 43 0 .048 5.0 0 .0028 .26 -
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i 0 900   5800 9500 0 .52 41 0 .020 5.0 0 .0040 .26 -
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i 0 900   6400 8300 0 .57 41 0 .048 4.9 0 .0045 .26 -
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i 0 900   6600 8900 0 .58 43 0 .050 4.8 0 .0040 .34 -
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i 0 900   4800 9200 0 .56 43 0 .018 4.9 0 .0037 .34 -
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i 0 900   6300 9100 0 .57 43 0 .021 4.9 0 .0045 .26 -
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i 0 900   6200 11000 0 .58 42 0 .023 4.8 0 .0037 .30 -
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i 0 900   6400 9500 0 .58 44 0 .024 4.8 0 .0045 .28 -
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i 0 900   6400 9600 0 .58 46 0 .027 4.8 0 .0039 .30 -
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i 0 360   1200 4600 - - - 0 .026 4.9
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i 0 900   1400 13000 - - - 0 .039 4.9
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i 0 560   1700 6900 - - - 0 .020 4.8
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i 0 900   1500 14000 - - - 0 .019 4.9
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i 0 900   1300 9600 - - - 0 .019 4.8
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i 0 900   1500 11000 - - - 0 .040 4.8
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i 0 900   1500 12000 - - - 0 .049 4.9
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i 0 900   1600 12000 - - - 0 .047 5.0
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i 0 900   1200 10000 - - - 0 .018 4.9
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i 0 510   1100 6600 - - - 0 .042 4.8
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i 0 430   1500 5200 - - - 0 .019 4.8
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i 0 900   880 10000 - - - 0 .019 4.8
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i 0 900   1700 11000 - - - 0 .041 4.9
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i 0 900   1400 13000 - - - 0 .042 4.9
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i 0 900   1600 14000 - - - 0 .018 4.8
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i 0 900   1900 12000 - - - 0 .047 5.0
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i 0 900   1300 12000 - - - 0 .042 4.9
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i 0 900   1500 11000 - - - 0 .021 4.9
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i 0 900   1500 13000 - - - 0 .022 4.9
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i 0 900   1800 15000 0 .56 43 0 .044 4.9 0 .0020 .26 -
forester-heap/sll-01_false-unreach-call_false-valid-deref.i 1 120   1100 1300 0 92    2500 -32 8.8   320   1 .67   18    -
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i 0 900   1400 15000 0 .58 41 0 .018 5.0 0 .0012 .29 -
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 36000 130000 440000 24 0 200 6100 24 -64 16 720 24 2 1.4 43 27 2 110 1700
    correct results 3 4 360 6300 3900 0 0 2 2 1.3 37 1 2 110 1500
        correct true 1 2 230 4900 2600 0 0 0 1 2 110 1500
        correct false 2 2 120 1400 1400 0 0 2 2 1.3 37 0
    incorrect results 0 0 2 -64 15 610 0 0
        incorrect true 0 0 2 -64 15 610 0 0
        incorrect false 0 0 0 0 0
score (51 tasks, max score: 78) 4 0 -64 2 2
Run set utaipan.sv-comp18.MemSafety-LinkedLists cpa-seq-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.MemSafety-LinkedLists uautomizer-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.MemSafety-LinkedLists fshell-witness2test-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.MemSafety-LinkedLists uautomizer-validate-correctness-witnesses-utaipan.sv-comp18-correctness-witness.MemSafety-LinkedLists