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 04:52:43 CET [[ 2017-01-15 00:23:14 CET ]] [[ 2017-01-15 00:35:58 CET ]] [[ 2017-01-15 00:29:47 CET ]] [[ 2017-01-15 00:40:29 CET ]]
Run set sv-comp17.MemSafety-Arrays
Options -s fixed [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc.2017-01-13_0452.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc.2017-01-13_0452.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc.2017-01-13_0452.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc.2017-01-13_0452.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 130   130   1500 3300 2.0  0   error (invalid witness file) .52 .33 12   40 error (invalid witness file) 5.9 3.2 110 300 - -
array-memsafety/bubblesort_unsafe_false-valid-deref.i timeout 0 wit inspect 900   900   5500 12000 .99 0   error (invalid witness file) .49 .31 12   39 error (invalid witness file) 6.0 3.2 120 300 - -
array-memsafety/count_down_unsafe_false-valid-deref.i out of memory 0 wit inspect 230   230   2900 15000 .99 0   error (invalid witness file) .51 .33 9.9 40 error (invalid witness file) 5.9 3.2 130 300 - -
array-memsafety/cstrcat_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 15   15   170 850 1.8  0   error (invalid witness file) .50 .32 8.7 40 error (invalid witness file) 6.1 3.2 120 300 - -
array-memsafety/cstrchr_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 3.4 3.4 44 280 2.0  0   error (invalid witness file) .50 .32 3.6 39 error (invalid witness file) 6.3 3.3 110 310 - -
array-memsafety/cstrlen_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 1.9 1.9 26 180 2.0  0   error (invalid witness file) .48 .32 6.2 39 error (invalid witness file) 6.3 3.3 120 300 - -
array-memsafety/cstrncat_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 20   20   260 1600 2.0  0   error (invalid witness file) .50 .33 5.7 39 error (invalid witness file) 6.5 3.4 130 310 - -
array-memsafety/cstrncpy_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 890   890   7000 9100 2.0  0   error (invalid witness file) .52 .34 3.8 41 error (invalid witness file) 5.4 2.9 110 280 - -
array-memsafety/cstrpbrk_unsafe_false-valid-deref.i timeout 0 wit inspect 900   900   7700 5700 .99 0   error (invalid witness file) .52 .33 6.8 40 error (invalid witness file) 6.1 3.3 120 290 - -
array-memsafety/diff_usafe_false-valid-deref.i timeout 0 wit inspect 900   900   9100 7200 .99 0   error (invalid witness file) .49 .33 9.4 39 error (invalid witness file) 6.2 3.3 120 300 - -
array-memsafety/knapsack_alloca_unsafe_false-valid-deref.i out of memory 0 wit inspect 540   540   3400 15000 .84 0   error (invalid witness file) .49 .32 9.0 40 error (invalid witness file) 6.0 3.2 120 290 - -
array-memsafety/lis_unsafe_false-valid-deref.i out of memory 0 wit inspect 32   32   380 15000 .99 0   error (invalid witness file) .51 .33 6.8 41 error (invalid witness file) 5.9 3.1 110 300 - -
array-memsafety/mult_array_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 20   20   240 1300 2.0  0   error (invalid witness file) .47 .32 9.9 39 error (invalid witness file) 6.1 3.2 130 290 - -
array-memsafety/reverse_array_alloca_unsafe_false-valid-deref.i timeout 0 wit inspect 900   900   11000 4200 .84 0   error (invalid witness file) .46 .31 8.3 39 error (invalid witness file) 5.9 3.1 120 300 - -
array-memsafety/reverse_array_unsafe_false-valid-deref.i timeout 0 wit inspect 900   900   11000 2000 .99 0   error (invalid witness file) .52 .33 13   40 error (invalid witness file) 5.6 3.0 110 290 - -
array-memsafety/selectionsort_unsafe_false-valid-deref.i timeout 0 wit inspect 900   900   8000 7200 .99 0   error (invalid witness file) .53 .34 13   39 error (invalid witness file) 5.7 3.0 120 290 - -
array-memsafety/stroeder1_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 2.9 2.9 33 310 1.7  0   error (invalid witness file) .48 .30 9.4 40 error (invalid witness file) 5.8 3.1 120 300 - -
array-memsafety/add_last-alloca_true-valid-memsafety.i true 2 wit inspect 890   890   11000 4100 1.7  0   - - error (invalid witness file) .56 .37 8.6 42 error (invalid witness file) 6.1 3.2 130 300
array-memsafety/array01-alloca_true-valid-memsafety.i out of memory 0 wit inspect 230   230   2500 15000 .99 0   - - error (invalid witness file) .52 .32 9.7 40 error (invalid witness file) 6.1 3.2 120 300
array-memsafety/array02-alloca_true-valid-memsafety.i out of memory 0 wit inspect 300   300   2300 15000 .99 0   - - error (invalid witness file) .49 .32 7.0 39 error (invalid witness file) 6.3 3.3 130 300
array-memsafety/array03-alloca_true-valid-memsafety.i out of memory 0 wit inspect 50   50   570 15000 .99 0   - - error (invalid witness file) .49 .31 9.7 39 error (invalid witness file) 6.1 3.2 120 300
array-memsafety/bubblesort-alloca_true-valid-memsafety.i out of memory 0 wit inspect 330   330   3000 15000 .99 0   - - error (invalid witness file) .54 .35 9.1 39 error (invalid witness file) 5.3 2.9 110 290
array-memsafety/count_down-alloca_true-valid-memsafety.i out of memory 0 wit inspect 250   250   2300 15000 .99 0   - - error (invalid witness file) .50 .32 12   42 error (invalid witness file) 5.9 3.2 120 300
array-memsafety/cstrcat-alloca_true-valid-memsafety.i true 2 wit inspect 390   390   4700 1600 1.8  0   - - error (invalid witness file) .52 .33 11   39 error (invalid witness file) 5.6 3.0 120 290
array-memsafety/cstrchr-alloca_true-valid-memsafety.i true 2 wit inspect 20   20   210 490 2.0  0   - - error (invalid witness file) .52 .34 13   40 error (invalid witness file) 6.6 3.5 130 320
array-memsafety/cstrcmp-alloca_true-valid-memsafety.i true 2 wit inspect 320   320   1100 850 2.0  0   - - error (invalid witness file) .50 .32 9.8 39 error (invalid witness file) 6.2 3.3 110 300
array-memsafety/cstrcpy-alloca_true-valid-memsafety.i true 2 wit inspect 21   21   260 860 2.0  0   - - error (invalid witness file) .54 .37 8.5 43 error (invalid witness file) 6.2 3.3 120 300
array-memsafety/cstrcspn-alloca_true-valid-memsafety.i timeout 0 wit inspect 900   900   8800 10000 .99 0   - - error (invalid witness file) .51 .32 9.7 39 error (invalid witness file) 5.9 3.1 120 300
array-memsafety/cstrlen-alloca_true-valid-memsafety.i true 2 wit inspect 11   11   140 290 1.7  0   - - error (invalid witness file) .51 .33 9.1 39 error (invalid witness file) 6.0 3.2 120 300
array-memsafety/cstrncat-alloca_true-valid-memsafety.i true 2 wit inspect 890   900   12000 3100 1.7  0   - - error (invalid witness file) .48 .31 7.3 39 error (invalid witness file) 6.1 3.2 120 300
array-memsafety/cstrncmp-alloca_true-valid-memsafety.i true 2 wit inspect 210   210   2700 3700 1.7  0   - - error (invalid witness file) .54 .36 5.1 41 error (invalid witness file) 6.3 3.3 120 300
array-memsafety/cstrncpy-alloca_true-valid-memsafety.i out of memory 0 wit inspect 170   170   1900 15000 2.0  0   - - error (invalid witness file) .59 .37 9.9 41 error (invalid witness file) 6.9 3.6 130 320
array-memsafety/cstrpbrk-alloca_true-valid-memsafety.i timeout 0 wit inspect 900   900   7900 10000 .84 0   - - error (invalid witness file) .50 .35 3.4 40 error (invalid witness file) 5.7 3.1 120 290
array-memsafety/cstrspn-alloca_true-valid-memsafety.i timeout 0 wit inspect 900   900   11000 10000 .99 0   - - error (invalid witness file) .48 .31 6.1 39 error (invalid witness file) 6.1 3.2 120 300
array-memsafety/diff-alloca_true-valid-memsafety.i timeout 0 wit inspect 900   900   11000 12000 .84 0   - - error (invalid witness file) .50 .31 11   40 error (invalid witness file) 6.6 3.5 130 310
array-memsafety/insertionsort-alloca_true-valid-memsafety.i timeout 0 wit inspect 900   900   8100 8300 .84 0   - - error (invalid witness file) .52 .34 13   40 error (invalid witness file) 6.7 3.5 130 310
array-memsafety/java_BubbleSort-alloca_true-valid-memsafety.i out of memory 0 wit inspect 550   550   2600 15000 .99 0   - - error (invalid witness file) .52 .35 4.1 43 error (invalid witness file) 6.0 3.1 110 290
array-memsafety/lis-alloca_true-valid-memsafety.i out of memory 0 wit inspect 150   150   400 15000 .99 0   - - error (invalid witness file) .53 .35 4.1 39 error (invalid witness file) 6.2 3.2 120 300
array-memsafety/mult_array-alloca_true-valid-memsafety.i true 2 wit inspect 25   25   260 1300 2.0  0   - - error (invalid witness file) .52 .34 11   40 error (invalid witness file) 5.7 3.1 110 290
array-memsafety/openbsd_cbzero-alloca_true-valid-memsafety.i true 2 wit inspect 5.2 5.2 57 450 2.0  0   - - error (invalid witness file) .53 .34 12   40 error (invalid witness file) 6.7 3.5 140 300
array-memsafety/openbsd_cmemchr-alloca_true-valid-memsafety.i true 2 wit inspect 42   42   130 1000 2.0  0   - - error (invalid witness file) .49 .32 6.8 39 error (invalid witness file) 7.2 3.8 130 330
array-memsafety/openbsd_cmemrchr-alloca_true-valid-memsafety.i unknown 0 wit inspect 5.9 5.9 83 840 2.0  0   - - error (invalid witness file) .52 .34 7.2 45 error (invalid witness file) 6.3 3.4 120 300
array-memsafety/openbsd_cmemset-alloca_true-valid-memsafety.i true 2 wit inspect 4.9 4.9 64 410 1.7  0   - - error (invalid witness file) .50 .33 10   39 error (invalid witness file) 6.4 3.3 120 300
array-memsafety/openbsd_cstpcpy-alloca_true-valid-memsafety.i true 2 wit inspect 20   20   210 760 2.0  0   - - error (invalid witness file) .51 .33 10   40 error (invalid witness file) 5.8 3.1 110 290
array-memsafety/openbsd_cstpncpy-alloca_true-valid-memsafety.i out of memory 0 wit inspect 170   170   2200 15000 2.0  0   - - error (invalid witness file) .51 .32 12   39 error (invalid witness file) 6.2 3.3 120 300
array-memsafety/openbsd_cstrcat-alloca_true-valid-memsafety.i true 2 wit inspect 380   380   4000 1600 2.0  0   - - error (invalid witness file) .50 .33 12   39 error (invalid witness file) 6.0 3.2 120 300
array-memsafety/openbsd_cstrcmp-alloca_true-valid-memsafety.i true 2 wit inspect 84   84   1000 2300 2.0  0   - - error (invalid witness file) .48 .32 5.3 39 error (invalid witness file) 6.4 3.4 130 300
array-memsafety/openbsd_cstrcpy-alloca_true-valid-memsafety.i true 2 wit inspect 20   20   240 760 1.7  0   - - error (invalid witness file) .49 .35 11   41 error (invalid witness file) 6.4 3.3 120 310
array-memsafety/openbsd_cstrcspn-alloca_true-valid-memsafety.i timeout 0 wit inspect 900   900   6600 14000 .99 0   - - error (invalid witness file) .52 .35 10   39 error (invalid witness file) 6.1 3.2 130 300
array-memsafety/openbsd_cstrlcpy-alloca_true-valid-memsafety.i true 2 wit inspect 890   890   8600 4400 2.0  0   - - error (invalid witness file) .53 .34 10   41 error (invalid witness file) 5.9 3.2 120 300
array-memsafety/openbsd_cstrlen-alloca_true-valid-memsafety.i true 2 wit inspect 46   46   91 290 1.8  0   - - error (invalid witness file) .58 .37 9.5 43 error (invalid witness file) 5.4 2.9 86 300
array-memsafety/openbsd_cstrncat-alloca_true-valid-memsafety.i true 2 wit inspect 680   680   9400 2700 1.7  0   - - error (invalid witness file) .47 .32 4.3 39 error (invalid witness file) 6.3 3.3 130 300
array-memsafety/openbsd_cstrncmp-alloca_true-valid-memsafety.i true 2 wit inspect 100   100   1400 4700 2.0  0   - - error (invalid witness file) .52 .33 14   41 error (invalid witness file) 5.7 3.0 110 300
array-memsafety/openbsd_cstrncpy-alloca_true-valid-memsafety.i out of memory 0 wit inspect 170   170   2200 15000 1.7  0   - - error (invalid witness file) .50 .32 6.3 39 error (invalid witness file) 5.3 2.9 91 290
array-memsafety/openbsd_cstrnlen-alloca_true-valid-memsafety.i true 2 wit inspect 13   13   180 340 2.0  0   - - error (invalid witness file) .52 .34 7.4 39 error (invalid witness file) 6.3 3.3 120 300
array-memsafety/openbsd_cstrpbrk-alloca_true-valid-memsafety.i timeout 0 wit inspect 900   900   7200 9700 .84 0   - - error (invalid witness file) .50 .32 9.7 39 error (invalid witness file) 6.0 3.2 120 300
array-memsafety/openbsd_cstrspn-alloca_true-valid-memsafety.i out of memory 0 wit inspect 38   37   460 15000 .99 0   - - error (invalid witness file) .49 .32 11   40 error (invalid witness file) 6.5 3.4 130 300
array-memsafety/openbsd_cstrstr-alloca_true-valid-memsafety.i out of memory 0 wit inspect 45   45   530 15000 .84 0   - - error (invalid witness file) .51 .33 8.3 40 error (invalid witness file) 6.1 3.2 120 300
array-memsafety/rec_strlen-alloca_true-valid-memsafety.i true 2 wit inspect 15   15   180 510 2.0  0   - - error (invalid witness file) .51 .33 10   40 error (invalid witness file) 5.9 3.2 120 300
array-memsafety/selectionsort-alloca_true-valid-memsafety.i timeout 0 wit inspect 900   900   6400 12000 .99 0   - - error (invalid witness file) .52 .34 13   42 error (invalid witness file) 6.0 3.2 130 300
array-memsafety/stroeder1-alloca_true-valid-memsafety.i true 2 wit inspect 4.3 4.3 50 400 1.8  0   - - error (invalid witness file) .50 .31 12   39 error (invalid witness file) 5.9 3.1 110 290
array-memsafety/stroeder2-alloca_true-valid-memsafety.i timeout 0 wit inspect 900   900   1800 14000 .99 0   - - error (invalid witness file) .51 .34 9.6 41 error (invalid witness file) 6.8 3.6 140 310
array-memsafety/strreplace-alloca_true-valid-memsafety.i timeout 0 wit inspect 900   900   11000 1000 .84 0   - - error (invalid witness file) .51 .33 9.4 40 error (invalid witness file) 6.4 3.4 130 310
array-memsafety/subseq-alloca_true-valid-memsafety.i true 2 wit inspect 890   890   9400 2200 1.7  0   - - error (invalid witness file) .50 .33 12   39 error (invalid witness file) 5.8 3.1 100 300
array-memsafety/substring-alloca_true-valid-memsafety.i out of memory 0 wit inspect 41   41   560 15000 .84 0   - - error (invalid witness file) .53 .34 14   42 error (invalid witness file) 5.8 3.1 120 300
array-examples/relax_false-valid-deref.i false(valid-deref) 1 wit inspect 900   900   1900 5400 2.0  0   error (invalid witness file) .51 .32 9.2 39 error (invalid witness file) 6.7 3.5 120 310 - -
array-examples/sanfoundry_24_false-valid-deref.i true -32 wit inspect 61   61   120 590 1.7  0   error (invalid witness file) .51 .32 11   39 error (invalid witness file) 5.9 3.2 110 300 - -
array-examples/standard_strcpy_false-valid-deref_ground.i true -32 wit inspect 5.4 5.4 63 620 2.0  0   error (invalid witness file) .50 .32 9.2 40 error (invalid witness file) 5.5 3.0 110 290 - -
array-examples/standard_strcpy_original_false-valid-deref.i true -32 wit inspect 5.4 5.4 65 620 2.0  0   error (invalid witness file) .54 .36 9.8 40 error (invalid witness file) 6.0 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 -39 26000 26000 240000 440000 100   0   69 11   6.8  190 840   69 130 67   2500 6300   69 25 16   450 1900   69 290 160 5800 14000  
    correct results 33 57 8000 8000 78000 61000 62   0   0 4.5 2.9  69 360   0 55 29   1100 2700   0 12 8.1 230 960   0 150 78 2900 7200  
        correct true 24 48 6000 6000 67000 39000 45   0   0 0   0    0 0   0 0 0   0 0   0 12 8.1 230 960   0 150 78 2900 7200  
        correct false 9 9 2000 2000 11000 22000 17   0   0 4.5 2.9  69 360   0 55 29   1100 2700   0 0 0   0 0   0 0 0 0 0  
    correct-unconfimed results 0
        correct-unconfirmed true 0
        correct-unconfirmed false 0
    incorrect results 3 -96 72 72 250 1800 5.6 0   0 1.5 1.0  30 120   0 17 9.3 360 890   0 0 0   0 0   0 0 0 0 0  
        incorrect true 3 -96 72 72 250 1800 5.6 0   0 1.5 1.0  30 120   0 17 9.3 360 890   0 0 0   0 0   0 0 0 0 0  
        incorrect false 0
score (69 tasks, max score: 117) -39
Run set sv-comp17.MemSafety-Arrays