Tool DepthK DepthK version 3.0 - Fri Jan 6 18:14:20 AMT 2017
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:51:53 CET [[ 2017-01-15 00:05:22 CET ]] [[ 2017-01-15 00:31:32 CET ]] [[ 2017-01-15 00:11:25 CET ]] [[ 2017-01-15 00:39:18 CET ]]
Run set sv-comp17.MemSafety-Arrays
Options [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/depthk.2017-01-13_0451.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/depthk.2017-01-13_0451.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/depthk.2017-01-13_0451.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/depthk.2017-01-13_0451.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 .50 .49 6.9 29 .99 0   4.6  2.5  92   260 7.7 4.2 120 330
array-memsafety/bubblesort_unsafe_false-valid-deref.i 1 .36 .36 3.8 28 .84 0   93    70    1000   4400 7.6 4.1 170 320
array-memsafety/count_down_unsafe_false-valid-deref.i 1 .55 .55 6.3 29 .84 0   4.1  2.2  44   260 9.1 4.8 130 340
array-memsafety/cstrcat_unsafe_false-valid-deref.i 1 .33 .32 4.1 28 .99 0   3.5  2.0  54   250 7.3 3.9 100 330
array-memsafety/cstrchr_unsafe_false-valid-deref.i 1 .36 .36 4.2 29 .84 0   4.8  2.6  72   260 8.6 4.7 110 360
array-memsafety/cstrlen_unsafe_false-valid-deref.i 1 .37 .37 4.3 29 .84 0   4.1  2.2  68   270 7.5 4.0 140 320
array-memsafety/cstrncat_unsafe_false-valid-deref.i 1 .36 .35 3.8 28 .99 0   3.3  1.9  63   260 8.3 4.4 170 330
array-memsafety/cstrncpy_unsafe_false-valid-deref.i 1 .36 .36 3.8 28 .99 0   3.5  2.0  61   260 8.0 4.3 100 310
array-memsafety/cstrpbrk_unsafe_false-valid-deref.i 1 .35 .35 4.5 29 .99 0   4.2  2.3  68   260 7.4 4.0 130 310
array-memsafety/diff_usafe_false-valid-deref.i 1 .35 .35 3.7 28 .84 0   95    75    1100   3900 7.5 4.1 110 330
array-memsafety/knapsack_alloca_unsafe_false-valid-deref.i 1 .88 .88 12   29 .84 0   5.5  2.9  49   260 16   9.0 210 440
array-memsafety/lis_unsafe_false-valid-deref.i 1 .73 .72 7.9 29 .99 0   5.2  2.8  55   270 11   5.7 130 370
array-memsafety/mult_array_unsafe_false-valid-deref.i 1 .64 .63 8.8 29 .99 0   4.8  2.6  59   260 8.8 4.8 160 350
array-memsafety/reverse_array_alloca_unsafe_false-valid-deref.i 1 1.8  1.8  25   29 4.0  0   4.4  2.4  51   260 8.2 4.5 130 350
array-memsafety/reverse_array_unsafe_false-valid-deref.i 1 .59 .58 8.1 29 .99 0   4.6  2.5  75   260 9.9 5.3 140 360
array-memsafety/selectionsort_unsafe_false-valid-deref.i 1 .36 .36 4.1 28 .99 0   3.8  2.1  67   260 8.6 4.5 150 330
array-memsafety/stroeder1_unsafe_false-valid-deref.i 1 .35 .35 3.9 27 .84 0   3.5  2.0  54   250 7.6 4.1 130 320
array-memsafety/add_last-alloca_true-valid-memsafety.i 0 900    900    2100   69 170    0   .54 .34 10   43 6.4 3.4 130 310
array-memsafety/array01-alloca_true-valid-memsafety.i 0 890    900    10000   280 20    0   .54 .34 9.2 41 6.2 3.3 130 300
array-memsafety/array02-alloca_true-valid-memsafety.i 0 890    900    9300   280 14    0   .52 .34 9.2 40 5.7 3.1 100 300
array-memsafety/array03-alloca_true-valid-memsafety.i 0 890    900    1700   280 17    0   .53 .33 12   40 6.8 3.5 140 310
array-memsafety/bubblesort-alloca_true-valid-memsafety.i 0 890    900    8600   310 20    0   .52 .34 11   40 6.0 3.2 130 310
array-memsafety/count_down-alloca_true-valid-memsafety.i 0 890    900    11000   300 23    0   .57 .36 6.7 40 5.8 3.1 100 300
array-memsafety/cstrcat-alloca_true-valid-memsafety.i 0 900    900    12000   84 250    0   .51 .33 13   42 6.1 3.3 120 300
array-memsafety/cstrchr-alloca_true-valid-memsafety.i 0 170    170    2400   46 260    0   .50 .32 11   40 6.4 3.4 140 300
array-memsafety/cstrcmp-alloca_true-valid-memsafety.i 0 39    39    520   35 86    0   .53 .33 9.8 40 6.2 3.3 120 310
array-memsafety/cstrcpy-alloca_true-valid-memsafety.i 0 140    140    1600   48 260    0   .53 .34 11   40 5.8 3.1 110 300
array-memsafety/cstrcspn-alloca_true-valid-memsafety.i 0 900    900    12000   170 72    0   .50 .33 13   39 5.7 3.1 120 290
array-memsafety/cstrlen-alloca_true-valid-memsafety.i 0 100    100    1300   30 300    0   .51 .32 13   39 6.2 3.3 120 300
array-memsafety/cstrncat-alloca_true-valid-memsafety.i 0 900    900    10000   150 100    0   .54 .34 13   43 6.3 3.3 110 290
array-memsafety/cstrncmp-alloca_true-valid-memsafety.i 0 62    62    870   79 86    0   .59 .37 11   41 5.8 3.2 120 300
array-memsafety/cstrncpy-alloca_true-valid-memsafety.i 0 900    890    11000   960 240    0   .58 .37 8.0 40 6.7 3.5 120 300
array-memsafety/cstrpbrk-alloca_true-valid-memsafety.i 0 900    900    11000   140 56    0   .54 .36 11   40 6.1 3.3 110 300
array-memsafety/cstrspn-alloca_true-valid-memsafety.i 0 900    900    12000   150 65    0   .49 .32 11   40 6.2 3.3 110 310
array-memsafety/diff-alloca_true-valid-memsafety.i 0 890    900    7800   180 37    0   .55 .36 11   39 6.0 3.2 110 300
array-memsafety/insertionsort-alloca_true-valid-memsafety.i 0 890    900    9000   180 25    0   .57 .37 7.8 40 6.7 3.5 130 310
array-memsafety/java_BubbleSort-alloca_true-valid-memsafety.i 0 890    900    8900   300 17    0   .54 .34 12   43 5.8 3.1 120 300
array-memsafety/lis-alloca_true-valid-memsafety.i 0 890    900    10000   190 20    0   .50 .33 12   39 5.9 3.1 120 300
array-memsafety/mult_array-alloca_true-valid-memsafety.i 0 320    320    3600   89 300    0   .53 .35 11   40 6.9 3.6 150 310
array-memsafety/openbsd_cbzero-alloca_true-valid-memsafety.i 0 100    100    1300   33 280    0   .55 .35 8.8 39 5.3 2.9 100 300
array-memsafety/openbsd_cmemchr-alloca_true-valid-memsafety.i 0 110    110    1300   43 260    0   .55 .35 9.7 39 6.0 3.2 120 300
array-memsafety/openbsd_cmemrchr-alloca_true-valid-memsafety.i 0 32    32    410   34 86    0   .48 .31 12   39 6.0 3.2 120 300
array-memsafety/openbsd_cmemset-alloca_true-valid-memsafety.i 0 93    93    1200   32 300    0   .52 .33 11   40 7.2 3.7 140 320
array-memsafety/openbsd_cstpcpy-alloca_true-valid-memsafety.i 0 130    130    2000   45 300    0   .49 .32 10   40 5.6 3.0 120 290
array-memsafety/openbsd_cstpncpy-alloca_true-valid-memsafety.i 0 900    890    13000   940 250    0   .53 .34 12   42 6.0 3.2 130 300
array-memsafety/openbsd_cstrcat-alloca_true-valid-memsafety.i 0 900    900    13000   85 250    0   .64 .40 8.2 40 6.2 3.3 130 300
array-memsafety/openbsd_cstrcmp-alloca_true-valid-memsafety.i 0 270    270    3800   81 300    0   .69 .43 8.2 41 6.4 3.4 120 320
array-memsafety/openbsd_cstrcpy-alloca_true-valid-memsafety.i 0 130    130    1600   45 300    0   .52 .33 11   43 5.6 3.0 110 300
array-memsafety/openbsd_cstrcspn-alloca_true-valid-memsafety.i 0 900    900    12000   1100 180    0   .50 .32 12   39 5.7 3.1 110 290
array-memsafety/openbsd_cstrlcpy-alloca_true-valid-memsafety.i 0 900    900    9500   95 200    0   .50 .33 8.8 40 5.9 3.2 130 290
array-memsafety/openbsd_cstrlen-alloca_true-valid-memsafety.i 0 390    390    760   30 260    0   .51 .33 12   40 6.2 3.3 120 300
array-memsafety/openbsd_cstrncat-alloca_true-valid-memsafety.i 0 900    900    11000   64 160    0   .52 .34 11   40 6.0 3.2 110 300
array-memsafety/openbsd_cstrncmp-alloca_true-valid-memsafety.i 0 220    220    2600   120 300    0   .53 .34 11   41 6.4 3.4 140 310
array-memsafety/openbsd_cstrncpy-alloca_true-valid-memsafety.i 0 900    890    10000   970 250    0   .55 .36 11   40 5.7 3.1 110 290
array-memsafety/openbsd_cstrnlen-alloca_true-valid-memsafety.i 0 110    110    1500   32 300    0   .48 .32 11   40 6.2 3.3 130 300
array-memsafety/openbsd_cstrpbrk-alloca_true-valid-memsafety.i 0 900    900    10000   370 130    0   .61 .39 9.4 42 5.6 3.0 110 290
array-memsafety/openbsd_cstrspn-alloca_true-valid-memsafety.i 0 890    900    9900   120 24    0   .50 .32 13   40 6.4 3.4 130 300
array-memsafety/openbsd_cstrstr-alloca_true-valid-memsafety.i 0 900    900    14000   590 31    0   .50 .32 12   39 6.2 3.3 130 300
array-memsafety/rec_strlen-alloca_true-valid-memsafety.i 2 1.1  1.1  13   29 3.4  0   4.9  2.7  52   260 25   18   320 520
array-memsafety/selectionsort-alloca_true-valid-memsafety.i 0 890    900    6500   310 26    0   .54 .34 11   41 6.2 3.3 110 300
array-memsafety/stroeder1-alloca_true-valid-memsafety.i 0 100    100    1400   53 260    0   .60 .38 7.9 39 6.2 3.3 120 300
array-memsafety/stroeder2-alloca_true-valid-memsafety.i 0 890    900    8800   270 28    0   .52 .33 11   41 5.9 3.2 120 300
array-memsafety/strreplace-alloca_true-valid-memsafety.i 0 890    900    10000   59 100    0   .47 .31 8.4 40 5.9 3.1 120 290
array-memsafety/subseq-alloca_true-valid-memsafety.i 0 890    900    13000   59 98    0   .51 .33 12   40 5.9 3.1 120 310
array-memsafety/substring-alloca_true-valid-memsafety.i 0 900    900    12000   220 63    0   .52 .32 8.7 41 6.4 3.3 140 300
array-examples/relax_false-valid-deref.i 1 .63 .62 7.4 29 .99 0   5.1  2.8  54   250 11   5.8 180 370
array-examples/sanfoundry_24_false-valid-deref.i 0 440    440    830   100 260    0   .51 .33 5.4 42 6.2 3.3 93 300
array-examples/standard_strcpy_false-valid-deref_ground.i 0 67    66    920   31 300    0   .63 .40 7.3 41 6.1 3.2 120 300
array-examples/standard_strcpy_original_false-valid-deref.i 0 67    66    710   31 300    0   .60 .39 8.3 40 6.9 3.6 94 310
../../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 20 30000   30000   330000 11000 8000   0   69 260 180 3200 13000   69 180 96 2800 7100   69 30   19   550 2100   69 310 170 6000 15000  
    correct results 19 20 11   11   130 540 23   0   11 260 180 3100 12000   18 160 86 2500 6200   0 4.9 2.7 52 260   1 25 18 320 520  
        correct true 1 2 1.1 1.1 13 29 3.4 0   7 0 0 0 0   13 0 0 0 0   0 4.9 2.7 52 260   1 25 18 320 520  
        correct false 18 18 9.9 9.8 120 510 20   0   4 260 180 3100 12000   5 160 86 2500 6200   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) 20
Run set sv-comp17.MemSafety-Arrays