Tool ESBMC ESBMC version 3.1 64-bit x86_64 linux
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 06:35:22 CET [[ 2017-01-15 01:30:25 CET ]] [[ 2017-01-15 01:30:43 CET ]] [[ 2017-01-15 01:30:33 CET ]] [[ 2017-01-15 01:30:54 CET ]]
Run set sv-comp17.MemSafety-Arrays
Options -s kinduction [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-kind.2017-01-13_0635.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-kind.2017-01-13_0635.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-kind.2017-01-13_0635.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-kind.2017-01-13_0635.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 .21  .21  2.2  24 .99 0   error (invalid witness file) .52 .33 12   39 error (invalid witness file) 6.2 3.3 120 290 - -
array-memsafety/bubblesort_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .093 .092 1.0  23 .84 0   error (invalid witness file) .52 .34 12   39 error (invalid witness file) 6.3 3.4 130 300 - -
array-memsafety/count_down_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .20  .20  2.0  24 .99 0   error (invalid witness file) .59 .38 7.7 40 error (invalid witness file) 5.7 3.1 100 290 - -
array-memsafety/cstrcat_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .094 .095 .91 23 .99 0   error (invalid witness file) .57 .36 9.8 40 error (invalid witness file) 5.9 3.1 110 300 - -
array-memsafety/cstrchr_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .10  .10  1.2  24 .99 0   error (invalid witness file) .51 .32 11   40 error (invalid witness file) 6.3 3.3 140 310 - -
array-memsafety/cstrlen_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .14  .13  1.1  24 .84 0   error (invalid witness file) .50 .32 11   39 error (invalid witness file) 6.2 3.3 110 300 - -
array-memsafety/cstrncat_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .11  .11  1.1  23 .99 0   error (invalid witness file) .56 .36 13   40 error (invalid witness file) 6.9 3.6 81 300 - -
array-memsafety/cstrncpy_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .094 .093 1.2  23 .84 0   error (invalid witness file) .52 .34 11   41 error (invalid witness file) 6.1 3.3 110 290 - -
array-memsafety/cstrpbrk_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .11  .11  1.3  24 .84 0   error (invalid witness file) .50 .31 11   41 error (invalid witness file) 5.8 3.1 110 300 - -
array-memsafety/diff_usafe_false-valid-deref.i false(valid-deref) 1 wit inspect .098 .097 1.0  23 .99 0   error (invalid witness file) .53 .33 12   40 error (invalid witness file) 5.8 3.1 130 300 - -
array-memsafety/knapsack_alloca_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .30  .30  3.8  24 .84 0   error (invalid witness file) .50 .32 11   39 error (invalid witness file) 5.9 3.1 130 290 - -
array-memsafety/lis_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .29  .29  3.5  25 .96 0   error (invalid witness file) .50 .32 11   40 error (invalid witness file) 6.0 3.1 120 300 - -
array-memsafety/mult_array_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .31  .31  3.4  26 .84 0   error (invalid witness file) .56 .37 11   41 error (invalid witness file) 5.9 3.1 100 290 - -
array-memsafety/reverse_array_alloca_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .51  .51  6.7  27 .99 0   error (invalid witness file) .54 .34 9.9 43 error (invalid witness file) 6.7 3.6 76 300 - -
array-memsafety/reverse_array_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .21  .21  2.5  24 .84 0   error (invalid witness file) .53 .34 14   41 error (invalid witness file) 5.6 3.0 65 290 - -
array-memsafety/selectionsort_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .11  .10  1.2  23 .99 0   error (invalid witness file) .50 .32 12   40 error (invalid witness file) 5.8 3.1 110 290 - -
array-memsafety/stroeder1_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .10  .10  1.1  23 .84 0   error (invalid witness file) .51 .31 12   40 error (invalid witness file) 6.0 3.2 110 300 - -
array-memsafety/add_last-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     11000    5800 .99 0   - - error (invalid witness file) .51 .33 12   40 error (invalid witness file) 6.8 3.6 100 300
array-memsafety/array01-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     9000    430 .84 0   - - error (invalid witness file) .52 .33 11   40 error (invalid witness file) 6.4 3.4 130 300
array-memsafety/array02-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     12000    410 .99 0   - - error (invalid witness file) .51 .33 12   40 error (invalid witness file) 6.6 3.4 130 300
array-memsafety/array03-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     7700    880 .99 0   - - error (invalid witness file) .58 .37 9.2 40 error (invalid witness file) 7.3 3.8 130 310
array-memsafety/bubblesort-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     8100    530 .84 0   - - error (invalid witness file) .52 .34 8.3 41 error (invalid witness file) 6.1 3.2 130 300
array-memsafety/count_down-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     9200    390 .84 0   - - error (invalid witness file) .49 .32 13   40 error (invalid witness file) 6.0 3.2 130 300
array-memsafety/cstrcat-alloca_true-valid-memsafety.i unknown 0 wit inspect .23  .23  2.6  24 .99 0   - - error (invalid witness file) .53 .34 11   40 error (invalid witness file) 6.1 3.3 130 290
array-memsafety/cstrchr-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     12000    12000 .99 0   - - error (invalid witness file) .50 .32 11   40 error (invalid witness file) 6.0 3.2 96 290
array-memsafety/cstrcmp-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     13000    8600 .99 0   - - error (invalid witness file) .54 .34 12   41 error (invalid witness file) 6.0 3.2 130 300
array-memsafety/cstrcpy-alloca_true-valid-memsafety.i unknown 0 wit inspect .16  .16  1.9  24 .99 0   - - error (invalid witness file) .50 .32 11   39 error (invalid witness file) 6.5 3.4 120 300
array-memsafety/cstrcspn-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     12000    1600 .99 0   - - error (invalid witness file) .48 .31 11   40 error (invalid witness file) 6.3 3.3 120 300
array-memsafety/cstrlen-alloca_true-valid-memsafety.i out of memory 0 wit inspect 520     520     7600    15000 .99 0   - - error (invalid witness file) .49 .32 13   40 error (invalid witness file) 6.2 3.3 120 290
array-memsafety/cstrncat-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     12000    1000 .99 0   - - error (invalid witness file) .50 .32 14   40 error (invalid witness file) 5.6 3.0 110 290
array-memsafety/cstrncmp-alloca_true-valid-memsafety.i unknown 0 wit inspect .23  .22  2.7  24 .99 0   - - error (invalid witness file) .54 .36 12   40 error (invalid witness file) 5.5 3.0 100 290
array-memsafety/cstrncpy-alloca_true-valid-memsafety.i unknown 0 wit inspect .20  .20  1.9  24 .99 0   - - error (invalid witness file) .50 .31 10   40 error (invalid witness file) 6.5 3.4 120 300
array-memsafety/cstrpbrk-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     12000    1100 .99 0   - - error (invalid witness file) .50 .34 10   40 error (invalid witness file) 6.7 3.5 100 310
array-memsafety/cstrspn-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     11000    1200 .99 0   - - error (invalid witness file) .50 .32 6.9 40 error (invalid witness file) 6.1 3.2 120 310
array-memsafety/diff-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     10000    700 .99 0   - - error (invalid witness file) .47 .32 4.8 39 error (invalid witness file) 6.3 3.3 130 300
array-memsafety/insertionsort-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     10000    400 .99 0   - - error (invalid witness file) .51 .33 12   39 error (invalid witness file) 5.8 3.1 100 290
array-memsafety/java_BubbleSort-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     8800    510 .99 0   - - error (invalid witness file) .54 .36 12   41 error (invalid witness file) 6.1 3.2 110 300
array-memsafety/lis-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     8500    490 .84 0   - - error (invalid witness file) .57 .40 12   40 error (invalid witness file) 7.0 3.7 81 300
array-memsafety/mult_array-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     9600    13000 .84 0   - - error (invalid witness file) .60 .41 13   39 error (invalid witness file) 5.9 3.2 110 300
array-memsafety/openbsd_cbzero-alloca_true-valid-memsafety.i unknown 0 wit inspect .13  .13  1.6  24 .84 0   - - error (invalid witness file) .51 .33 11   40 error (invalid witness file) 6.3 3.3 120 300
array-memsafety/openbsd_cmemchr-alloca_true-valid-memsafety.i unknown 0 wit inspect .13  .13  1.7  24 .84 0   - - error (invalid witness file) .53 .36 12   42 error (invalid witness file) 6.1 3.2 140 300
array-memsafety/openbsd_cmemrchr-alloca_true-valid-memsafety.i unknown 0 wit inspect .13  .13  1.4  24 .99 0   - - error (invalid witness file) .57 .36 10   41 error (invalid witness file) 5.4 2.9 110 290
array-memsafety/openbsd_cmemset-alloca_true-valid-memsafety.i unknown 0 wit inspect .13  .13  1.5  24 .99 0   - - error (invalid witness file) .53 .34 12   41 error (invalid witness file) 6.1 3.2 130 300
array-memsafety/openbsd_cstpcpy-alloca_true-valid-memsafety.i unknown 0 wit inspect .16  .15  1.7  24 .84 0   - - error (invalid witness file) .49 .33 9.2 39 error (invalid witness file) 5.5 3.0 130 290
array-memsafety/openbsd_cstpncpy-alloca_true-valid-memsafety.i unknown 0 wit inspect .18  .18  2.3  24 .99 0   - - error (invalid witness file) .57 .37 13   41 error (invalid witness file) 7.4 3.9 110 320
array-memsafety/openbsd_cstrcat-alloca_true-valid-memsafety.i unknown 0 wit inspect .21  .21  2.9  24 .99 0   - - error (invalid witness file) .52 .33 12   40 error (invalid witness file) 6.5 3.4 140 310
array-memsafety/openbsd_cstrcmp-alloca_true-valid-memsafety.i unknown 0 wit inspect .22  .22  2.3  24 .84 0   - - error (invalid witness file) .49 .32 12   40 error (invalid witness file) 6.3 3.4 130 300
array-memsafety/openbsd_cstrcpy-alloca_true-valid-memsafety.i unknown 0 wit inspect .16  .16  1.8  25 .99 0   - - error (invalid witness file) .52 .36 12   40 error (invalid witness file) 6.4 3.4 110 300
array-memsafety/openbsd_cstrcspn-alloca_true-valid-memsafety.i unknown 0 wit inspect .20  .20  1.9  25 .84 0   - - error (invalid witness file) .60 .41 13   40 error (invalid witness file) 6.3 3.3 120 290
array-memsafety/openbsd_cstrlcpy-alloca_true-valid-memsafety.i unknown 0 wit inspect .22  .21  2.8  25 .84 0   - - error (invalid witness file) .54 .35 11   40 error (invalid witness file) 5.5 3.0 110 290
array-memsafety/openbsd_cstrlen-alloca_true-valid-memsafety.i out of memory 0 wit inspect 300     300     3700    15000 .84 0   - - error (invalid witness file) .49 .33 12   39 error (invalid witness file) 6.2 3.3 130 300
array-memsafety/openbsd_cstrncat-alloca_true-valid-memsafety.i unknown 0 wit inspect .37  .37  5.2  25 .84 0   - - error (invalid witness file) .53 .36 13   41 error (invalid witness file) 6.3 3.3 110 300
array-memsafety/openbsd_cstrncmp-alloca_true-valid-memsafety.i unknown 0 wit inspect .19  .19  2.2  24 .99 0   - - error (invalid witness file) .52 .34 9.1 41 error (invalid witness file) 6.0 3.1 120 300
array-memsafety/openbsd_cstrncpy-alloca_true-valid-memsafety.i unknown 0 wit inspect .18  .18  2.1  24 .99 0   - - error (invalid witness file) .51 .33 11   41 error (invalid witness file) 5.3 2.9 110 290
array-memsafety/openbsd_cstrnlen-alloca_true-valid-memsafety.i out of memory 0 wit inspect 490     490     6600    15000 .99 0   - - error (invalid witness file) .53 .35 11   39 error (invalid witness file) 6.7 3.5 130 320
array-memsafety/openbsd_cstrpbrk-alloca_true-valid-memsafety.i unknown 0 wit inspect .17  .17  2.0  25 .99 0   - - error (invalid witness file) .54 .34 12   43 error (invalid witness file) 6.3 3.3 120 310
array-memsafety/openbsd_cstrspn-alloca_true-valid-memsafety.i unknown 0 wit inspect .18  .17  2.2  24 .99 0   - - error (invalid witness file) .52 .35 12   39 error (invalid witness file) 6.2 3.3 120 300
array-memsafety/openbsd_cstrstr-alloca_true-valid-memsafety.i unknown 0 wit inspect .16  .16  1.9  25 .99 0   - - error (invalid witness file) .57 .37 7.3 39 error (invalid witness file) 5.5 2.9 99 290
array-memsafety/rec_strlen-alloca_true-valid-memsafety.i out of memory 0 wit inspect 480     470     5700    15000 .99 0   - - error (invalid witness file) .48 .31 9.8 39 error (invalid witness file) 5.7 3.1 130 290
array-memsafety/selectionsort-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     8200    610 .99 0   - - error (invalid witness file) .59 .40 11   40 error (invalid witness file) 6.8 3.6 130 320
array-memsafety/stroeder1-alloca_true-valid-memsafety.i out of memory 0 wit inspect 190     190     2400    15000 .84 0   - - error (invalid witness file) .61 .42 12   40 error (invalid witness file) 6.4 3.4 120 300
array-memsafety/stroeder2-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     10000    440 .99 0   - - error (invalid witness file) .50 .32 12   40 error (invalid witness file) 6.3 3.3 130 300
array-memsafety/strreplace-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     14000    460 .99 0   - - error (invalid witness file) .52 .35 11   40 error (invalid witness file) 5.5 3.0 120 280
array-memsafety/subseq-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     11000    820 .99 0   - - error (invalid witness file) .48 .31 8.0 40 error (invalid witness file) 6.7 3.5 100 300
array-memsafety/substring-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     11000    2000 .99 0   - - error (invalid witness file) .51 .35 12   40 error (invalid witness file) 6.0 3.1 120 290
array-examples/relax_false-valid-deref.i false(valid-deref) 1 wit inspect .28  .28  3.3  25 .99 0   error (invalid witness file) .53 .32 12   40 error (invalid witness file) 6.2 3.3 120 300 - -
array-examples/sanfoundry_24_false-valid-deref.i out of memory 0 wit inspect 370     370     4800    15000 .84 0   error (invalid witness file) .59 .38 7.9 40 error (invalid witness file) 6.1 3.2 120 310 - -
array-examples/standard_strcpy_false-valid-deref_ground.i unknown 0 wit inspect .11  .11  .66 23 .99 0   error (invalid witness file) .53 .33 12   40 error (invalid witness file) 5.7 3.0 120 300 - -
array-examples/standard_strcpy_original_false-valid-deref.i unknown 0 wit inspect .11  .11  .69 23 .99 0   error (invalid witness file) .50 .32 12   39 error (invalid witness file) 6.1 3.2 130 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 22000   22000   260000 140000 65 0   69 11   7.1 240 840 69 130 68 2400 6200 69 25 17 530 1900   69 300 160 5700 14000  
    correct results 18 18 3.3 3.3 39 430 17 0   0 9.5 6.0 200 720 0 110 58 2000 5300 0 0 0 0 0   0 0 0 0 0  
        correct true 0
        correct false 18 18 3.3 3.3 39 430 17 0   0 9.5 6.0 200 720 0 110 58 2000 5300 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