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-Arrays
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)
array-memsafety/add_last_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .19 .19 1.8  20 .0082 0     error 4.4  2.4  77   260 false(valid-deref) 8.9 4.8 180 350 - -
array-memsafety/bubblesort_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .11 .10 .98 17 0      0     error 3.4  1.9  54   260 false(valid-deref) 8.6 4.7 190 340 - -
array-memsafety/count_down_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .25 .24 2.3  24 .0082 0     error 4.4  2.4  82   260 false(valid-deref) 10   5.4 140 350 - -
array-memsafety/cstrcat_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .11 .11 1.1  20 0      2.3   false(valid-deref) 3.2  1.8  68   240 false(valid-deref) 8.3 4.5 170 340 - -
array-memsafety/cstrchr_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .12 .12 1.1  19 0      0     error 4.5  2.5  85   250 false(valid-deref) 17   9.5 360 560 - -
array-memsafety/cstrlen_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .21 .20 1.7  20 .0082 0     error 4.3  2.3  70   260 false(valid-deref) 11   5.8 220 370 - -
array-memsafety/cstrncat_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .12 .12 1.1  21 0      0     error 3.4  1.9  55   250 false(valid-deref) 8.5 4.6 170 350 - -
array-memsafety/cstrncpy_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .12 .11 1.3  21 0      0     error 3.3  1.9  46   250 false(valid-deref) 8.9 4.7 150 320 - -
array-memsafety/cstrpbrk_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .13 .12 1.3  20 0      0     true 4.3  2.4  68   270 false(valid-deref) 12   6.7 270 380 - -
array-memsafety/diff_usafe_false-valid-deref.i false(valid-deref) 1 wit inspect .11 .11 1.1  20 0      0     error 3.6  2.0  65   250 false(valid-deref) 8.4 4.4 180 330 - -
array-memsafety/knapsack_alloca_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .39 .38 3.7  39 .0082 0     error 5.2  2.8  55   260 false(valid-deref) 28   17   520 660 - -
array-memsafety/lis_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .24 .23 1.8  20 .0082 0     exception 3.0  1.7  51   190 false(valid-deref) 15   8.2 320 420 - -
array-memsafety/mult_array_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .25 .24 2.8  27 .0082 0     error 5.3  2.8  58   260 false(valid-deref) 10   5.5 230 350 - -
array-memsafety/reverse_array_alloca_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .32 .32 3.0  33 .0082 2.0   error 4.1  2.2  77   260 false(valid-deref) 10   5.3 130 340 - -
array-memsafety/reverse_array_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .70 .69 9.5  83 .0082 0     error 4.7  2.6  97   260 false(valid-deref) 12   6.6 230 360 - -
array-memsafety/selectionsort_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .11 .10 1.0  18 0      0     error 3.3  1.9  72   250 false(valid-deref) 8.4 4.5 180 340 - -
array-memsafety/stroeder1_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .12 .11 .88 17 0      0     error 3.2  1.8  69   250 false(valid-deref) 8.7 4.7 180 350 - -
array-memsafety/add_last-alloca_true-valid-memsafety.i error (134) 0 wit inspect 120    120    1200    13000 .66   .074 - - error (invalid witness file) .48 .31 5.0 40 error (invalid witness file) 7.1 3.8 87 320
array-memsafety/array01-alloca_true-valid-memsafety.i error (42) 0 wit inspect 850    850    6300    8900 3.6    .19  - - error (invalid witness file) .52 .32 8.9 40 error (invalid witness file) 7.0 3.7 93 300
array-memsafety/array02-alloca_true-valid-memsafety.i error (1) 0 wit inspect 470    470    3700    14000 2.6    0     - - error (invalid witness file) .63 .41 7.1 39 error (invalid witness file) 5.7 3.0 120 300
array-memsafety/array03-alloca_true-valid-memsafety.i error (134) 0 wit inspect 510    510    3700    14000 1.7    12     - - error (invalid witness file) .59 .38 10   42 error (invalid witness file) 6.0 3.2 120 300
array-memsafety/bubblesort-alloca_true-valid-memsafety.i error (42) 0 wit inspect 850    850    6600    2700 3.2    0     - - error (invalid witness file) .50 .33 8.6 40 error (invalid witness file) 5.8 3.1 110 300
array-memsafety/count_down-alloca_true-valid-memsafety.i error (42) 0 wit inspect 850    850    5400    9000 3.0    0     - - error (invalid witness file) .47 .31 6.4 39 error (invalid witness file) 5.7 3.0 100 290
array-memsafety/cstrcat-alloca_true-valid-memsafety.i error (134) 0 wit inspect 110    110    1100    14000 .72   .18  - - error (invalid witness file) .59 .38 9.6 39 error (invalid witness file) 6.6 3.5 88 300
array-memsafety/cstrchr-alloca_true-valid-memsafety.i error (42) 0 wit inspect 850    850    6700    4600 5.1    2.4   - - error (invalid witness file) .49 .32 8.2 39 error (invalid witness file) 6.3 3.4 100 300
array-memsafety/cstrcmp-alloca_true-valid-memsafety.i error (42) 0 wit inspect 850    850    9700    1800 4.2    0     - - error (invalid witness file) .54 .36 8.5 42 error (invalid witness file) 6.6 3.5 110 300
array-memsafety/cstrcpy-alloca_true-valid-memsafety.i error (134) 0 wit inspect 83    83    940    13000 1.8    .074 - - error (invalid witness file) .54 .35 11   40 error (invalid witness file) 7.1 3.7 110 320
array-memsafety/cstrcspn-alloca_true-valid-memsafety.i error (42) 0 wit inspect 850    850    7300    9000 4.3    0     - - error (invalid witness file) .52 .32 11   40 error (invalid witness file) 8.1 4.2 100 310
array-memsafety/cstrlen-alloca_true-valid-memsafety.i error (42) 0 wit inspect 850    850    4500    3900 4.1    0     - - error (invalid witness file) .49 .32 8.5 41 error (invalid witness file) 5.8 3.1 110 300
array-memsafety/cstrncat-alloca_true-valid-memsafety.i error (134) 0 wit inspect 380    380    3600    14000 .78   0     - - error (invalid witness file) .54 .35 9.7 39 error (invalid witness file) 6.3 3.3 130 310
array-memsafety/cstrncmp-alloca_true-valid-memsafety.i error (42) 0 wit inspect 850    850    8500    2000 2.4    0     - - error (invalid witness file) .49 .31 5.7 40 error (invalid witness file) 7.0 3.7 100 300
array-memsafety/cstrncpy-alloca_true-valid-memsafety.i error (134) 0 wit inspect 220    220    3000    14000 4.8    12     - - error (invalid witness file) .59 .38 10   40 error (invalid witness file) 6.2 3.3 110 300
array-memsafety/cstrpbrk-alloca_true-valid-memsafety.i error (42) 0 wit inspect 850    850    8600    9200 4.5    0     - - error (invalid witness file) .54 .35 11   40 error (invalid witness file) 6.1 3.2 110 300
array-memsafety/cstrspn-alloca_true-valid-memsafety.i error (42) 0 wit inspect 850    850    7400    9100 3.8    .10  - - error (invalid witness file) .51 .34 5.0 39 error (invalid witness file) 6.7 3.6 72 290
array-memsafety/diff-alloca_true-valid-memsafety.i error (42) 0 wit inspect 850    850    3400    6500 2.0    2.4   - - error (invalid witness file) .60 .38 12   42 error (invalid witness file) 6.1 3.2 84 280
array-memsafety/insertionsort-alloca_true-valid-memsafety.i error (42) 0 wit inspect 850    850    3700    9000 .24   0     - - error (invalid witness file) .61 .39 8.9 40 error (invalid witness file) 6.2 3.3 120 300
array-memsafety/java_BubbleSort-alloca_true-valid-memsafety.i error (42) 0 wit inspect 850    850    6500    2800 2.9    0     - - error (invalid witness file) .50 .31 10   39 error (invalid witness file) 6.8 3.6 81 290
array-memsafety/lis-alloca_true-valid-memsafety.i error (42) 0 wit inspect 850    850    5700    2500 1.8    0     - - error (invalid witness file) .50 .32 10   40 error (invalid witness file) 6.9 3.6 80 300
array-memsafety/mult_array-alloca_true-valid-memsafety.i error (134) 0 wit inspect 110    110    1300    14000 1.8    .074 - - error (invalid witness file) .51 .32 13   39 error (invalid witness file) 8.2 4.3 84 320
array-memsafety/openbsd_cbzero-alloca_true-valid-memsafety.i error (1) 0 wit inspect 83    83    1100    13000 1.5    0     - - error (invalid witness file) .59 .37 14   44 error (invalid witness file) 7.7 4.0 110 320
array-memsafety/openbsd_cmemchr-alloca_true-valid-memsafety.i error (42) 0 wit inspect 850    850    5900    1300 7.8    0     - - error (invalid witness file) .47 .30 8.6 39 error (invalid witness file) 8.4 4.4 85 310
array-memsafety/openbsd_cmemrchr-alloca_true-valid-memsafety.i error (42) 0 wit inspect 850    850    3900    1000 .44   0     - - error (invalid witness file) .60 .38 6.2 42 error (invalid witness file) 6.1 3.2 100 300
array-memsafety/openbsd_cmemset-alloca_true-valid-memsafety.i error (1) 0 wit inspect 84    84    870    13000 1.5    0     - - error (invalid witness file) .57 .37 9.6 41 error (invalid witness file) 6.1 3.2 100 310
array-memsafety/openbsd_cstpcpy-alloca_true-valid-memsafety.i error (1) 0 wit inspect 93    94    1000    13000 2.1    0     - - error (invalid witness file) .65 .40 6.4 40 error (invalid witness file) 6.8 3.5 110 310
array-memsafety/openbsd_cstpncpy-alloca_true-valid-memsafety.i error (134) 0 wit inspect 220    220    2600    14000 5.8    0     - - error (invalid witness file) .50 .33 11   41 error (invalid witness file) 6.1 3.2 120 310
array-memsafety/openbsd_cstrcat-alloca_true-valid-memsafety.i error (134) 0 wit inspect 110    110    1300    14000 .73   .36  - - error (invalid witness file) .62 .40 8.0 40 error (invalid witness file) 5.3 2.8 82 290
array-memsafety/openbsd_cstrcmp-alloca_true-valid-memsafety.i error (42) 0 wit inspect 850    850    8900    2200 4.8    .10  - - error (invalid witness file) .50 .32 5.5 39 error (invalid witness file) 6.0 3.2 99 300
array-memsafety/openbsd_cstrcpy-alloca_true-valid-memsafety.i error (134) 0 wit inspect 96    96    1100    13000 1.9    .20  - - error (invalid witness file) .51 .34 6.8 42 error (invalid witness file) 6.5 3.4 110 300
array-memsafety/openbsd_cstrcspn-alloca_true-valid-memsafety.i error (42) 0 wit inspect 850    850    2600    380 4.6    0     - - error (invalid witness file) .51 .32 13   39 error (invalid witness file) 7.7 4.0 91 300
array-memsafety/openbsd_cstrlcpy-alloca_true-valid-memsafety.i error (42) 0 wit inspect 850    850    4600    13000 .71   0     - - error (invalid witness file) .52 .33 10   39 error (invalid witness file) 7.8 4.1 80 300
array-memsafety/openbsd_cstrlen-alloca_true-valid-memsafety.i error (42) 0 wit inspect 850    850    5100    4700 4.6    0     - - error (invalid witness file) .57 .37 10   39 error (invalid witness file) 7.2 3.8 91 300
array-memsafety/openbsd_cstrncat-alloca_true-valid-memsafety.i error (134) 0 wit inspect 430    430    2500    14000 .82   .18  - - error (invalid witness file) .50 .31 7.8 40 error (invalid witness file) 6.2 3.3 110 300
array-memsafety/openbsd_cstrncmp-alloca_true-valid-memsafety.i error (42) 0 wit inspect 850    850    8800    2100 2.7    .19  - - error (invalid witness file) .49 .31 8.3 40 error (invalid witness file) 5.7 3.0 110 300
array-memsafety/openbsd_cstrncpy-alloca_true-valid-memsafety.i error (134) 0 wit inspect 200    200    2400    14000 5.7    .18  - - error (invalid witness file) .51 .32 8.2 40 error (invalid witness file) 7.0 3.6 120 310
array-memsafety/openbsd_cstrnlen-alloca_true-valid-memsafety.i error (42) 0 wit inspect 850    850    4700    2100 6.0    0     - - error (invalid witness file) .55 .36 11   41 error (invalid witness file) 6.9 3.7 100 300
array-memsafety/openbsd_cstrpbrk-alloca_true-valid-memsafety.i error (42) 0 wit inspect 850    850    3900    300 4.6    12     - - error (invalid witness file) .49 .32 10   40 error (invalid witness file) 5.7 3.1 110 300
array-memsafety/openbsd_cstrspn-alloca_true-valid-memsafety.i error (42) 0 wit inspect 850    850    4900    920 .19   0     - - error (invalid witness file) .53 .33 12   40 error (invalid witness file) 7.2 3.8 81 290
array-memsafety/openbsd_cstrstr-alloca_true-valid-memsafety.i error (42) 0 wit inspect 850    850    3100    7600 .38   0     - - error (invalid witness file) .49 .32 12   39 error (invalid witness file) 6.9 3.6 83 310
array-memsafety/rec_strlen-alloca_true-valid-memsafety.i error (42) 0 wit inspect 850    850    5000    8300 4.1    0     - - error (invalid witness file) .47 .31 7.9 39 error (invalid witness file) 7.6 3.9 85 290
array-memsafety/selectionsort-alloca_true-valid-memsafety.i error (134) 0 wit inspect 63    63    640    14000 .18   .074 - - error (invalid witness file) .50 .33 8.4 39 error (invalid witness file) 7.6 3.9 89 310
array-memsafety/stroeder1-alloca_true-valid-memsafety.i error (134) 0 wit inspect 76    76    1000    14000 .88   0     - - error (invalid witness file) .52 .33 11   41 error (invalid witness file) 6.3 3.3 110 300
array-memsafety/stroeder2-alloca_true-valid-memsafety.i error (134) 0 wit inspect 61    61    560    14000 .12   .074 - - error (invalid witness file) .68 .42 8.1 41 error (invalid witness file) 7.2 3.7 86 300
array-memsafety/strreplace-alloca_true-valid-memsafety.i error (134) 0 wit inspect 220    220    1300    14000 .80   2.4   - - error (invalid witness file) .48 .33 11   39 error (invalid witness file) 6.6 3.5 95 300
array-memsafety/subseq-alloca_true-valid-memsafety.i error (42) 0 wit inspect 850    850    4700    1900 .66   0     - - error (invalid witness file) .52 .33 10   41 error (invalid witness file) 6.1 3.2 120 290
array-memsafety/substring-alloca_true-valid-memsafety.i error (42) 0 wit inspect 850    850    6500    10000 5.6    .10  - - error (invalid witness file) .51 .33 12   40 error (invalid witness file) 8.7 4.5 85 310
array-examples/relax_false-valid-deref.i false(valid-deref) 1 wit inspect .20 .20 1.9  20 .0082 0     error 4.5  2.5  100   260 false(valid-deref) 10   5.7 140 350 - -
array-examples/sanfoundry_24_false-valid-deref.i error (42) 0 wit inspect 850    850    5200    6200 15      0     error (invalid witness file) .50 .31 9.2 39 error (invalid witness file) 5.5 3.0 120 300 - -
array-examples/standard_strcpy_false-valid-deref_ground.i out of memory 0 wit inspect 74    74    930    15000 .76   2.0   error (invalid witness file) .64 .40 7.9 40 error (invalid witness file) 6.0 3.2 110 290 - -
array-examples/standard_strcpy_original_false-valid-deref.i out of memory 0 wit inspect 74    74    960    15000 .76   0     error (invalid witness file) .49 .32 9.8 40 error (invalid witness file) 6.0 3.2 91 300 - -
../../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 69 18 29000   29000   200000 440000 150     53   69 74 41 1300 4700 69 220 120 4300 7800 69 26 16 440 1900   69 320 170 4800 14000  
    correct results 18 18 3.8 3.7 39 460 .074 4.3 2 72 40 1200 4600 18 200 110 3900 6900 0 0 0 0 0   0 0 0 0 0  
        correct true 0
        correct false 18 18 3.8 3.7 39 460 .074 4.3 1 72 40 1200 4600 18 200 110 3900 6900 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 (69 tasks, max score: 117) 18
Run set sv-comp17.MemSafety-Arrays