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 1 1.8 1.8 22 79 1.2 0      .49 .33 9.5 40 6.4 3.4 110 290
array-memsafety/bubblesort_unsafe_false-valid-deref.i 1 1.9 1.8 24 73 1.2 0      .55 .35 11   43 6.7 3.5 120 320
array-memsafety/count_down_unsafe_false-valid-deref.i 1 1.9 1.8 25 79 1.2 0      .49 .32 8.9 40 6.6 3.5 140 300
array-memsafety/cstrcat_unsafe_false-valid-deref.i 1 1.8 1.8 23 86 1.2 0      .54 .34 10   41 5.8 3.1 110 300
array-memsafety/cstrchr_unsafe_false-valid-deref.i 1 2.0 1.9 22 84 1.2 0      .52 .34 12   40 6.1 3.3 100 300
array-memsafety/cstrlen_unsafe_false-valid-deref.i 1 1.9 1.9 26 84 1.2 0      .49 .32 9.6 40 5.5 3.0 120 290
array-memsafety/cstrncat_unsafe_false-valid-deref.i 1 1.9 1.8 22 81 1.2 0      .56 .36 8.8 39 5.3 2.9 110 290
array-memsafety/cstrncpy_unsafe_false-valid-deref.i 1 1.9 1.8 26 85 1.2 0      .54 .33 9.9 40 5.9 3.1 100 300
array-memsafety/cstrpbrk_unsafe_false-valid-deref.i 1 2.2 2.2 25 85 1.2 0      .46 .30 5.8 39 6.0 3.2 110 300
array-memsafety/diff_usafe_false-valid-deref.i 1 1.8 1.8 25 80 1.2 0      .55 .33 7.5 42 7.0 3.7 150 330
array-memsafety/knapsack_alloca_unsafe_false-valid-deref.i 1 2.0 2.0 24 86 1.3 0      .53 .34 11   41 7.3 3.9 84 300
array-memsafety/lis_unsafe_false-valid-deref.i 1 2.2 2.2 27 95 1.3 0      .50 .32 9.0 40 5.5 3.0 120 290
array-memsafety/mult_array_unsafe_false-valid-deref.i 1 1.9 1.8 24 82 1.3 0      .53 .33 11   43 5.9 3.1 120 290
array-memsafety/reverse_array_alloca_unsafe_false-valid-deref.i 1 2.0 1.9 22 84 1.2 0      .50 .31 4.2 41 5.6 3.0 85 290
array-memsafety/reverse_array_unsafe_false-valid-deref.i 1 1.9 1.8 28 81 1.2 0      .56 .37 7.1 44 5.9 3.1 120 300
array-memsafety/selectionsort_unsafe_false-valid-deref.i 1 1.9 1.8 23 73 1.2 0      .49 .32 7.0 39 5.8 3.1 110 300
array-memsafety/stroeder1_unsafe_false-valid-deref.i 1 1.8 1.8 21 82 1.2 0      .51 .32 9.1 39 5.8 3.1 120 290
array-memsafety/add_last-alloca_true-valid-memsafety.i 2 750   750   8200 330 1.8 0      .52 .33 12   40 5.8 3.1 110 300
array-memsafety/array01-alloca_true-valid-memsafety.i 2 750   750   7800 500 1.8 0      .52 .34 10   42 6.1 3.3 120 300
array-memsafety/array02-alloca_true-valid-memsafety.i 2 760   750   7200 580 1.9 0      .49 .33 4.0 40 6.0 3.2 130 300
array-memsafety/array03-alloca_true-valid-memsafety.i 2 750   750   7000 390 1.9 0      .53 .34 7.0 40 7.6 4.0 86 300
array-memsafety/bubblesort-alloca_true-valid-memsafety.i 2 750   750   6600 510 1.9 0      .50 .33 11   39 5.8 3.1 100 300
array-memsafety/count_down-alloca_true-valid-memsafety.i 2 750   750   8500 210 1.9 0      .51 .32 9.5 40 6.1 3.2 120 310
array-memsafety/cstrcat-alloca_true-valid-memsafety.i 2 750   750   8800 280 1.9 0      .48 .31 3.7 40 6.1 3.2 120 300
array-memsafety/cstrchr-alloca_true-valid-memsafety.i 2 750   750   10000 170 1.8 0      .51 .32 12   41 6.0 3.2 120 300
array-memsafety/cstrcmp-alloca_true-valid-memsafety.i 2 750   750   8300 210 1.9 0      .50 .32 12   39 6.1 3.2 140 310
array-memsafety/cstrcpy-alloca_true-valid-memsafety.i 2 750   750   9100 220 1.8 0      .58 .38 9.5 39 5.7 3.1 110 290
array-memsafety/cstrcspn-alloca_true-valid-memsafety.i 2 750   750   7600 610 1.9 0      .52 .34 4.5 40 6.2 3.3 120 300
array-memsafety/cstrlen-alloca_true-valid-memsafety.i 2 750   750   9300 150 1.8 0      .52 .35 11   39 6.4 3.4 130 300
array-memsafety/cstrncat-alloca_true-valid-memsafety.i 2 750   750   8700 260 1.9 0      .48 .31 5.2 39 6.0 3.2 110 290
array-memsafety/cstrncmp-alloca_true-valid-memsafety.i 2 750   750   8000 240 1.9 .0041 .50 .32 13   40 7.4 3.8 140 330
array-memsafety/cstrncpy-alloca_true-valid-memsafety.i 2 750   750   7100 240 1.9 0      .51 .34 8.9 39 5.9 3.2 110 300
array-memsafety/cstrpbrk-alloca_true-valid-memsafety.i 2 750   750   6500 550 1.9 0      .52 .33 11   40 6.0 3.2 120 300
array-memsafety/cstrspn-alloca_true-valid-memsafety.i 2 750   750   6100 510 1.9 0      .50 .32 7.0 41 6.2 3.3 110 300
array-memsafety/diff-alloca_true-valid-memsafety.i 2 750   750   11000 150 1.9 0      .52 .33 11   41 5.8 3.1 100 290
array-memsafety/insertionsort-alloca_true-valid-memsafety.i 2 750   750   6100 440 1.9 0      .49 .33 4.9 39 6.4 3.4 120 310
array-memsafety/java_BubbleSort-alloca_true-valid-memsafety.i 2 750   750   8100 460 1.9 0      .51 .33 10   40 5.8 3.1 110 300
array-memsafety/lis-alloca_true-valid-memsafety.i 2 750   750   6500 350 2.0 0      .51 .33 12   39 6.8 3.6 130 320
array-memsafety/mult_array-alloca_true-valid-memsafety.i 2 750   750   7700 370 1.9 0      .50 .32 8.7 40 6.1 3.3 120 300
array-memsafety/openbsd_cbzero-alloca_true-valid-memsafety.i 2 750   750   11000 320 1.8 0      .54 .36 8.3 41 6.0 3.2 100 310
array-memsafety/openbsd_cmemchr-alloca_true-valid-memsafety.i 2 750   750   11000 410 1.8 0      .55 .35 14   41 5.9 3.1 120 300
array-memsafety/openbsd_cmemrchr-alloca_true-valid-memsafety.i 2 750   750   8900 450 1.8 0      .49 .32 9.4 40 6.9 3.6 140 310
array-memsafety/openbsd_cmemset-alloca_true-valid-memsafety.i 2 750   750   8400 410 1.8 0      .52 .34 12   40 6.0 3.2 110 290
array-memsafety/openbsd_cstpcpy-alloca_true-valid-memsafety.i 2 750   750   8500 270 1.8 0      .50 .32 4.1 40 6.2 3.3 120 300
array-memsafety/openbsd_cstpncpy-alloca_true-valid-memsafety.i 2 750   750   7100 230 1.9 0      .49 .32 6.8 40 6.3 3.3 130 300
array-memsafety/openbsd_cstrcat-alloca_true-valid-memsafety.i 2 750   750   8100 290 1.9 0      .54 .35 14   42 6.2 3.3 120 300
array-memsafety/openbsd_cstrcmp-alloca_true-valid-memsafety.i 2 750   750   8500 230 1.9 0      .48 .30 7.9 40 6.3 3.3 110 310
array-memsafety/openbsd_cstrcpy-alloca_true-valid-memsafety.i 2 750   750   9000 230 1.8 0      .50 .32 9.9 40 5.3 2.9 110 280
array-memsafety/openbsd_cstrcspn-alloca_true-valid-memsafety.i 2 750   750   8100 230 1.8 0      .52 .33 10   42 6.1 3.3 120 300
array-memsafety/openbsd_cstrlcpy-alloca_true-valid-memsafety.i 2 750   750   10000 250 1.9 0      .47 .31 3.6 40 6.4 3.3 120 300
array-memsafety/openbsd_cstrlen-alloca_true-valid-memsafety.i 2 750   750   9100 150 1.8 0      .51 .35 4.0 42 6.1 3.2 120 300
array-memsafety/openbsd_cstrncat-alloca_true-valid-memsafety.i 2 750   750   11000 260 1.9 0      .54 .35 11   41 5.6 3.1 110 280
array-memsafety/openbsd_cstrncmp-alloca_true-valid-memsafety.i 2 750   750   8400 210 1.9 0      .53 .33 11   39 5.9 3.1 110 300
array-memsafety/openbsd_cstrncpy-alloca_true-valid-memsafety.i 2 750   750   8800 230 1.9 0      .51 .32 11   40 6.1 3.2 120 290
array-memsafety/openbsd_cstrnlen-alloca_true-valid-memsafety.i 2 750   750   9300 180 1.8 0      .57 .36 8.8 40 6.3 3.3 130 310
array-memsafety/openbsd_cstrpbrk-alloca_true-valid-memsafety.i 2 750   750   6900 600 1.9 0      .49 .31 10   39 6.1 3.2 130 300
array-memsafety/openbsd_cstrspn-alloca_true-valid-memsafety.i 2 750   750   7500 320 1.9 0      .52 .33 12   40 6.3 3.4 130 310
array-memsafety/openbsd_cstrstr-alloca_true-valid-memsafety.i 0 750   930   7400 290 2.0 0      .50 .33 12   39 6.0 3.2 110 290
array-memsafety/rec_strlen-alloca_true-valid-memsafety.i 2 750   750   9200 240 1.8 0      .49 .32 4.3 40 5.7 3.1 120 290
array-memsafety/selectionsort-alloca_true-valid-memsafety.i 2 750   750   6600 470 1.9 0      .53 .34 6.7 39 5.9 3.2 120 290
array-memsafety/stroeder1-alloca_true-valid-memsafety.i 2 750   750   8200 180 1.8 0      .51 .34 6.2 39 6.6 3.4 130 300
array-memsafety/stroeder2-alloca_true-valid-memsafety.i 2 760   750   6000 660 1.9 0      .51 .33 11   40 6.8 3.6 110 300
array-memsafety/strreplace-alloca_true-valid-memsafety.i 2 750   750   9100 130 1.8 0      .50 .32 12   40 6.4 3.5 110 300
array-memsafety/subseq-alloca_true-valid-memsafety.i 2 750   750   8600 210 1.9 0      .51 .32 12   39 6.2 3.3 110 300
array-memsafety/substring-alloca_true-valid-memsafety.i 2 750   750   6600 510 1.9 0      .53 .35 6.5 41 6.3 3.4 110 300
array-examples/relax_false-valid-deref.i -32 750   750   8800 220 2.1 0      .52 .33 12   39 5.8 3.1 87 300
array-examples/sanfoundry_24_false-valid-deref.i 1 6.2 6.0 79 92 1.2 0      .52 .33 13   40 5.5 3.0 110 290
array-examples/standard_strcpy_false-valid-deref_ground.i 1 8.4 8.3 100 95 1.2 0      .50 .32 9.4 39 6.2 3.3 100 300
array-examples/standard_strcpy_original_false-valid-deref.i 1 11   11   160 100 1.2 0      .49 .32 6.5 40 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