Tool CBMC 5.8 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* [apollon077; apollon078; apollon091] 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: [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 08:19:34 CET 2017-12-01 08:48:13 CET 2017-12-01 09:05:59 CET 2017-12-01 09:09:10 CET 2017-12-01 08:49:56 CET
Run set cbmc.sv-comp18.MemSafety-LinkedLists cpa-seq-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.MemSafety-LinkedLists uautomizer-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.MemSafety-LinkedLists fshell-witness2test-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.MemSafety-LinkedLists uautomizer-validate-correctness-witnesses-cbmc.sv-comp18-correctness-witness.MemSafety-LinkedLists
Options --graphml-witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cbmc.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/cbmc.2017-12-01_0819.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/cbmc.2017-12-01_0819.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cbmc.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 (42) 0 wit inspect 870    720 8500   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 870    3300 8700   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i error (134) 0 wit inspect 440    13000 4700   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 870    4300 5500   - 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 .75 46 7.7 timeout 0 wit inspect 92   3000 out of memory 0 wit inspect 57   7000 false(valid-deref) 1 wit inspect .69 19 - wit inspect
heap-manipulation/tree_false-valid-deref.i false(valid-deref) 1 wit inspect .76 47 8.8 false(valid-deref) 1 wit inspect 4.1 250 false(valid-deref) 1 wit inspect 4.7 280 false(valid-deref) 1 wit inspect .69 19 - wit inspect
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i false(unreach-call) 0 wit inspect .56 36 4.8 error (recursion) 0 wit inspect 4.8 250 unknown 0 wit inspect 13   370 true -32 wit inspect .70 19 - wit inspect
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i false(unreach-call) 0 wit inspect .70 44 7.1 timeout 0 wit inspect 93   2700 true -32 wit inspect 4.3 280 true -32 wit inspect .65 19 - wit inspect
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i false(unreach-call) 0 wit inspect .59 39 5.6 timeout 0 wit inspect 98   2700 true -32 wit inspect 6.2 280 true -32 wit inspect .66 19 - wit inspect
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i false(unreach-call) 0 wit inspect .56 36 5.3 timeout 0 wit inspect 92   2600 true -32 wit inspect 5.7 290 true -32 wit inspect .66 19 - wit inspect
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 870    4400 6200   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.8
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i false(unreach-call) 0 wit inspect .48 37 5.6 timeout 0 wit inspect 91   2800 true -32 wit inspect 5.1 250 true -32 wit inspect .66 19 - wit inspect
list-properties/list_true-unreach-call_false-valid-memtrack.i false(unreach-call) 0 wit inspect .56 38 5.0 timeout 0 wit inspect 92   2900 unknown 0 wit inspect 15   320 true -32 wit inspect .65 19 - wit inspect
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i false(unreach-call) 0 wit inspect .45 36 4.3 timeout 0 wit inspect 98   3500 true -32 wit inspect 5.7 250 error (1) 0 wit inspect .62 19 - wit inspect
list-properties/simple_true-unreach-call_false-valid-memtrack.i false(unreach-call) 0 wit inspect .51 36 4.4 timeout 0 wit inspect 92   1800 true -32 wit inspect 3.7 240 error (1) 0 wit inspect .61 18 - wit inspect
list-properties/splice_true-unreach-call_false-valid-memtrack.i false(unreach-call) 0 wit inspect .54 37 4.7 timeout 0 wit inspect 95   3400 true -32 wit inspect 5.8 270 error (1) 0 wit inspect .59 19 - wit inspect
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i true 2 wit inspect 71    920 740   - wit inspect - wit inspect - wit inspect true 2 wit inspect 170     1600  
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i true 2 wit inspect 58    910 730   - wit inspect - wit inspect - wit inspect true 2 wit inspect 160     1500  
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i true 2 wit inspect 64    910 690   - wit inspect - wit inspect - wit inspect true 2 wit inspect 220     1600  
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i false(unreach-call) 0 wit inspect 50    1100 540   error (invalid witness file) 0 wit inspect 4.3 210 true -32 wit inspect 15   480 false(valid-deref) -16 wit inspect 1.3  19 - wit inspect
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i false(unreach-call) 0 wit inspect 50    1100 550   error (invalid witness file) 0 wit inspect 4.4 220 true -32 wit inspect 15   480 false(valid-deref) -16 wit inspect 1.3  19 - wit inspect
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i false(unreach-call) 0 wit inspect 49    1100 600   error (invalid witness file) 0 wit inspect 4.6 210 true -32 wit inspect 16   480 false(valid-deref) -16 wit inspect 1.3  19 - wit inspect
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i false(unreach-call) 0 wit inspect 50    1100 550   error (invalid witness file) 0 wit inspect 4.4 210 true -32 wit inspect 10   480 false(valid-deref) -16 wit inspect 1.3  19 - wit inspect
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i false(unreach-call) 0 wit inspect 51    1100 510   error (invalid witness file) 0 wit inspect 4.3 220 true -32 wit inspect 14   480 false(valid-deref) -16 wit inspect 1.3  19 - wit inspect
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i false(unreach-call) 0 wit inspect 51    1100 560   error (invalid witness file) 0 wit inspect 4.4 230 true -32 wit inspect 14   470 false(valid-deref) -16 wit inspect 1.3  19 - wit inspect
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i false(unreach-call) 0 wit inspect 49    1100 540   error (invalid witness file) 0 wit inspect 4.2 210 true -32 wit inspect 16   470 false(valid-deref) -16 wit inspect 1.2  19 - wit inspect
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i false(unreach-call) 0 wit inspect 50    1100 530   error (invalid witness file) 0 wit inspect 4.1 210 true -32 wit inspect 15   480 false(valid-deref) -16 wit inspect 1.3  19 - wit inspect
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i false(unreach-call) 0 wit inspect 49    1100 650   error (invalid witness file) 0 wit inspect 4.4 230 true -32 wit inspect 12   480 false(valid-deref) -16 wit inspect 1.3  19 - wit inspect
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i false(unreach-call) 0 wit inspect 51    1100 610   error (invalid witness file) 0 wit inspect 4.5 210 true -32 wit inspect 16   470 false(valid-deref) -16 wit inspect 1.3  19 - wit inspect
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 880    3800 9700   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 420    15000 4400   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 870    5200 5500   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 870    2200 4600   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 870    3100 5800   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 870    3300 5000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.9
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 870    5400 6400   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 870    1000 7500   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 870    970 9600   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 870    700 10000   - 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 error (42) 0 wit inspect 870    970 7600   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.9
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 410    15000 4900   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 880    4800 6500   - 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 (42) 0 wit inspect 870    1900 7000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 870    2100 5200   - 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 error (42) 0 wit inspect 870    2300 7100   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 870    2400 4700   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 870    800 7600   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 870    970 9000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect .67 42 6.5 timeout 0 wit inspect 92   2600 false(valid-deref) 1 wit inspect 9.4 360 false(valid-deref) 1 wit inspect .67 19 - wit inspect
forester-heap/sll-01_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect .57 36 5.1 timeout 0 wit inspect 92   2600 false(valid-deref) 1 wit inspect 10   520 false(valid-deref) 1 wit inspect .67 19 - wit inspect
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect .59 37 5.1 timeout 0 wit inspect 98   2700 false(valid-deref) 1 wit inspect 5.5 350 false(valid-deref) 1 wit inspect .70 19 - 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 11 20000   110000 170000 24 1 1200   36000 24 -540 290 16000 24 -347 22   450 27 6 560 4900
    correct results 8 11 200   2900 2200 1 1 4.1 250 4 4 30 1500 5 5 3.4 94 3 6 550 4800
        correct true 3 6 190   2700 2200 0 0 0 3 6 550 4800
        correct false 5 5 3.3 210 33 1 1 4.1 250 4 4 30 1500 5 5 3.4 94 0
    incorrect results 0 0 17 -544 180 6600 16 -352 17   300 0
        incorrect true 0 0 17 -544 180 6600 6 -192 4.0 110 0
        incorrect false 0 0 0 10 -160 13   190 0
score (51 tasks, max score: 78) 11 1 -540 -347 6
Run set cbmc.sv-comp18.MemSafety-LinkedLists cpa-seq-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.MemSafety-LinkedLists uautomizer-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.MemSafety-LinkedLists fshell-witness2test-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.MemSafety-LinkedLists uautomizer-validate-correctness-witnesses-cbmc.sv-comp18-correctness-witness.MemSafety-LinkedLists