Tool Forester
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-13 11:23:04 CET [[ 2017-01-15 01:40:02 CET ]] [[ 2017-01-15 01:58:53 CET ]] [[ 2017-01-15 01:41:42 CET ]] [[ 2017-01-15 02:00:15 CET ]]
Run set sv-comp17.MemSafety-LinkedLists
Options --trace error-witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/forester.2017-01-13_1123.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/forester.2017-01-13_1123.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/forester.2017-01-13_1123.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/forester.2017-01-13_1123.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 unknown 0 wit inspect .083 .086 .52 12 .0082 .66  - - error (invalid witness file) .57 .37 9.1 40 error (invalid witness file) 6.0 3.2 130 310
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .054 .054 .56 11 .012  .061 - - error (invalid witness file) .57 .36 10   41 error (invalid witness file) 7.9 4.2 87 310
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .061 .064 .50 11 .0082 .79  - - error (invalid witness file) .64 .40 8.9 41 error (invalid witness file) 8.4 4.4 74 300
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 1.3   1.3   18    49 .0082 1.7   - - error (invalid witness file) 3.1  1.7  60   180 true 11   6.0 170 340
heap-manipulation/tree_false-unreach-call_false-valid-deref.i unknown 0 wit inspect .053 .053 .57 11 .0041 0     error (invalid witness file) .59 .38 9.1 43 error (invalid witness file) 7.1 3.8 74 290 - -
heap-manipulation/tree_false-valid-deref.i false(valid-deref) 1 wit inspect .094 .12  .71 18 .0041 7.9   error (invalid witness file) 2.8  1.5  62   160 true 12   6.5 110 350 - -
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .078 .078 .92 14 .0082 0     timeout 94    78    2100   3800 timeout 97   76   1200 810 - -
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .43  .43  5.2  19 .094  0     error (invalid witness file) 2.9  1.6  65   170 error 13   7.0 150 300 - -
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 1.6   1.7   33    45 .078  7.8   timeout 94    76    2200   3800 timeout 97   73   2200 910 - -
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .70  .70  8.3  24 .078  .10  timeout 95    75    1900   3900 timeout 97   70   1500 820 - -
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .19  .20  2.4  16 .066  5.1   - - out of memory 590    480    14000   7000 timeout 960   890   15000 1500
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .051 .053 .47 11 .0041 .73  error (invalid witness file) .60 .38 9.8 41 error (invalid witness file) 5.9 3.2 98 300 - -
list-properties/list_search_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .22  .22  2.4  19 .0041 0     error 4.8  2.6  65   260 timeout 97   62   1900 1200 - -
list-properties/list_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 2.6   930     830    38 .64   7.7   error (invalid witness file) .54 .35 13   44 error (invalid witness file) 6.3 3.3 87 300 - -
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .071 .071 .57 11 .0041 .090 error (invalid witness file) .71 .44 8.2 42 error (invalid witness file) 7.1 3.7 85 300 - -
list-properties/simple_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .082 .082 .54 11 .0041 0     timeout 93    71    2100   4100 unknown 31   18   350 490 - -
list-properties/splice_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 6.5   930     900    84 .80   0     error (invalid witness file) .69 .44 11   42 error (invalid witness file) 8.5 4.4 82 320 - -
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .12  .12  1.5  18 .11   .066 - - error (invalid witness file) .51 .32 12   39 error (invalid witness file) 7.9 4.1 78 300
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .12  .12  1.3  17 .11   .17  - - error (invalid witness file) .57 .36 10   39 error (invalid witness file) 6.3 3.3 76 290
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .12  .12  1.4  17 .11   .066 - - error (invalid witness file) .49 .32 11   40 error (invalid witness file) 6.9 3.6 100 300
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .12  .13  1.5  18 .11   .83  error (invalid witness file) .51 .32 11   40 error (invalid witness file) 7.7 4.1 96 300 - -
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .15  .15  1.4  18 .11   .17  error (invalid witness file) .62 .39 9.2 40 error (invalid witness file) 6.3 3.3 120 300 - -
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .15  .19  1.3  26 .11   8.3   error (invalid witness file) .52 .34 9.3 39 error (invalid witness file) 6.5 3.4 130 290 - -
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .12  .12  1.6  18 .11   .18  error (invalid witness file) .61 .38 8.7 39 error (invalid witness file) 5.9 3.1 100 300 - -
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .12  .12  1.7  17 .11   .074 error (invalid witness file) .53 .35 9.5 39 error (invalid witness file) 5.7 3.1 92 300 - -
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .17  .17  1.3  17 .11   .10  error (invalid witness file) .55 .35 11   40 error (invalid witness file) 6.1 3.3 73 290 - -
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .12  .12  1.4  17 .11   .11  error (invalid witness file) .58 .37 9.0 41 error (invalid witness file) 7.2 3.8 110 300 - -
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .15  .15  1.3  17 .11   .074 error (invalid witness file) .59 .37 8.8 40 error (invalid witness file) 6.3 3.3 110 300 - -
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .14  .17  1.6  26 .11   8.3   error (invalid witness file) .56 .35 11   39 error (invalid witness file) 6.2 3.3 120 300 - -
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .12  .13  1.6  18 .11   .64  error (invalid witness file) .64 .41 7.5 39 error (invalid witness file) 6.6 3.5 100 300 - -
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .54  .54  6.4  29 .041  0     - - timeout 910    840    21000   5400 timeout 960   900   19000 950
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 30     30     410    120 .27   0     - - timeout 910    860    20000   4500 timeout 960   910   25000 970
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 1.3   1.3   15    41 .041  0     - - timeout 910    850    18000   4700 timeout 960   880   16000 1200
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 10     10     120    78 .26   4.9   - - out of memory 760    650    21000   7000 timeout 960   880   14000 2300
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 1.4   1.4   18    37 .094  5.0   - - timeout 910    850    21000   4800 timeout 960   870   22000 1600
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 1.3   1.4   19    45 .098  13     - - timeout 910    850    20000   4800 error 12   6.5 120 300
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 230     230     3100    710 .73   .45  - - timeout 910    850    20000   4800 timeout 960   880   19000 1600
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 120     120     1600    440 .37   13     - - timeout 910    870    17000   4400 timeout 960   890   27000 1300
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .16  .21  1.5  23 .025  13     - - timeout 910    790    19000   6700 timeout 960   920   16000 980
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .86  .87  10    38 .053  5.4   - - timeout 910    840    18000   5300 timeout 960   900   19000 1000
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 670     670     10000    1600 3.1    7.7   - - out of memory 730    600    12000   7000 timeout 960   920   24000 1500
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 2.8   2.8   34    53 .094  0     - - timeout 910    860    31000   4600 timeout 960   890   24000 1600
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .96  .96  13    35 .033  0     - - timeout 910    860    28000   4800 timeout 960   860   14000 1500
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 17     17     230    91 .30   0     - - out of memory 800    670    13000   7000 timeout 960   880   23000 2600
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 6.0   6.1   83    59 .21   13     - - timeout 910    850    26000   4800 timeout 960   870   26000 1500
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .53  .61  6.1  22 .061  4.8   - - timeout 910    860    28000   4800 error 14   7.4 150 310
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.3   4.3   55    66 .38   .56  - - timeout 910    850    18000   4900 timeout 960   860   18000 1900
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 190     190     2400    350 .45   4.8   - - timeout 920    870    21000   4500 timeout 960   880   24000 2000
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .10  .10  1.1  14 .029  0     - - timeout 910    790    18000   7000 timeout 960   880   16000 1600
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i unknown 0 wit inspect .079 .079 .52 11 .0041 0     error (invalid witness file) 2.7  1.5  54   160 true 21   11   210 450 - -
forester-heap/sll-01_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect .071 .098 .96 20 .016  7.8   error (invalid witness file) 3.1  1.7  52   170 true 20   11   370 650 - -
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i unknown 0 wit inspect .053 .055 .64 11 .0041 .62  error (invalid witness file) 2.8  1.5  55   170 true 65   42   1400 910 - -
../../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 48 1300   3200   20000 4600 10    140 52 400 320 8800 17000   52 650 430 11000 11000   52 17000 16000 400000 110000   52 17000 16000 360000 31000  
    correct results 28 48 1300   1300   18000 4000 7.0  110 0 390 310 8500 16000   2 460 320 7800 5500   0 17000 16000 400000 110000   0 17000 16000 360000 28000  
        correct true 20 40 1300   1300   18000 3900 6.8  89 0 0 0 0 0   2 0 0 0 0   0 17000 16000 400000 110000   0 17000 16000 360000 28000  
        correct false 8 8 3.0 3.0 47 160 .20 24 0 390 310 8500 16000   0 460 320 7800 5500   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) 48
Run set sv-comp17.MemSafety-LinkedLists