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