Tool Map2Check Map2Check 7.1 : Wed Nov 22 22:30:11 -04 2017 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 23:12:01 CET 2017-12-02 00:17:27 CET 2017-12-02 00:48:14 CET 2017-12-02 00:49:56 CET 2017-12-02 00:23:19 CET
Run set map2check.sv-comp18.MemSafety-LinkedLists cpa-seq-validate-violation-witnesses-map2check.sv-comp18-violation-witness.MemSafety-LinkedLists uautomizer-validate-violation-witnesses-map2check.sv-comp18-violation-witness.MemSafety-LinkedLists fshell-witness2test-validate-violation-witnesses-map2check.sv-comp18-violation-witness.MemSafety-LinkedLists uautomizer-validate-correctness-witnesses-map2check.sv-comp18-correctness-witness.MemSafety-LinkedLists
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/map2check.2017-12-01_2312.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/map2check.2017-12-01_2312.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/map2check.2017-12-01_2312.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/map2check.2017-12-01_2312.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    210 11000   - - - 0 .019 4.8
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i 0 900    420 10000   - - - 0 .020 4.9
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i 0 900    340 11000   - - - 0 .024 4.8
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i 0 890    370 12000   - - - 0 .020 4.9
heap-manipulation/tree_false-unreach-call_false-valid-deref.i 1 2.7  15 31   1 4.9  250 -32 17     520   1 .87   18    -
heap-manipulation/tree_false-valid-deref.i 1 1.1  15 15   1 3.7  250 1 6.9   280   1 .68   18    -
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i 0 .42 12 5.0 0 .74 43 0 .019 4.9 0 .0015 .26 -
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i 1 .95 15 11   1 3.0  270 -32 6.6   260   -32 .67   18    -
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i 1 1.3  14 19   1 4.6  250 -32 9.9   330   -32 .67   18    -
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i 1 1.2  14 13   1 3.7  250 -32 15     500   -32 .69   18    -
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i 0 890    220 14000   - - - 0 .024 5.0
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i 0 .71 14 9.3 -32 3.9  250 0 16     290   -32 .72   18    -
list-properties/list_true-unreach-call_false-valid-memtrack.i 1 .65 13 7.8 1 3.9  270 -32 7.6   280   -32 .68   18    -
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i 0 .74 13 8.6 -32 2.8  270 0 19     340   -32 .66   18    -
list-properties/simple_true-unreach-call_false-valid-memtrack.i 1 .61 13 7.3 1 2.6  250 -32 8.2   260   -32 .65   18    -
list-properties/splice_true-unreach-call_false-valid-memtrack.i 1 .70 14 9.4 1 3.5  250 0 17     280   -32 .83   18    -
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i 0 27    15000 350   - - - 0 .034 4.9
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i 0 27    15000 380   - - - 0 .020 4.9
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i 0 27    15000 340   - - - 0 .020 4.8
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i 0 6.5  29 78   -32 5.9  270 -32 10     480   -32 1.3    19    -
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i 0 6.5  29 77   -32 5.6  270 -32 14     470   -32 1.2    19    -
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i 0 6.5  29 74   -32 6.0  270 -32 14     460   -32 1.5    19    -
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i 0 6.5  31 83   -32 4.6  270 -32 14     460   -32 1.2    19    -
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i 0 6.5  29 81   -32 6.3  270 -32 16     470   -32 1.2    19    -
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i 0 6.5  29 83   -32 6.6  260 -32 16     470   -32 1.2    19    -
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i 0 6.5  30 82   -32 4.1  270 -32 15     480   -32 1.5    19    -
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i 0 6.5  29 63   -32 4.3  280 -32 14     470   -32 1.4    19    -
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i 0 6.5  29 79   -32 6.4  270 -32 15     470   -32 1.2    19    -
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i 0 6.6  29 91   -32 6.3  270 -32 16     480   -32 1.3    19    -
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i 0 900    470 12000   - - - 0 .019 4.9
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i 0 890    260 10000   - - - 0 .020 4.8
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i 0 900    750 11000   - - - 0 .023 4.8
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i 0 900    75 11000   - - - 0 .020 4.8
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i 0 900    430 11000   - - - 0 .020 4.9
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i 0 900    450 11000   - - - 0 .022 4.8
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i 0 890    200 13000   - - - 0 .020 4.8
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i 0 900    960 11000   - - - 0 .024 4.8
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i 0 890    100 9900   - - - 0 .018 5.0
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i 0 900    390 12000   - - - 0 .021 4.9
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i 0 900    580 13000   - - - 0 .022 4.8
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i 0 900    320 10000   - - - 0 .024 4.8
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i 0 900    1000 10000   - - - 0 .037 4.8
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i 0 890    75 11000   - - - 0 .021 5.0
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i 0 900    510 11000   - - - 0 .020 4.9
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i 0 900    550 12000   - - - 0 .019 4.8
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i 0 890    200 13000   - - - 0 .024 5.0
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i 0 900    920 11000   - - - 0 .025 4.9
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i 0 890    120 9600   - - - 0 .024 4.8
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i 1 1.5  15 18   1 3.8  260 -32 13     510   1 .86   18    -
forester-heap/sll-01_false-unreach-call_false-valid-deref.i 1 1.6  16 20   1 5.0  250 -32 11     350   1 .67   18    -
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i 1 1.4  14 19   1 5.0  250 -32 13     480   1 .86   18    -
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 22000 55000 270000 24 -373 110 6000 24 -607 300   9400 24 -571 22   430 27 0 .60 130
    correct results 11 11 14 160 170 11 11 44 2800 1 1 6.9 280 5 5 3.9 92 0
        correct true 0 0 0 0 0
        correct false 11 11 14 160 170 11 11 44 2800 1 1 6.9 280 5 5 3.9 92 0
    correct-unconfimed results 12 0 66 320 810 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0
        correct-unconfirmed false 12 0 66 320 810 0 0 0 0
    incorrect results 0 12 -384 63 3200 19 -608 250   8200 18 -576 19   330 0
        incorrect true 0 12 -384 63 3200 19 -608 250   8200 18 -576 19   330 0
        incorrect false 0 0 0 0 0
score (51 tasks, max score: 78) 11 -373 -607 -571 0
Run set map2check.sv-comp18.MemSafety-LinkedLists cpa-seq-validate-violation-witnesses-map2check.sv-comp18-violation-witness.MemSafety-LinkedLists uautomizer-validate-violation-witnesses-map2check.sv-comp18-violation-witness.MemSafety-LinkedLists fshell-witness2test-validate-violation-witnesses-map2check.sv-comp18-violation-witness.MemSafety-LinkedLists uautomizer-validate-correctness-witnesses-map2check.sv-comp18-correctness-witness.MemSafety-LinkedLists