Tool CBMC 5.6
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-59-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-01-11 10:20:18 CET [[ 2017-01-14 21:14:41 CET ]] [[ 2017-01-14 21:35:33 CET ]] [[ 2017-01-14 21:19:46 CET ]] [[ 2017-01-14 21:37:38 CET ]]
Run set sv-comp17.MemSafety-LinkedLists
Options --graphml-witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cbmc.2017-01-11_1020.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cbmc.2017-01-11_1020.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cbmc.2017-01-11_1020.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cbmc.2017-01-11_1020.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]
../../sv-benchmarks/c/ verifier status score witness inspect witness cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i error (1) 0 wit inspect .30 .29 2.4 21 .0082 0    - - error (invalid witness file) .54 .35 11   43 error (invalid witness file) 6.9 3.6 98 300
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 850    850    9100   3300 6.8    0    - - error (invalid witness file) .65 .41 9.0 40 error (invalid witness file) 6.0 3.2 110 300
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i error (134) 0 wit inspect 400    400    3700   13000 6.7    .18 - - error (invalid witness file) .52 .33 12   41 error (invalid witness file) 6.4 3.3 120 290
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 850    850    4500   4300 1.7    0    - - error (invalid witness file) .50 .32 7.7 39 error (invalid witness file) 6.2 3.3 96 300
heap-manipulation/tree_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect .47 .46 4.5 36 .0082 .19 error 4.8 2.6 100 260 timeout 96   54   1300 6300 - -
heap-manipulation/tree_false-valid-deref.i false(valid-deref) 1 wit inspect .44 .43 4.9 37 .0082 .16 error 5.2 2.8 110 300 false(valid-deref) 9.1 4.9 200 320 - -
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .30 .30 2.5 26 .0082 0    error 5.2 2.8 110 270 true 9.1 4.9 180 330 - -
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .40 .39 4.5 33 .0082 0    assertion 5.0 2.7 48 260 error 11   5.9 230 300 - -
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .29 .28 2.9 27 .0082 0    assertion 4.1 2.3 80 260 true 9.1 4.9 150 340 - -
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .27 .27 2.5 25 .0082 0    assertion 4.3 2.4 63 270 true 8.9 4.8 170 340 - -
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 850    850    4900   4400 2.9    0    - - error (invalid witness file) .51 .33 5.1 39 error (invalid witness file) 7.1 3.8 98 300
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .24 .24 1.8 20 .0082 0    assertion 4.3 2.3 90 260 true 8.8 4.7 160 320 - -
list-properties/list_search_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .65 .64 5.0 24 .10   .19 error 8.3 4.4 70 280 true 11   5.8 220 450 - -
list-properties/list_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .28 .27 2.6 26 .0082 0    assertion 4.1 2.3 75 250 true 9.6 5.0 180 330 - -
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .22 .22 1.6 19 .0082 0    assertion 3.9 2.2 52 260 true 7.7 4.1 160 320 - -
list-properties/simple_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .23 .22 1.5 22 .0082 0    assertion 4.0 2.2 79 260 true 8.3 4.4 170 330 - -
list-properties/splice_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .26 .25 2.0 25 .0082 0    assertion 4.7 2.6 75 270 true 9.3 5.0 150 340 - -
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i true 2 wit inspect 49    49    580   930 6.1    0    - - true 12    6.2  220   350 true 320   240   7600 2200
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i true 2 wit inspect 43    43    480   910 5.4    0    - - true 10    5.2  130   320 true 310   220   4200 1700
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i true 2 wit inspect 48    48    530   920 5.8    0    - - true 12    6.1  180   320 true 290   210   5400 2000
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 38    38    430   1100 1.8    0    exception 5.5 2.9 92 230 true 15   8.3 320 480 - -
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 39    39    470   1100 1.7    .10 exception 5.8 3.1 83 220 true 16   8.6 240 490 - -
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 38    38    510   1100 1.8    .10 exception 5.5 3.0 89 220 true 15   8.2 310 480 - -
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 39    39    460   1100 1.7    .29 exception 5.5 2.9 91 220 true 15   8.3 300 480 - -
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 39    39    450   1100 1.8    0    exception 5.5 2.9 93 220 true 17   9.1 310 480 - -
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 39    39    440   1100 1.8    .27 exception 5.5 2.9 110 220 true 16   8.7 340 480 - -
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 39    39    470   1100 1.8    0    exception 5.5 2.9 110 220 true 18   9.4 270 490 - -
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 39    39    510   1100 1.8    0    exception 5.4 2.9 100 220 true 16   8.6 320 490 - -
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 39    39    460   1100 1.8    0    exception 5.3 2.8 100 220 true 17   9.3 260 480 - -
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 39    39    420   1100 1.9    .10 exception 6.7 3.5 76 230 true 16   8.5 330 480 - -
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 850    850    7900   3900 8.9    .19 - - error (invalid witness file) .51 .33 9.6 40 error (invalid witness file) 8.0 4.2 87 310
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 340    340    3900   15000 14      0    - - error (invalid witness file) .54 .35 12   41 error (invalid witness file) 7.3 3.8 81 300
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i error (1) 0 wit inspect 98    98    1100   400 4.4    0    - - error (invalid witness file) .53 .34 10   41 error (invalid witness file) 7.6 4.0 80 300
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 850    850    4200   2300 2.4    0    - - error (invalid witness file) .48 .31 5.3 40 error (invalid witness file) 6.9 3.6 91 290
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 850    850    5300   3100 2.1    0    - - error (invalid witness file) .52 .33 10   42 error (invalid witness file) 6.4 3.4 110 320
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 850    850    6100   3300 2.1    0    - - error (invalid witness file) .48 .32 8.4 40 error (invalid witness file) 6.7 3.5 130 300
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 850    850    6000   5400 5.1    .10 - - error (invalid witness file) .59 .38 8.3 40 error (invalid witness file) 5.4 2.9 120 290
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 850    850    5500   1000 3.6    .32 - - error (invalid witness file) .70 .45 9.9 39 error (invalid witness file) 5.8 3.1 120 300
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 850    850    11000   890 3.5    0    - - error (invalid witness file) .49 .32 7.1 41 error (invalid witness file) 7.1 3.8 120 310
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 850    850    11000   720 8.5    .19 - - error (invalid witness file) .50 .33 7.8 40 error (invalid witness file) 7.3 3.8 88 310
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 850    850    6400   880 1.2    0    - - error (invalid witness file) .50 .33 6.8 41 error (invalid witness file) 5.8 3.1 120 310
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 320    320    3900   15000 12      0    - - error (invalid witness file) .51 .33 9.7 39 error (invalid witness file) 6.3 3.3 120 300
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i error (1) 0 wit inspect 94    94    930   390 4.1    .10 - - error (invalid witness file) .48 .30 7.5 39 error (invalid witness file) 6.3 3.3 130 300
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 850    850    3600   1800 2.0    0    - - error (invalid witness file) .50 .32 7.0 40 error (invalid witness file) 7.0 3.7 87 310
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 850    850    5600   2100 2.5    .10 - - error (invalid witness file) .51 .33 9.1 40 error (invalid witness file) 6.9 3.6 110 300
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 850    850    5100   2300 2.4    .10 - - error (invalid witness file) .56 .37 9.8 39 error (invalid witness file) 6.7 3.5 110 300
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 850    850    5800   2400 4.2    0    - - error (invalid witness file) .62 .40 6.2 40 error (invalid witness file) 7.2 3.8 100 310
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 850    850    7800   870 6.5    .19 - - error (invalid witness file) .51 .31 8.7 41 error (invalid witness file) 6.7 3.5 130 320
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 850    850    10000   910 2.9    0    - - error (invalid witness file) .65 .41 8.1 41 error (invalid witness file) 6.4 3.4 110 320
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect .37 .36 3.6 31 .0082 0    assertion 4.5 2.5 91 260 false(valid-deref) 13   6.7 250 470 - -
forester-heap/sll-01_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect .25 .25 2.9 23 .0082 .19 assertion 4.5 2.4 84 260 false(valid-deref) 29   16   580 890 - -
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect .29 .28 2.7 26 .0082 0    assertion 4.6 2.5 86 260 false(valid-deref) 13   6.9 260 460 - -
../../sv-benchmarks/c/ verifier status score witness inspect witness cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
total 52 31 17000 17000 140000 100000 150 3.1 52 130 69 2200 6200   52 410 220 7400 17000   52 47 26 740 1900   52 1100 760 20000 13000  
    correct results 28 31 530 530 6300 14000 35 1.6 0 130 69 2200 6200   23 410 220 7400 17000   3 34 17 540 980   3 920 670 17000 5900  
        correct true 3 6 140 140 1600 2800 17 0   0 0 0 0 0   19 0 0 0 0   3 34 17 540 980   3 920 670 17000 5900  
        correct false 25 25 390 390 4700 11000 18 1.6 0 130 69 2200 6200   4 410 220 7400 17000   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 0
        correct-unconfirmed true 0
        correct-unconfirmed false 0
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (52 tasks, max score: 79) 31
Run set sv-comp17.MemSafety-LinkedLists