Tool 2LS 0.5.0
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 09:48:02 CET [[ 2017-01-14 21:34:09 CET ]] [[ 2017-01-14 21:49:16 CET ]] [[ 2017-01-14 21:34:25 CET ]] [[ 2017-01-14 21:52:20 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/2ls.2017-01-11_0948.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/2ls.2017-01-11_0948.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/2ls.2017-01-11_0948.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/2ls.2017-01-11_0948.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 error (8) 0 wit inspect .19 .19 1.4  26 .0082 0    error (invalid witness file) .62 .40 7.6 39 error (invalid witness file) 7.6 4.0 83 300 - -
array-memsafety/bubblesort_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .13 .14 .87 25 0      1.9  error 3.1  1.7  55   250 false(valid-deref) 9.1 4.8 130 330 - -
array-memsafety/count_down_unsafe_false-valid-deref.i error (8) 0 wit inspect .17 .17 1.4  26 .0082 0    error (invalid witness file) .49 .31 11   40 error (invalid witness file) 6.9 3.6 89 300 - -
array-memsafety/cstrcat_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .13 .13 .86 23 0      0    false(valid-deref) 3.6  2.0  36   240 false(valid-deref) 10   5.4 97 360 - -
array-memsafety/cstrchr_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .12 .12 1.2  25 0      0    true 4.5  2.6  61   260 false(valid-deref) 20   11   210 510 - -
array-memsafety/cstrlen_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .19 .19 1.4  26 .0082 0    error 4.9  2.7  94   260 true 9.7 5.2 100 350 - -
array-memsafety/cstrncat_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .11 .10 1.2  23 0      0    error 3.1  1.7  53   250 false(valid-deref) 9.3 5.0 110 310 - -
array-memsafety/cstrncpy_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .10 .10 .91 23 0      0    error 3.3  1.8  77   250 false(valid-deref) 9.4 5.0 93 320 - -
array-memsafety/cstrpbrk_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .12 .11 1.3  26 0      0    error 3.8  2.1  61   250 true 8.7 4.6 150 330 - -
array-memsafety/diff_usafe_false-valid-deref.i false(valid-deref) 1 wit inspect .12 .11 1.1  23 0      0    error 3.5  2.0  82   260 false(valid-deref) 7.6 4.0 130 320 - -
array-memsafety/knapsack_alloca_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .22 .22 2.6  30 .0082 2.2  error 5.4  2.9  69   270 false(valid-deref) 12   6.3 190 370 - -
array-memsafety/lis_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .29 .28 2.8  34 .0082 0    error 5.0  2.7  68   270 false(valid-deref) 16   8.7 170 410 - -
array-memsafety/mult_array_unsafe_false-valid-deref.i error (8) 0 wit inspect .19 .19 1.4  28 .0082 0    error (invalid witness file) .53 .33 12   41 error (invalid witness file) 5.7 3.1 110 300 - -
array-memsafety/reverse_array_alloca_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .27 .26 2.7  33 .0082 0    error 4.6  2.5  92   270 false(valid-deref) 9.5 5.1 180 350 - -
array-memsafety/reverse_array_unsafe_false-valid-deref.i error (8) 0 wit inspect .21 .25 1.9  38 .0082 12    error (invalid witness file) .56 .35 11   42 error (invalid witness file) 7.7 4.1 77 300 - -
array-memsafety/selectionsort_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .15 .14 .95 26 0      .16 error 3.4  1.9  63   260 false(valid-deref) 11   5.7 110 340 - -
array-memsafety/stroeder1_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .12 .12 .79 22 0      0    error 3.1  1.8  54   250 false(valid-deref) 8.5 4.5 100 320 - -
array-memsafety/add_last-alloca_true-valid-memsafety.i false(valid-deref) -16 wit inspect .27 .27 2.6  31 .0082 0    - - error 4.8  2.6  72   260 true 20   11   230 560
array-memsafety/array01-alloca_true-valid-memsafety.i true 2 wit inspect .37 .37 3.7  28 .0082 0    - - error 3.9  2.1  75   250 timeout 960   810   16000 2400
array-memsafety/array02-alloca_true-valid-memsafety.i true 2 wit inspect .47 .47 5.3  30 .0082 0    - - error 4.7  2.5  48   250 timeout 960   820   24000 2400
array-memsafety/array03-alloca_true-valid-memsafety.i true 2 wit inspect .38 .37 3.7  29 .0082 0    - - error 4.0  2.2  60   260 false(unreach-call) 11   6.0 110 340
array-memsafety/bubblesort-alloca_true-valid-memsafety.i timeout 0 wit inspect 900    900    5300    13000 .0082 0    - - error (invalid witness file) .47 .31 9.8 41 error (invalid witness file) 6.6 3.5 77 290
array-memsafety/count_down-alloca_true-valid-memsafety.i true 2 wit inspect .55 .55 5.7  30 .0082 0    - - error 4.8  2.6  56   260 false(unreach-call) 8.3 4.5 120 320
array-memsafety/cstrcat-alloca_true-valid-memsafety.i false(valid-deref) -16 wit inspect .26 .26 2.4  29 .0082 .10 - - error 4.6  2.5  62   260 true 35   21   590 710
array-memsafety/cstrchr-alloca_true-valid-memsafety.i false(valid-deref) -16 wit inspect .22 .21 1.8  26 .0082 0    - - error 5.2  2.9  37   260 true 20   12   220 560
array-memsafety/cstrcmp-alloca_true-valid-memsafety.i false(valid-deref) -16 wit inspect .26 .25 2.2  27 .0082 .17 - - error 4.2  2.3  75   260 true 27   19   350 540
array-memsafety/cstrcpy-alloca_true-valid-memsafety.i false(valid-deref) -16 wit inspect .24 .24 2.5  28 .0082 0    - - error 4.3  2.4  82   260 true 25   15   290 610
array-memsafety/cstrcspn-alloca_true-valid-memsafety.i false(valid-deref) -16 wit inspect .37 .36 3.3  33 .0082 .16 - - error 4.7  2.5  73   260 true 26   17   450 560
array-memsafety/cstrlen-alloca_true-valid-memsafety.i false(valid-deref) -16 wit inspect .21 .20 1.7  26 .0082 0    - - error 4.4  2.4  68   260 true 20   11   260 520
array-memsafety/cstrncat-alloca_true-valid-memsafety.i false(valid-deref) -16 wit inspect .45 .45 4.7  32 .0082 .27 - - error 4.5  2.4  66   260 true 25   16   600 640
array-memsafety/cstrncmp-alloca_true-valid-memsafety.i false(valid-deref) -16 wit inspect .32 .32 3.1  29 .0082 .10 - - error 4.3  2.4  56   260 true 42   31   1100 640
array-memsafety/cstrncpy-alloca_true-valid-memsafety.i false(valid-deref) -16 wit inspect 1.9  1.9  22    120 .0082 .10 - - error 4.5  2.4  54   260 true 60   37   710 830
array-memsafety/cstrpbrk-alloca_true-valid-memsafety.i false(valid-deref) -16 wit inspect .34 .37 3.7  46 .0082 12    - - error 4.9  2.7  49   270 true 29   21   730 540
array-memsafety/cstrspn-alloca_true-valid-memsafety.i false(valid-deref) -16 wit inspect .33 .33 3.7  33 .0082 0    - - error 4.6  2.5  81   260 true 29   20   540 540
array-memsafety/diff-alloca_true-valid-memsafety.i timeout 0 wit inspect 900    900    5200    6200 .0082 0    - - error (invalid witness file) .49 .32 11   39 error (invalid witness file) 6.2 3.3 120 310
array-memsafety/insertionsort-alloca_true-valid-memsafety.i out of memory 0 wit inspect 750    750    5200    15000 .0082 0    - - error (invalid witness file) .50 .33 10   39 error (invalid witness file) 5.9 3.1 110 300
array-memsafety/java_BubbleSort-alloca_true-valid-memsafety.i true 2 wit inspect .52 .51 5.9  30 .0082 .10 - - error 4.5  2.5  50   250 false(unreach-call) 9.6 5.2 110 320
array-memsafety/lis-alloca_true-valid-memsafety.i timeout 0 wit inspect 900    900    10000    340 .0082 0    - - error (invalid witness file) .50 .33 11   40 error (invalid witness file) 7.5 4.0 71 290
array-memsafety/mult_array-alloca_true-valid-memsafety.i timeout 0 wit inspect 900    900    10000    190 .0082 0    - - error (invalid witness file) .50 .31 11   41 error (invalid witness file) 7.8 4.1 69 300
array-memsafety/openbsd_cbzero-alloca_true-valid-memsafety.i timeout 0 wit inspect 900    900    8800    11000 .0082 0    - - error (invalid witness file) .57 .36 9.8 39 error (invalid witness file) 6.5 3.4 120 310
array-memsafety/openbsd_cmemchr-alloca_true-valid-memsafety.i timeout 0 wit inspect 900    900    9700    3400 .0082 0    - - error (invalid witness file) .49 .31 8.8 40 error (invalid witness file) 6.2 3.3 100 300
array-memsafety/openbsd_cmemrchr-alloca_true-valid-memsafety.i false(valid-deref) -16 wit inspect .18 .18 1.5  26 .0082 .16 - - error 4.1  2.2  36   260 true 20   12   360 510
array-memsafety/openbsd_cmemset-alloca_true-valid-memsafety.i error (8) 0 wit inspect .19 .19 1.5  26 .0082 0    - - error (invalid witness file) .55 .34 12   41 error (invalid witness file) 7.0 3.7 78 290
array-memsafety/openbsd_cstpcpy-alloca_true-valid-memsafety.i false(valid-deref) -16 wit inspect .27 .27 2.4  28 .0082 0    - - error 4.7  2.6  74   260 true 21   12   360 560
array-memsafety/openbsd_cstpncpy-alloca_true-valid-memsafety.i false(valid-deref) -16 wit inspect 2.5  2.5  24    120 .0082 0    - - error 5.5  3.0  57   270 true 57   37   850 880
array-memsafety/openbsd_cstrcat-alloca_true-valid-memsafety.i false(valid-deref) -16 wit inspect .23 .23 3.0  28 .0082 0    - - error 4.2  2.3  65   260 true 30   18   600 700
array-memsafety/openbsd_cstrcmp-alloca_true-valid-memsafety.i false(valid-deref) -16 wit inspect .29 .29 2.5  31 .0082 2.2  - - error 4.4  2.4  70   270 true 39   28   850 710
array-memsafety/openbsd_cstrcpy-alloca_true-valid-memsafety.i false(valid-deref) -16 wit inspect .23 .23 2.4  28 .0082 0    - - error 4.3  2.3  62   260 true 23   13   260 540
array-memsafety/openbsd_cstrcspn-alloca_true-valid-memsafety.i false(valid-deref) -16 wit inspect .31 .31 3.0  30 .0082 0    - - error 5.2  2.8  55   260 true 33   21   470 660
array-memsafety/openbsd_cstrlcpy-alloca_true-valid-memsafety.i false(valid-deref) -16 wit inspect .36 .35 3.6  30 .0082 0    - - error 4.2  2.3  33   260 true 37   23   690 710
array-memsafety/openbsd_cstrlen-alloca_true-valid-memsafety.i false(valid-deref) -16 wit inspect .21 .20 1.8  26 .0082 0    - - error 4.3  2.4  90   260 true 17   9.6 300 550
array-memsafety/openbsd_cstrncat-alloca_true-valid-memsafety.i false(valid-deref) -16 wit inspect .43 .42 4.2  32 .0082 .16 - - error 4.2  2.3  72   270 true 39   27   750 720
array-memsafety/openbsd_cstrncmp-alloca_true-valid-memsafety.i false(valid-deref) -16 wit inspect .32 .32 3.4  31 .0082 0    - - error 4.6  2.5  87   260 true 33   23   670 610
array-memsafety/openbsd_cstrncpy-alloca_true-valid-memsafety.i false(valid-deref) -16 wit inspect 2.1  2.1  25    120 .0082 .16 - - error 4.4  2.4  50   260 true 44   27   670 750
array-memsafety/openbsd_cstrnlen-alloca_true-valid-memsafety.i false(valid-deref) -16 wit inspect .32 .32 2.9  28 .0082 0    - - error 4.2  2.3  70   270 true 19   11   390 530
array-memsafety/openbsd_cstrpbrk-alloca_true-valid-memsafety.i false(valid-deref) -16 wit inspect .42 .43 6.0  37 .0082 2.4  - - error 4.1  2.2  55   260 true 8.1 4.3 150 330
array-memsafety/openbsd_cstrspn-alloca_true-valid-memsafety.i timeout 0 wit inspect 900    900    11000    27 .0082 0    - - error (invalid witness file) .55 .35 9.7 39 error (invalid witness file) 6.7 3.5 100 300
array-memsafety/openbsd_cstrstr-alloca_true-valid-memsafety.i timeout 0 wit inspect 900    900    13000    27 .0082 0    - - error (invalid witness file) .53 .34 11   41 error (invalid witness file) 6.0 3.2 91 300
array-memsafety/rec_strlen-alloca_true-valid-memsafety.i error (5) 0 wit inspect .20 .24 1.8  38 .0082 12    - - error (invalid witness file) .49 .30 10   39 error (invalid witness file) 6.4 3.4 100 310
array-memsafety/selectionsort-alloca_true-valid-memsafety.i out of memory 0 wit inspect 510    510    3600    15000 .0082 0    - - error (invalid witness file) .68 .44 8.8 42 error (invalid witness file) 6.1 3.2 130 300
array-memsafety/stroeder1-alloca_true-valid-memsafety.i timeout 0 wit inspect 900    900    8100    5700 .0082 1.8  - - error (invalid witness file) .52 .34 9.7 39 error (invalid witness file) 5.3 2.8 120 280
array-memsafety/stroeder2-alloca_true-valid-memsafety.i error (8) 0 wit inspect .17 .17 1.6  26 .0082 0    - - error (invalid witness file) .50 .33 10   41 error (invalid witness file) 7.6 4.0 81 310
array-memsafety/strreplace-alloca_true-valid-memsafety.i false(valid-deref) -16 wit inspect .32 .32 3.1  29 .0082 0    - - error 4.3  2.4  95   260 true 17   9.4 160 490
array-memsafety/subseq-alloca_true-valid-memsafety.i false(valid-deref) -16 wit inspect .24 .24 2.6  27 .0082 .17 - - error 4.4  2.4  47   260 true 9.5 5.1 130 350
array-memsafety/substring-alloca_true-valid-memsafety.i false(valid-deref) -16 wit inspect .25 .24 2.5  29 .0082 0    - - error 5.1  2.8  46   260 true 52   37   800 680
array-examples/relax_false-valid-deref.i false(valid-deref) 1 wit inspect .23 .23 2.2  27 .0082 .17 error 4.4  2.4  92   270 false(valid-deref) 11   5.8 120 330 - -
array-examples/sanfoundry_24_false-valid-deref.i out of memory 0 wit inspect 320    320    2800    15000 0      0    error (invalid witness file) .54 .34 11   42 error (invalid witness file) 6.4 3.4 94 300 - -
array-examples/standard_strcpy_false-valid-deref_ground.i timeout 0 wit inspect 900    900    10000    14000 0      0    error (invalid witness file) .52 .33 9.7 41 error (invalid witness file) 7.6 4.0 75 300 - -
array-examples/standard_strcpy_original_false-valid-deref.i timeout 0 wit inspect 900    900    9800    14000 0      0    error (invalid witness file) .63 .40 7.5 39 error (invalid witness file) 6.1 3.2 120 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 -440 12000   12000   110000 110000 .47  49    69 60 33 1000 3900   69 200 110 2500 7100   69 160 88 2300 9400   69 2900 2200 55000 28000  
    correct results 19 24 4.6 4.5 45 510 .082 4.6  2 56 31 960 3600   14 150 82 1900 4900   0 22 12 290 1300   3 2000 1600 40000 5800  
        correct true 5 10 2.3 2.3 24 150 .041 .10 1 0 0 0 0   2 0 0 0 0   0 22 12 290 1300   0 2000 1600 40000 5800  
        correct false 14 14 2.3 2.2 21 360 .041 4.5  1 56 31 960 3600   12 150 82 1900 4900   0 0 0 0 0   3 0 0 0 0  
    correct-unconfimed results 0
        correct-unconfirmed true 0
        correct-unconfirmed false 0
    incorrect results 29 -464 14   14   150 1100 .24  19    0 0 0 0 0   0 0 0 0 0   0 130 72 1800 7600   29 860 550 14000 18000  
        incorrect true 0
        incorrect false 29 -464 14   14   150 1100 .24  19    0 0 0 0 0   0 0 0 0 0   0 130 72 1800 7600   0 860 550 14000 18000  
score (69 tasks, max score: 117) -440
Run set sv-comp17.MemSafety-Arrays