Tool SMACK+Corral 1.7.2
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-14 05:56:27 CET [[ 2017-01-15 04:08:20 CET ]] [[ 2017-01-15 04:18:47 CET ]] [[ 2017-01-15 04:12:29 CET ]] [[ 2017-01-15 04:25:58 CET ]]
Run set sv-comp17.MemSafety-Arrays
Options -w error-witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/smack.2017-01-14_0556.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/smack.2017-01-14_0556.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/smack.2017-01-14_0556.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/smack.2017-01-14_0556.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 1.8 1.8 22 79 1.2 0      error (invalid witness file) .49 .33 9.5 40 error (invalid witness file) 6.4 3.4 110 290 - -
array-memsafety/bubblesort_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 1.9 1.8 24 73 1.2 0      error (invalid witness file) .55 .35 11   43 error (invalid witness file) 6.7 3.5 120 320 - -
array-memsafety/count_down_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 1.9 1.8 25 79 1.2 0      error (invalid witness file) .49 .32 8.9 40 error (invalid witness file) 6.6 3.5 140 300 - -
array-memsafety/cstrcat_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 1.8 1.8 23 86 1.2 0      error (invalid witness file) .54 .34 10   41 error (invalid witness file) 5.8 3.1 110 300 - -
array-memsafety/cstrchr_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 2.0 1.9 22 84 1.2 0      error (invalid witness file) .52 .34 12   40 error (invalid witness file) 6.1 3.3 100 300 - -
array-memsafety/cstrlen_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 1.9 1.9 26 84 1.2 0      error (invalid witness file) .49 .32 9.6 40 error (invalid witness file) 5.5 3.0 120 290 - -
array-memsafety/cstrncat_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 1.9 1.8 22 81 1.2 0      error (invalid witness file) .56 .36 8.8 39 error (invalid witness file) 5.3 2.9 110 290 - -
array-memsafety/cstrncpy_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 1.9 1.8 26 85 1.2 0      error (invalid witness file) .54 .33 9.9 40 error (invalid witness file) 5.9 3.1 100 300 - -
array-memsafety/cstrpbrk_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 2.2 2.2 25 85 1.2 0      error (invalid witness file) .46 .30 5.8 39 error (invalid witness file) 6.0 3.2 110 300 - -
array-memsafety/diff_usafe_false-valid-deref.i false(valid-deref) 1 wit inspect 1.8 1.8 25 80 1.2 0      error (invalid witness file) .55 .33 7.5 42 error (invalid witness file) 7.0 3.7 150 330 - -
array-memsafety/knapsack_alloca_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 2.0 2.0 24 86 1.3 0      error (invalid witness file) .53 .34 11   41 error (invalid witness file) 7.3 3.9 84 300 - -
array-memsafety/lis_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 2.2 2.2 27 95 1.3 0      error (invalid witness file) .50 .32 9.0 40 error (invalid witness file) 5.5 3.0 120 290 - -
array-memsafety/mult_array_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 1.9 1.8 24 82 1.3 0      error (invalid witness file) .53 .33 11   43 error (invalid witness file) 5.9 3.1 120 290 - -
array-memsafety/reverse_array_alloca_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 2.0 1.9 22 84 1.2 0      error (invalid witness file) .50 .31 4.2 41 error (invalid witness file) 5.6 3.0 85 290 - -
array-memsafety/reverse_array_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 1.9 1.8 28 81 1.2 0      error (invalid witness file) .56 .37 7.1 44 error (invalid witness file) 5.9 3.1 120 300 - -
array-memsafety/selectionsort_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 1.9 1.8 23 73 1.2 0      error (invalid witness file) .49 .32 7.0 39 error (invalid witness file) 5.8 3.1 110 300 - -
array-memsafety/stroeder1_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 1.8 1.8 21 82 1.2 0      error (invalid witness file) .51 .32 9.1 39 error (invalid witness file) 5.8 3.1 120 290 - -
array-memsafety/add_last-alloca_true-valid-memsafety.i true 2 wit inspect 750   750   8200 330 1.8 0      - - error (invalid witness file) .52 .33 12   40 error (invalid witness file) 5.8 3.1 110 300
array-memsafety/array01-alloca_true-valid-memsafety.i true 2 wit inspect 750   750   7800 500 1.8 0      - - error (invalid witness file) .52 .34 10   42 error (invalid witness file) 6.1 3.3 120 300
array-memsafety/array02-alloca_true-valid-memsafety.i true 2 wit inspect 760   750   7200 580 1.9 0      - - error (invalid witness file) .49 .33 4.0 40 error (invalid witness file) 6.0 3.2 130 300
array-memsafety/array03-alloca_true-valid-memsafety.i true 2 wit inspect 750   750   7000 390 1.9 0      - - error (invalid witness file) .53 .34 7.0 40 error (invalid witness file) 7.6 4.0 86 300
array-memsafety/bubblesort-alloca_true-valid-memsafety.i true 2 wit inspect 750   750   6600 510 1.9 0      - - error (invalid witness file) .50 .33 11   39 error (invalid witness file) 5.8 3.1 100 300
array-memsafety/count_down-alloca_true-valid-memsafety.i true 2 wit inspect 750   750   8500 210 1.9 0      - - error (invalid witness file) .51 .32 9.5 40 error (invalid witness file) 6.1 3.2 120 310
array-memsafety/cstrcat-alloca_true-valid-memsafety.i true 2 wit inspect 750   750   8800 280 1.9 0      - - error (invalid witness file) .48 .31 3.7 40 error (invalid witness file) 6.1 3.2 120 300
array-memsafety/cstrchr-alloca_true-valid-memsafety.i true 2 wit inspect 750   750   10000 170 1.8 0      - - error (invalid witness file) .51 .32 12   41 error (invalid witness file) 6.0 3.2 120 300
array-memsafety/cstrcmp-alloca_true-valid-memsafety.i true 2 wit inspect 750   750   8300 210 1.9 0      - - error (invalid witness file) .50 .32 12   39 error (invalid witness file) 6.1 3.2 140 310
array-memsafety/cstrcpy-alloca_true-valid-memsafety.i true 2 wit inspect 750   750   9100 220 1.8 0      - - error (invalid witness file) .58 .38 9.5 39 error (invalid witness file) 5.7 3.1 110 290
array-memsafety/cstrcspn-alloca_true-valid-memsafety.i true 2 wit inspect 750   750   7600 610 1.9 0      - - error (invalid witness file) .52 .34 4.5 40 error (invalid witness file) 6.2 3.3 120 300
array-memsafety/cstrlen-alloca_true-valid-memsafety.i true 2 wit inspect 750   750   9300 150 1.8 0      - - error (invalid witness file) .52 .35 11   39 error (invalid witness file) 6.4 3.4 130 300
array-memsafety/cstrncat-alloca_true-valid-memsafety.i true 2 wit inspect 750   750   8700 260 1.9 0      - - error (invalid witness file) .48 .31 5.2 39 error (invalid witness file) 6.0 3.2 110 290
array-memsafety/cstrncmp-alloca_true-valid-memsafety.i true 2 wit inspect 750   750   8000 240 1.9 .0041 - - error (invalid witness file) .50 .32 13   40 error (invalid witness file) 7.4 3.8 140 330
array-memsafety/cstrncpy-alloca_true-valid-memsafety.i true 2 wit inspect 750   750   7100 240 1.9 0      - - error (invalid witness file) .51 .34 8.9 39 error (invalid witness file) 5.9 3.2 110 300
array-memsafety/cstrpbrk-alloca_true-valid-memsafety.i true 2 wit inspect 750   750   6500 550 1.9 0      - - error (invalid witness file) .52 .33 11   40 error (invalid witness file) 6.0 3.2 120 300
array-memsafety/cstrspn-alloca_true-valid-memsafety.i true 2 wit inspect 750   750   6100 510 1.9 0      - - error (invalid witness file) .50 .32 7.0 41 error (invalid witness file) 6.2 3.3 110 300
array-memsafety/diff-alloca_true-valid-memsafety.i true 2 wit inspect 750   750   11000 150 1.9 0      - - error (invalid witness file) .52 .33 11   41 error (invalid witness file) 5.8 3.1 100 290
array-memsafety/insertionsort-alloca_true-valid-memsafety.i true 2 wit inspect 750   750   6100 440 1.9 0      - - error (invalid witness file) .49 .33 4.9 39 error (invalid witness file) 6.4 3.4 120 310
array-memsafety/java_BubbleSort-alloca_true-valid-memsafety.i true 2 wit inspect 750   750   8100 460 1.9 0      - - error (invalid witness file) .51 .33 10   40 error (invalid witness file) 5.8 3.1 110 300
array-memsafety/lis-alloca_true-valid-memsafety.i true 2 wit inspect 750   750   6500 350 2.0 0      - - error (invalid witness file) .51 .33 12   39 error (invalid witness file) 6.8 3.6 130 320
array-memsafety/mult_array-alloca_true-valid-memsafety.i true 2 wit inspect 750   750   7700 370 1.9 0      - - error (invalid witness file) .50 .32 8.7 40 error (invalid witness file) 6.1 3.3 120 300
array-memsafety/openbsd_cbzero-alloca_true-valid-memsafety.i true 2 wit inspect 750   750   11000 320 1.8 0      - - error (invalid witness file) .54 .36 8.3 41 error (invalid witness file) 6.0 3.2 100 310
array-memsafety/openbsd_cmemchr-alloca_true-valid-memsafety.i true 2 wit inspect 750   750   11000 410 1.8 0      - - error (invalid witness file) .55 .35 14   41 error (invalid witness file) 5.9 3.1 120 300
array-memsafety/openbsd_cmemrchr-alloca_true-valid-memsafety.i true 2 wit inspect 750   750   8900 450 1.8 0      - - error (invalid witness file) .49 .32 9.4 40 error (invalid witness file) 6.9 3.6 140 310
array-memsafety/openbsd_cmemset-alloca_true-valid-memsafety.i true 2 wit inspect 750   750   8400 410 1.8 0      - - error (invalid witness file) .52 .34 12   40 error (invalid witness file) 6.0 3.2 110 290
array-memsafety/openbsd_cstpcpy-alloca_true-valid-memsafety.i true 2 wit inspect 750   750   8500 270 1.8 0      - - error (invalid witness file) .50 .32 4.1 40 error (invalid witness file) 6.2 3.3 120 300
array-memsafety/openbsd_cstpncpy-alloca_true-valid-memsafety.i true 2 wit inspect 750   750   7100 230 1.9 0      - - error (invalid witness file) .49 .32 6.8 40 error (invalid witness file) 6.3 3.3 130 300
array-memsafety/openbsd_cstrcat-alloca_true-valid-memsafety.i true 2 wit inspect 750   750   8100 290 1.9 0      - - error (invalid witness file) .54 .35 14   42 error (invalid witness file) 6.2 3.3 120 300
array-memsafety/openbsd_cstrcmp-alloca_true-valid-memsafety.i true 2 wit inspect 750   750   8500 230 1.9 0      - - error (invalid witness file) .48 .30 7.9 40 error (invalid witness file) 6.3 3.3 110 310
array-memsafety/openbsd_cstrcpy-alloca_true-valid-memsafety.i true 2 wit inspect 750   750   9000 230 1.8 0      - - error (invalid witness file) .50 .32 9.9 40 error (invalid witness file) 5.3 2.9 110 280
array-memsafety/openbsd_cstrcspn-alloca_true-valid-memsafety.i true 2 wit inspect 750   750   8100 230 1.8 0      - - error (invalid witness file) .52 .33 10   42 error (invalid witness file) 6.1 3.3 120 300
array-memsafety/openbsd_cstrlcpy-alloca_true-valid-memsafety.i true 2 wit inspect 750   750   10000 250 1.9 0      - - error (invalid witness file) .47 .31 3.6 40 error (invalid witness file) 6.4 3.3 120 300
array-memsafety/openbsd_cstrlen-alloca_true-valid-memsafety.i true 2 wit inspect 750   750   9100 150 1.8 0      - - error (invalid witness file) .51 .35 4.0 42 error (invalid witness file) 6.1 3.2 120 300
array-memsafety/openbsd_cstrncat-alloca_true-valid-memsafety.i true 2 wit inspect 750   750   11000 260 1.9 0      - - error (invalid witness file) .54 .35 11   41 error (invalid witness file) 5.6 3.1 110 280
array-memsafety/openbsd_cstrncmp-alloca_true-valid-memsafety.i true 2 wit inspect 750   750   8400 210 1.9 0      - - error (invalid witness file) .53 .33 11   39 error (invalid witness file) 5.9 3.1 110 300
array-memsafety/openbsd_cstrncpy-alloca_true-valid-memsafety.i true 2 wit inspect 750   750   8800 230 1.9 0      - - error (invalid witness file) .51 .32 11   40 error (invalid witness file) 6.1 3.2 120 290
array-memsafety/openbsd_cstrnlen-alloca_true-valid-memsafety.i true 2 wit inspect 750   750   9300 180 1.8 0      - - error (invalid witness file) .57 .36 8.8 40 error (invalid witness file) 6.3 3.3 130 310
array-memsafety/openbsd_cstrpbrk-alloca_true-valid-memsafety.i true 2 wit inspect 750   750   6900 600 1.9 0      - - error (invalid witness file) .49 .31 10   39 error (invalid witness file) 6.1 3.2 130 300
array-memsafety/openbsd_cstrspn-alloca_true-valid-memsafety.i true 2 wit inspect 750   750   7500 320 1.9 0      - - error (invalid witness file) .52 .33 12   40 error (invalid witness file) 6.3 3.4 130 310
array-memsafety/openbsd_cstrstr-alloca_true-valid-memsafety.i timeout 0 wit inspect 750   930   7400 290 2.0 0      - - error (invalid witness file) .50 .33 12   39 error (invalid witness file) 6.0 3.2 110 290
array-memsafety/rec_strlen-alloca_true-valid-memsafety.i true 2 wit inspect 750   750   9200 240 1.8 0      - - error (invalid witness file) .49 .32 4.3 40 error (invalid witness file) 5.7 3.1 120 290
array-memsafety/selectionsort-alloca_true-valid-memsafety.i true 2 wit inspect 750   750   6600 470 1.9 0      - - error (invalid witness file) .53 .34 6.7 39 error (invalid witness file) 5.9 3.2 120 290
array-memsafety/stroeder1-alloca_true-valid-memsafety.i true 2 wit inspect 750   750   8200 180 1.8 0      - - error (invalid witness file) .51 .34 6.2 39 error (invalid witness file) 6.6 3.4 130 300
array-memsafety/stroeder2-alloca_true-valid-memsafety.i true 2 wit inspect 760   750   6000 660 1.9 0      - - error (invalid witness file) .51 .33 11   40 error (invalid witness file) 6.8 3.6 110 300
array-memsafety/strreplace-alloca_true-valid-memsafety.i true 2 wit inspect 750   750   9100 130 1.8 0      - - error (invalid witness file) .50 .32 12   40 error (invalid witness file) 6.4 3.5 110 300
array-memsafety/subseq-alloca_true-valid-memsafety.i true 2 wit inspect 750   750   8600 210 1.9 0      - - error (invalid witness file) .51 .32 12   39 error (invalid witness file) 6.2 3.3 110 300
array-memsafety/substring-alloca_true-valid-memsafety.i true 2 wit inspect 750   750   6600 510 1.9 0      - - error (invalid witness file) .53 .35 6.5 41 error (invalid witness file) 6.3 3.4 110 300
array-examples/relax_false-valid-deref.i true -32 wit inspect 750   750   8800 220 2.1 0      error (invalid witness file) .52 .33 12   39 error (invalid witness file) 5.8 3.1 87 300 - -
array-examples/sanfoundry_24_false-valid-deref.i false(valid-deref) 1 wit inspect 6.2 6.0 79 92 1.2 0      error (invalid witness file) .52 .33 13   40 error (invalid witness file) 5.5 3.0 110 290 - -
array-examples/standard_strcpy_false-valid-deref_ground.i false(valid-deref) 1 wit inspect 8.4 8.3 100 95 1.2 0      error (invalid witness file) .50 .32 9.4 39 error (invalid witness file) 6.2 3.3 100 300 - -
array-examples/standard_strcpy_original_false-valid-deref.i false(valid-deref) 1 wit inspect 11   11   160 100 1.2 0      error (invalid witness file) .49 .32 6.5 40 error (invalid witness file) 6.5 3.4 100 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 82 37000 37000 400000 18000 120   .0041 69 11    7.0  190 850   69 130   68   2300 6300   69 25 16 440 1900   69 300 160 5700 14000  
    correct results 67 114 35000 35000 390000 17000 110   .0041 0 10    6.6  180 810   0 120   65   2200 6000   0 24 16 430 1900   0 290 150 5600 14000  
        correct true 47 94 35000 35000 390000 15000 87   .0041 0 0    0    0 0   0 0   0   0 0   0 24 16 430 1900   0 290 150 5600 14000  
        correct false 20 20 58 58 750 1700 24   0      0 10    6.6  180 810   0 120   65   2200 6000   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 0
        correct-unconfirmed true 0
        correct-unconfirmed false 0
    incorrect results 1 -32 750 750 8800 220 2.1 0      0 .52 .33 12 39   0 5.8 3.1 87 300   0 0 0 0 0   0 0 0 0 0  
        incorrect true 1 -32 750 750 8800 220 2.1 0      0 .52 .33 12 39   0 5.8 3.1 87 300   0 0 0 0 0   0 0 0 0 0  
        incorrect false 0
score (69 tasks, max score: 117) 82
Run set sv-comp17.MemSafety-Arrays