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 05:20:12 CET [[ 2017-01-15 00:51:08 CET ]] [[ 2017-01-15 01:00:54 CET ]] [[ 2017-01-15 00:55:05 CET ]] [[ 2017-01-15 01:06:26 CET ]]
Run set sv-comp17.MemSafety-Arrays
Options -s falsi [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-falsi.2017-01-13_0520.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-falsi.2017-01-13_0520.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-falsi.2017-01-13_0520.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-falsi.2017-01-13_0520.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  .20  2.2  24 .84 0   error (invalid witness file) .50 .31 9.4 40 error (invalid witness file) 5.8 3.1 93 310 - -
array-memsafety/bubblesort_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .10  .10  1.1  23 .99 0   error (invalid witness file) .51 .34 11   40 error (invalid witness file) 6.0 3.1 80 300 - -
array-memsafety/count_down_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .21  .21  1.9  24 .84 0   error (invalid witness file) .50 .33 11   39 error (invalid witness file) 5.4 2.9 84 290 - -
array-memsafety/cstrcat_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .12  .12  .96 23 .84 0   error (invalid witness file) .50 .33 11   40 error (invalid witness file) 6.0 3.1 110 300 - -
array-memsafety/cstrchr_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .13  .13  1.2  24 .99 0   error (invalid witness file) .50 .33 12   40 error (invalid witness file) 5.9 3.2 100 290 - -
array-memsafety/cstrlen_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .10  .10  1.2  24 .84 0   error (invalid witness file) .50 .33 12   39 error (invalid witness file) 5.7 3.0 88 300 - -
array-memsafety/cstrncat_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .13  .12  1.0  23 .99 0   error (invalid witness file) .53 .34 12   41 error (invalid witness file) 5.1 2.8 95 290 - -
array-memsafety/cstrncpy_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .12  .12  .98 23 .84 0   error (invalid witness file) .55 .35 9.0 43 error (invalid witness file) 5.7 3.1 83 300 - -
array-memsafety/cstrpbrk_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .12  .12  1.3  24 .99 0   error (invalid witness file) .50 .33 11   40 error (invalid witness file) 5.9 3.1 120 300 - -
array-memsafety/diff_usafe_false-valid-deref.i false(valid-deref) 1 wit inspect .12  .12  .95 23 .84 0   error (invalid witness file) .56 .37 13   44 error (invalid witness file) 6.4 3.4 120 310 - -
array-memsafety/knapsack_alloca_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .29  .29  3.5  24 .84 0   error (invalid witness file) .50 .32 12   39 error (invalid witness file) 6.1 3.3 110 300 - -
array-memsafety/lis_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .27  .27  3.3  24 .99 0   error (invalid witness file) .51 .32 12   39 error (invalid witness file) 6.4 3.4 110 310 - -
array-memsafety/mult_array_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .28  .28  3.9  27 .84 0   error (invalid witness file) .49 .32 11   40 error (invalid witness file) 5.9 3.1 100 310 - -
array-memsafety/reverse_array_alloca_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .51  .51  7.3  25 .99 0   error (invalid witness file) .53 .34 13   42 error (invalid witness file) 6.0 3.2 120 300 - -
array-memsafety/reverse_array_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .20  .20  2.5  24 .99 0   error (invalid witness file) .54 .34 8.8 39 error (invalid witness file) 5.7 3.0 87 300 - -
array-memsafety/selectionsort_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .13  .13  .85 23 .99 0   error (invalid witness file) .55 .36 7.4 41 error (invalid witness file) 5.7 3.0 74 310 - -
array-memsafety/stroeder1_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .093 .092 1.0  23 .84 0   error (invalid witness file) .52 .34 9.5 42 error (invalid witness file) 5.7 3.0 96 290 - -
array-memsafety/add_last-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     9500    2700 .99 0   - - error (invalid witness file) .49 .34 6.9 41 error (invalid witness file) 5.9 3.1 110 300
array-memsafety/array01-alloca_true-valid-memsafety.i out of memory 0 wit inspect 850     850     9200    15000 .84 0   - - error (invalid witness file) .51 .33 11   40 error (invalid witness file) 6.1 3.2 110 300
array-memsafety/array02-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     8400    10000 .84 0   - - error (invalid witness file) .49 .32 7.2 41 error (invalid witness file) 5.5 2.9 96 290
array-memsafety/array03-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     9000    13000 .99 0   - - error (invalid witness file) .50 .31 6.7 40 error (invalid witness file) 6.2 3.3 99 300
array-memsafety/bubblesort-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     2200    4200 .99 0   - - error (invalid witness file) .49 .33 6.8 40 error (invalid witness file) 6.6 3.5 110 310
array-memsafety/count_down-alloca_true-valid-memsafety.i out of memory 0 wit inspect 380     370     4500    15000 .99 0   - - error (invalid witness file) .48 .30 9.6 39 error (invalid witness file) 5.6 3.0 99 290
array-memsafety/cstrcat-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     12000    1300 .99 0   - - error (invalid witness file) .50 .31 9.0 40 error (invalid witness file) 6.5 3.4 120 310
array-memsafety/cstrchr-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     13000    4000 .99 0   - - error (invalid witness file) .53 .35 8.3 44 error (invalid witness file) 6.1 3.2 120 300
array-memsafety/cstrcmp-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     2100    1200 .84 0   - - error (invalid witness file) .50 .31 8.6 39 error (invalid witness file) 5.6 3.0 89 290
array-memsafety/cstrcpy-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     11000    7800 .84 0   - - error (invalid witness file) .48 .31 8.3 39 error (invalid witness file) 5.8 3.1 110 300
array-memsafety/cstrcspn-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     11000    500 .99 0   - - error (invalid witness file) .50 .33 11   42 error (invalid witness file) 6.2 3.3 66 300
array-memsafety/cstrlen-alloca_true-valid-memsafety.i out of memory 0 wit inspect 690     690     8400    15000 .84 0   - - error (invalid witness file) .52 .34 5.3 39 error (invalid witness file) 5.6 3.0 76 300
array-memsafety/cstrncat-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     12000    650 .84 0   - - error (invalid witness file) .47 .31 8.2 39 error (invalid witness file) 6.0 3.2 110 300
array-memsafety/cstrncmp-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     12000    3200 .84 0   - - error (invalid witness file) .50 .32 8.3 42 error (invalid witness file) 8.4 4.4 92 290
array-memsafety/cstrncpy-alloca_true-valid-memsafety.i out of memory 0 wit inspect 720     710     7400    15000 .99 0   - - error (invalid witness file) .47 .31 6.4 39 error (invalid witness file) 6.3 3.3 110 300
array-memsafety/cstrpbrk-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     11000    360 .99 0   - - error (invalid witness file) .48 .32 11   40 error (invalid witness file) 6.0 3.2 120 300
array-memsafety/cstrspn-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     11000    390 .99 0   - - error (invalid witness file) .50 .31 6.8 40 error (invalid witness file) 6.1 3.2 100 290
array-memsafety/diff-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     9500    340 .99 0   - - error (invalid witness file) .53 .35 9.6 40 error (invalid witness file) 6.1 3.3 120 300
array-memsafety/insertionsort-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     6800    710 .99 0   - - error (invalid witness file) .49 .32 5.8 42 error (invalid witness file) 5.6 3.0 90 290
array-memsafety/java_BubbleSort-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     10000    8900 .99 0   - - error (invalid witness file) .47 .32 6.7 39 error (invalid witness file) 5.9 3.1 99 300
array-memsafety/lis-alloca_true-valid-memsafety.i out of memory 0 wit inspect 440     440     5500    15000 .99 0   - - error (invalid witness file) .49 .31 11   39 error (invalid witness file) 5.7 3.1 86 300
array-memsafety/mult_array-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     10000    6100 .84 0   - - error (invalid witness file) .49 .32 7.4 40 error (invalid witness file) 5.7 3.0 82 300
array-memsafety/openbsd_cbzero-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     13000    9100 .99 0   - - error (invalid witness file) .52 .35 7.1 42 error (invalid witness file) 6.1 3.2 110 300
array-memsafety/openbsd_cmemchr-alloca_true-valid-memsafety.i out of memory 0 wit inspect 710     700     9400    15000 .99 0   - - error (invalid witness file) .50 .32 9.4 39 error (invalid witness file) 5.6 3.0 95 300
array-memsafety/openbsd_cmemrchr-alloca_true-valid-memsafety.i unknown 0 wit inspect .14  .14  1.3  24 .99 0   - - error (invalid witness file) .49 .32 6.9 40 error (invalid witness file) 6.3 3.3 130 300
array-memsafety/openbsd_cmemset-alloca_true-valid-memsafety.i out of memory 0 wit inspect 800     800     10000    15000 .99 0   - - error (invalid witness file) .49 .31 11   40 error (invalid witness file) 6.1 3.2 99 300
array-memsafety/openbsd_cstpcpy-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     9700    7900 .99 0   - - error (invalid witness file) .54 .34 11   40 error (invalid witness file) 5.6 3.0 98 290
array-memsafety/openbsd_cstpncpy-alloca_true-valid-memsafety.i out of memory 0 wit inspect 640     630     7900    15000 .99 0   - - error (invalid witness file) .53 .33 12   39 error (invalid witness file) 5.6 3.0 74 300
array-memsafety/openbsd_cstrcat-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     11000    1200 .99 0   - - error (invalid witness file) .48 .32 8.1 39 error (invalid witness file) 5.8 3.1 110 290
array-memsafety/openbsd_cstrcmp-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     11000    5200 .99 0   - - error (invalid witness file) .52 .33 11   40 error (invalid witness file) 5.7 3.1 100 300
array-memsafety/openbsd_cstrcpy-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     11000    7900 .99 0   - - error (invalid witness file) .53 .33 7.9 40 error (invalid witness file) 6.0 3.3 110 310
array-memsafety/openbsd_cstrcspn-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     2100    1600 .84 0   - - error (invalid witness file) .48 .32 4.6 40 error (invalid witness file) 5.9 3.1 100 310
array-memsafety/openbsd_cstrlcpy-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     13000    790 .99 0   - - error (invalid witness file) .50 .33 9.3 39 error (invalid witness file) 6.7 3.5 110 310
array-memsafety/openbsd_cstrlen-alloca_true-valid-memsafety.i out of memory 0 wit inspect 510     510     7300    15000 .99 0   - - error (invalid witness file) .55 .36 7.4 44 error (invalid witness file) 5.9 3.1 110 300
array-memsafety/openbsd_cstrncat-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     11000    500 .99 0   - - error (invalid witness file) .47 .31 6.7 39 error (invalid witness file) 6.1 3.2 110 300
array-memsafety/openbsd_cstrncmp-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     14000    13000 .99 0   - - error (invalid witness file) .49 .34 4.7 39 error (invalid witness file) 6.2 3.2 120 300
array-memsafety/openbsd_cstrncpy-alloca_true-valid-memsafety.i out of memory 0 wit inspect 570     560     7500    15000 .99 0   - - error (invalid witness file) .50 .31 4.2 40 error (invalid witness file) 5.9 3.2 97 300
array-memsafety/openbsd_cstrnlen-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     8000    12000 .99 0   - - error (invalid witness file) .52 .35 7.3 40 error (invalid witness file) 6.0 3.2 120 310
array-memsafety/openbsd_cstrpbrk-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     13000    3100 .99 0   - - error (invalid witness file) .47 .30 6.5 39 error (invalid witness file) 6.3 3.3 92 310
array-memsafety/openbsd_cstrspn-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     11000    170 .84 0   - - error (invalid witness file) .50 .32 11   40 error (invalid witness file) 6.5 3.4 110 290
array-memsafety/openbsd_cstrstr-alloca_true-valid-memsafety.i unknown 0 wit inspect .18  .17  1.3  25 .99 0   - - error (invalid witness file) .52 .34 8.5 43 error (invalid witness file) 5.6 3.0 87 290
array-memsafety/rec_strlen-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     12000    14000 .84 0   - - error (invalid witness file) .56 .34 8.3 43 error (invalid witness file) 5.7 3.1 100 300
array-memsafety/selectionsort-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     6500    680 .99 0   - - error (invalid witness file) .52 .33 13   39 error (invalid witness file) 6.1 3.2 110 300
array-memsafety/stroeder1-alloca_true-valid-memsafety.i out of memory 0 wit inspect 320     320     3800    15000 .84 0   - - error (invalid witness file) .47 .32 11   39 error (invalid witness file) 5.9 3.1 88 300
array-memsafety/stroeder2-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     9200    3500 .84 0   - - error (invalid witness file) .49 .30 8.1 40 error (invalid witness file) 6.0 3.2 96 300
array-memsafety/strreplace-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     14000    150 .99 0   - - error (invalid witness file) .54 .35 7.2 41 error (invalid witness file) 5.7 3.0 88 300
array-memsafety/subseq-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     12000    340 .84 0   - - error (invalid witness file) .47 .31 7.1 39 error (invalid witness file) 5.5 2.9 81 300
array-memsafety/substring-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     900     13000    650 .99 0   - - error (invalid witness file) .49 .32 6.7 40 error (invalid witness file) 5.7 3.0 69 310
array-examples/relax_false-valid-deref.i false(valid-deref) 1 wit inspect .26  .26  2.9  25 .99 0   error (invalid witness file) .53 .35 13   42 error (invalid witness file) 5.9 3.1 110 300 - -
array-examples/sanfoundry_24_false-valid-deref.i timeout 0 wit inspect 900     890     10000    680 .99 0   error (invalid witness file) .53 .35 12   39 error (invalid witness file) 6.5 3.4 91 310 - -
array-examples/standard_strcpy_false-valid-deref_ground.i timeout 0 wit inspect 900     890     9400    1100 .99 0   error (invalid witness file) .55 .35 10   42 error (invalid witness file) 5.5 2.9 61 300 - -
array-examples/standard_strcpy_original_false-valid-deref.i timeout 0 wit inspect 900     890     11000    1100 .99 0   error (invalid witness file) .48 .33 7.4 39 error (invalid witness file) 5.9 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 41000   41000   470000 320000 65 0   69 11   7.1 230 850 69 120 65 2000 6300 69 24 16 400 1900   69 290 150 4800 14000  
    correct results 18 18 3.4 3.4 38 430 16 0   0 9.3 6.1 200 730 0 110 56 1800 5400 0 0 0 0 0   0 0 0 0 0  
        correct true 0
        correct false 18 18 3.4 3.4 38 430 16 0   0 9.3 6.1 200 730 0 110 56 1800 5400 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