Tool 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:22:21 CET 2017-12-01 08:49:28 CET 2017-12-01 09:05:52 CET 2017-12-01 09:09:01 CET 2017-12-01 08:49:44 CET
Run set cpa-seq.sv-comp18.MemSafety-LinkedLists cpa-seq-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.MemSafety-LinkedLists uautomizer-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.MemSafety-LinkedLists fshell-witness2test-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.MemSafety-LinkedLists uautomizer-validate-correctness-witnesses-cpa-seq.sv-comp18-correctness-witness.MemSafety-LinkedLists
Options -svcomp18 -heap 10000M -benchmark -timelimit 900s -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-seq.2017-12-01_0822.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/cpa-seq.2017-12-01_0822.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/cpa-seq.2017-12-01_0822.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cpa-seq.2017-12-01_0822.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 910   5300 6700 - - - 0 .024 4.8
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i 0 2.9 260 26 - - - 0 .018 4.8
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i 0 910   11000 5600 - - - 0 .019 4.9
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i 0 920   5300 6400 - - - 0 .020 4.8
heap-manipulation/tree_false-unreach-call_false-valid-deref.i 0 920   11000 5200 0 .54 41 0 .019 4.8 0 .0012 .26 -
heap-manipulation/tree_false-valid-deref.i 0 920   11000 6600 0 .56 43 0 .022 4.9 0 .0011 .30 -
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i 0 940   11000 5300 0 .56 44 0 .023 4.8 0 .0010 .26 -
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i 0 930   11000 5700 0 .66 41 0 .020 4.9 0 .0011 .26 -
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i 0 920   11000 5400 0 .65 41 0 .019 4.8 0 .0035 .26 -
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i 0 940   11000 6200 0 .57 43 0 .019 4.9 0 .0010 .31 -
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i 0 910   11000 5600 - - - 0 .021 4.8
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i 0 940   11000 5900 0 .44 44 0 .021 4.8 0 .0011 .29 -
list-properties/list_true-unreach-call_false-valid-memtrack.i 0 920   11000 5800 0 .68 42 0 .022 4.8 0 .0010 .30 -
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i 0 920   11000 6400 0 .53 44 0 .018 4.8 0 .0011 .26 -
list-properties/simple_true-unreach-call_false-valid-memtrack.i 0 930   11000 6400 0 .59 41 0 .020 4.9 0 .0012 .26 -
list-properties/splice_true-unreach-call_false-valid-memtrack.i 0 910   11000 5700 0 .53 43 0 .019 4.8 0 .0012 .30 -
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i 2 5.6 290 46 - - - 2 100     1500  
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i 2 6.2 300 51 - - - 2 160     1600  
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i 2 6.2 300 50 - - - 2 150     1700  
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i 1 5.8 310 47 1 6.6  280 -32 11     470   -32 1.2    19    -
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i 1 6.1 300 52 1 7.0  290 -32 15     480   -32 1.2    19    -
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i 1 5.9 300 51 1 6.6  280 -32 14     480   -32 1.2    19    -
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i 1 5.9 280 52 1 6.3  270 -32 15     480   -32 1.2    19    -
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i 1 6.2 310 46 1 6.5  290 -32 17     470   -32 1.2    19    -
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i 1 5.7 300 51 1 6.5  280 -32 11     490   -32 1.2    19    -
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i 1 6.0 300 44 1 7.0  280 -32 14     470   -32 1.2    20    -
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i 1 5.9 300 56 1 6.3  280 -32 15     480   -32 1.2    19    -
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i 1 5.9 310 46 1 6.2  280 -32 15     480   -32 1.2    19    -
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i 1 5.8 310 42 1 6.3  280 -32 14     480   -32 1.2    19    -
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i 0 900   11000 5600 - - - 0 .048 4.8
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i 0 900   9700 4600 - - - 0 .018 5.0
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i 0 940   11000 6200 - - - 0 .020 4.8
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i 0 970   11000 4800 - - - 0 .018 4.9
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i 0 930   11000 5600 - - - 0 .023 4.9
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i 0 930   11000 6200 - - - 0 .020 4.9
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i 0 930   11000 5800 - - - 0 .020 4.8
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i 0 940   11000 6300 - - - 0 .020 4.8
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i 0 920   11000 5600 - - - 0 .020 4.8
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i 0 920   11000 5000 - - - 0 .018 5.0
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i 0 910   11000 4800 - - - 0 .020 4.9
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i 0 960   10000 5600 - - - 0 .021 5.0
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i 0 940   11000 6100 - - - 0 .020 4.8
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i 0 920   11000 5300 - - - 0 .018 4.8
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i 0 910   11000 7700 - - - 0 .019 4.9
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i 0 910   11000 6300 - - - 0 .020 4.9
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i 0 910   11000 5600 - - - 0 .020 5.0
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i 0 900   11000 6700 - - - 0 .022 4.8
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i 0 900   11000 5600 - - - 0 .020 4.8
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i 0 970   11000 5900 0 .52 42 0 .020 4.9 0 .0037 .28 -
forester-heap/sll-01_false-unreach-call_false-valid-deref.i 0 940   11000 5500 0 .54 42 0 .020 5.0 0 .0013 .26 -
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i 0 970   11000 6200 0 .55 43 0 .018 4.9 0 .0012 .28 -
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 16 34000 410000 220000 24 10 73 3400 24 -320 140 4800 24 -320 12 200 27 6 410 5000
    correct results 13 16 77 3900 630 10 10 65 2800 0 0 3 6 410 4800
        correct true 3 6 18 890 150 0 0 0 3 6 410 4800
        correct false 10 10 59 3000 490 10 10 65 2800 0 0 0
    incorrect results 0 0 10 -320 140 4800 10 -320 12 190 0
        incorrect true 0 0 10 -320 140 4800 10 -320 12 190 0
        incorrect false 0 0 0 0 0
score (51 tasks, max score: 78) 16 10 -320 -320 6
Run set cpa-seq.sv-comp18.MemSafety-LinkedLists cpa-seq-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.MemSafety-LinkedLists uautomizer-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.MemSafety-LinkedLists fshell-witness2test-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.MemSafety-LinkedLists uautomizer-validate-correctness-witnesses-cpa-seq.sv-comp18-correctness-witness.MemSafety-LinkedLists