Tool CPAchecker 1.6.1-svn 24048
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:38:11 CET [[ 2017-01-14 23:48:17 CET ]] [[ 2017-01-14 23:57:43 CET ]] [[ 2017-01-14 23:52:59 CET ]] [[ 2017-01-15 00:03:21 CET ]]
Run set sv-comp17.MemSafety-Arrays
Options -sv-comp17 -heap 10000M -disable-java-assertions [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-seq.2017-01-13_0438.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-seq.2017-01-13_0438.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-seq.2017-01-13_0438.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-seq.2017-01-13_0438.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 0 wit inspect 2.4 1.0  22 210 0   0   error (invalid witness file) .48 .31 12   39 error (invalid witness file) 7.4 3.9 93 310 - -
array-memsafety/bubblesort_unsafe_false-valid-deref.i timeout 0 wit inspect 920   420    7300 11000 0   0   error (invalid witness file) .51 .32 11   39 error (invalid witness file) 5.9 3.1 110 300 - -
array-memsafety/count_down_unsafe_false-valid-deref.i error 0 wit inspect 2.5 1.0  21 220 0   0   error (invalid witness file) .49 .32 7.5 39 error (invalid witness file) 6.2 3.2 120 300 - -
array-memsafety/cstrcat_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 2.2 .96 19 230 0   0   false(valid-deref) 3.8  2.2  41   240 false(valid-deref) 9.1 4.9 150 360 - -
array-memsafety/cstrchr_unsafe_false-valid-deref.i error 0 wit inspect 2.6 1.0  25 220 0   0   error (invalid witness file) .55 .37 8.7 42 error (invalid witness file) 5.5 2.9 89 290 - -
array-memsafety/cstrlen_unsafe_false-valid-deref.i error 0 wit inspect 2.5 1.0  25 220 0   0   error (invalid witness file) .65 .41 9.2 41 error (invalid witness file) 7.4 3.9 80 300 - -
array-memsafety/cstrncat_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 2.2 .99 18 230 0   0   false(valid-deref) 4.2  2.4  48   240 false(valid-deref) 8.8 4.7 160 340 - -
array-memsafety/cstrncpy_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 2.3 .98 20 230 0   0   false(valid-deref) 3.2  1.8  34   230 false(valid-deref) 8.0 4.3 120 330 - -
array-memsafety/cstrpbrk_unsafe_false-valid-deref.i error 0 wit inspect 2.6 1.0  21 220 0   0   error (invalid witness file) .50 .32 11   40 error (invalid witness file) 7.2 3.8 92 300 - -
array-memsafety/diff_usafe_false-valid-deref.i false(valid-deref) 1 wit inspect 2.4 1.0  21 240 0   0   false(valid-deref) 3.8  2.1  60   240 false(valid-deref) 8.8 4.7 160 350 - -
array-memsafety/knapsack_alloca_unsafe_false-valid-deref.i error 0 wit inspect 10   4.1  14 220 0   0   error (invalid witness file) .61 .39 6.0 40 error (invalid witness file) 6.2 3.3 97 300 - -
array-memsafety/lis_unsafe_false-valid-deref.i error 0 wit inspect 2.5 1.0  23 220 0   0   error (invalid witness file) .48 .32 9.5 40 error (invalid witness file) 6.6 3.5 99 300 - -
array-memsafety/mult_array_unsafe_false-valid-deref.i error 0 wit inspect 2.6 1.0  21 220 0   0   error (invalid witness file) .47 .31 5.5 42 error (invalid witness file) 5.7 3.1 120 300 - -
array-memsafety/reverse_array_alloca_unsafe_false-valid-deref.i error 0 wit inspect 2.4 1.0  20 210 0   0   error (invalid witness file) .51 .33 11   40 error (invalid witness file) 6.6 3.4 110 310 - -
array-memsafety/reverse_array_unsafe_false-valid-deref.i error 0 wit inspect 2.6 1.0  21 220 0   0   error (invalid witness file) .55 .35 12   44 error (invalid witness file) 6.2 3.3 110 310 - -
array-memsafety/selectionsort_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 2.4 1.0  22 230 0   0   false(valid-deref) 3.6  2.0  56   250 false(valid-deref) 9.7 5.2 120 340 - -
array-memsafety/stroeder1_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 2.3 .98 20 230 0   0   false(valid-deref) 4.4  2.5  52   230 false(valid-deref) 9.1 4.9 74 330 - -
array-memsafety/add_last-alloca_true-valid-memsafety.i error 0 wit inspect 2.5 1.0  21 210 0   0   - - error (invalid witness file) .51 .32 9.2 42 error (invalid witness file) 6.5 3.4 79 300
array-memsafety/array01-alloca_true-valid-memsafety.i error 0 wit inspect 2.5 1.0  21 220 0   0   - - error (invalid witness file) .53 .33 10   40 error (invalid witness file) 8.3 4.3 81 310
array-memsafety/array02-alloca_true-valid-memsafety.i error 0 wit inspect 2.6 1.0  25 220 0   0   - - error (invalid witness file) .52 .33 10   40 error (invalid witness file) 6.0 3.2 95 300
array-memsafety/array03-alloca_true-valid-memsafety.i error 0 wit inspect 2.5 1.0  23 210 0   0   - - error (invalid witness file) .50 .32 10   39 error (invalid witness file) 7.2 3.8 66 290
array-memsafety/bubblesort-alloca_true-valid-memsafety.i error 0 wit inspect 2.5 1.0  23 210 0   0   - - error (invalid witness file) .50 .33 11   40 error (invalid witness file) 5.4 2.9 56 290
array-memsafety/count_down-alloca_true-valid-memsafety.i error 0 wit inspect 2.6 1.0  25 230 0   0   - - error (invalid witness file) .56 .37 11   43 error (invalid witness file) 5.8 3.1 86 300
array-memsafety/cstrcat-alloca_true-valid-memsafety.i error 0 wit inspect 2.6 1.0  24 220 0   0   - - error (invalid witness file) .51 .33 12   39 error (invalid witness file) 6.3 3.3 89 310
array-memsafety/cstrchr-alloca_true-valid-memsafety.i error 0 wit inspect 2.4 .99 23 210 0   0   - - error (invalid witness file) .49 .32 8.4 39 error (invalid witness file) 5.8 3.1 120 290
array-memsafety/cstrcmp-alloca_true-valid-memsafety.i error 0 wit inspect 2.5 1.0  20 220 0   0   - - error (invalid witness file) .49 .32 12   40 error (invalid witness file) 5.8 3.1 110 300
array-memsafety/cstrcpy-alloca_true-valid-memsafety.i error 0 wit inspect 2.6 1.0  23 220 0   0   - - error (invalid witness file) .56 .35 6.5 40 error (invalid witness file) 5.8 3.1 72 290
array-memsafety/cstrcspn-alloca_true-valid-memsafety.i error 0 wit inspect 2.4 1.0  22 210 0   0   - - error (invalid witness file) .50 .32 10   40 error (invalid witness file) 5.7 3.0 94 290
array-memsafety/cstrlen-alloca_true-valid-memsafety.i error 0 wit inspect 2.7 1.0  21 220 0   0   - - error (invalid witness file) .54 .35 8.7 42 error (invalid witness file) 6.1 3.2 130 300
array-memsafety/cstrncat-alloca_true-valid-memsafety.i error 0 wit inspect 2.6 1.0  22 220 0   0   - - error (invalid witness file) .60 .38 9.3 40 error (invalid witness file) 6.0 3.2 83 310
array-memsafety/cstrncmp-alloca_true-valid-memsafety.i error 0 wit inspect 2.6 1.0  24 220 0   0   - - error (invalid witness file) .61 .38 8.8 39 error (invalid witness file) 6.1 3.3 97 300
array-memsafety/cstrncpy-alloca_true-valid-memsafety.i error 0 wit inspect 2.5 1.0  20 210 0   0   - - error (invalid witness file) .51 .32 9.7 39 error (invalid witness file) 6.6 3.5 110 300
array-memsafety/cstrpbrk-alloca_true-valid-memsafety.i error 0 wit inspect 2.6 1.0  22 220 0   0   - - error (invalid witness file) .52 .35 13   39 error (invalid witness file) 6.5 3.4 130 310
array-memsafety/cstrspn-alloca_true-valid-memsafety.i error 0 wit inspect 10   4.2  14 220 0   0   - - error (invalid witness file) .57 .37 6.9 40 error (invalid witness file) 5.7 3.1 60 290
array-memsafety/diff-alloca_true-valid-memsafety.i error 0 wit inspect 2.6 1.0  20 220 0   0   - - error (invalid witness file) .54 .35 9.8 41 error (invalid witness file) 6.2 3.3 96 300
array-memsafety/insertionsort-alloca_true-valid-memsafety.i error 0 wit inspect 2.6 1.0  22 220 0   0   - - error (invalid witness file) .50 .33 10   39 error (invalid witness file) 6.4 3.4 120 310
array-memsafety/java_BubbleSort-alloca_true-valid-memsafety.i error 0 wit inspect 2.5 1.0  21 220 0   0   - - error (invalid witness file) .50 .31 9.5 41 error (invalid witness file) 5.8 3.1 87 300
array-memsafety/lis-alloca_true-valid-memsafety.i error 0 wit inspect 2.6 1.0  20 220 0   0   - - error (invalid witness file) .52 .32 5.7 40 error (invalid witness file) 6.2 3.3 71 300
array-memsafety/mult_array-alloca_true-valid-memsafety.i error 0 wit inspect 2.6 1.0  21 220 0   0   - - error (invalid witness file) .57 .37 7.9 41 error (invalid witness file) 6.5 3.4 73 300
array-memsafety/openbsd_cbzero-alloca_true-valid-memsafety.i error 0 wit inspect 2.5 .99 22 220 0   0   - - error (invalid witness file) .52 .33 8.4 39 error (invalid witness file) 6.1 3.2 110 300
array-memsafety/openbsd_cmemchr-alloca_true-valid-memsafety.i error 0 wit inspect 2.5 1.0  21 220 0   0   - - error (invalid witness file) .48 .32 11   39 error (invalid witness file) 6.7 3.5 130 320
array-memsafety/openbsd_cmemrchr-alloca_true-valid-memsafety.i error 0 wit inspect 2.6 1.0  21 210 0   0   - - error (invalid witness file) .55 .35 11   40 error (invalid witness file) 6.5 3.4 100 300
array-memsafety/openbsd_cmemset-alloca_true-valid-memsafety.i error 0 wit inspect 2.5 .99 20 220 0   0   - - error (invalid witness file) .64 .41 8.2 40 error (invalid witness file) 6.0 3.3 99 290
array-memsafety/openbsd_cstpcpy-alloca_true-valid-memsafety.i error 0 wit inspect 2.7 1.1  22 220 0   0   - - error (invalid witness file) .52 .33 12   39 error (invalid witness file) 5.9 3.1 77 300
array-memsafety/openbsd_cstpncpy-alloca_true-valid-memsafety.i error 0 wit inspect 2.6 1.0  22 230 0   0   - - error (invalid witness file) .50 .33 7.7 40 error (invalid witness file) 6.4 3.4 110 300
array-memsafety/openbsd_cstrcat-alloca_true-valid-memsafety.i error 0 wit inspect 2.4 1.0  23 210 0   0   - - error (invalid witness file) .58 .38 10   39 error (invalid witness file) 7.1 3.7 72 310
array-memsafety/openbsd_cstrcmp-alloca_true-valid-memsafety.i error 0 wit inspect 2.6 1.0  22 210 0   0   - - error (invalid witness file) .52 .33 9.6 40 error (invalid witness file) 6.9 3.7 110 300
array-memsafety/openbsd_cstrcpy-alloca_true-valid-memsafety.i error 0 wit inspect 2.5 1.0  22 220 0   0   - - error (invalid witness file) .48 .31 8.3 39 error (invalid witness file) 5.9 3.2 78 290
array-memsafety/openbsd_cstrcspn-alloca_true-valid-memsafety.i error 0 wit inspect 2.7 1.1  23 220 0   0   - - error (invalid witness file) .60 .39 11   41 error (invalid witness file) 7.3 3.8 140 320
array-memsafety/openbsd_cstrlcpy-alloca_true-valid-memsafety.i error 0 wit inspect 2.6 1.0  21 220 0   0   - - error (invalid witness file) .55 .36 12   41 error (invalid witness file) 5.6 3.0 86 290
array-memsafety/openbsd_cstrlen-alloca_true-valid-memsafety.i error 0 wit inspect 11   4.0  12 220 0   0   - - error (invalid witness file) .58 .38 12   40 error (invalid witness file) 6.0 3.2 120 280
array-memsafety/openbsd_cstrncat-alloca_true-valid-memsafety.i error 0 wit inspect 2.5 1.0  20 220 0   0   - - error (invalid witness file) .48 .31 6.6 39 error (invalid witness file) 6.2 3.3 120 300
array-memsafety/openbsd_cstrncmp-alloca_true-valid-memsafety.i error 0 wit inspect 2.8 1.1  20 220 0   0   - - error (invalid witness file) .59 .36 4.6 40 error (invalid witness file) 5.8 3.1 88 300
array-memsafety/openbsd_cstrncpy-alloca_true-valid-memsafety.i error 0 wit inspect 2.6 1.0  20 220 0   0   - - error (invalid witness file) .49 .32 11   39 error (invalid witness file) 5.3 2.9 84 300
array-memsafety/openbsd_cstrnlen-alloca_true-valid-memsafety.i error 0 wit inspect 2.6 1.0  24 220 0   0   - - error (invalid witness file) .55 .34 10   43 error (invalid witness file) 5.6 3.0 80 290
array-memsafety/openbsd_cstrpbrk-alloca_true-valid-memsafety.i error 0 wit inspect 2.5 1.0  23 220 0   0   - - error (invalid witness file) .63 .41 8.1 39 error (invalid witness file) 6.0 3.2 91 280
array-memsafety/openbsd_cstrspn-alloca_true-valid-memsafety.i error 0 wit inspect 2.7 1.0  22 220 0   0   - - error (invalid witness file) .49 .32 11   40 error (invalid witness file) 6.3 3.3 120 310
array-memsafety/openbsd_cstrstr-alloca_true-valid-memsafety.i error 0 wit inspect 2.7 1.0  24 220 0   0   - - error (invalid witness file) .51 .33 9.1 40 error (invalid witness file) 6.6 3.5 95 290
array-memsafety/rec_strlen-alloca_true-valid-memsafety.i error 0 wit inspect 10   4.0  14 220 0   0   - - error (invalid witness file) .48 .30 8.8 39 error (invalid witness file) 6.9 3.6 100 300
array-memsafety/selectionsort-alloca_true-valid-memsafety.i error 0 wit inspect 2.5 1.0  21 220 0   0   - - error (invalid witness file) .52 .33 12   40 error (invalid witness file) 6.2 3.3 110 300
array-memsafety/stroeder1-alloca_true-valid-memsafety.i error 0 wit inspect 2.5 1.0  21 220 0   0   - - error (invalid witness file) .49 .32 11   39 error (invalid witness file) 6.4 3.4 100 310
array-memsafety/stroeder2-alloca_true-valid-memsafety.i error 0 wit inspect 2.5 1.0  22 220 0   0   - - error (invalid witness file) .49 .31 8.7 41 error (invalid witness file) 6.4 3.4 110 290
array-memsafety/strreplace-alloca_true-valid-memsafety.i error 0 wit inspect 2.5 1.0  22 220 0   0   - - error (invalid witness file) .63 .40 5.1 41 error (invalid witness file) 6.6 3.5 92 300
array-memsafety/subseq-alloca_true-valid-memsafety.i error 0 wit inspect 2.5 1.0  23 220 0   0   - - error (invalid witness file) .49 .32 9.2 40 error (invalid witness file) 6.1 3.2 110 300
array-memsafety/substring-alloca_true-valid-memsafety.i error 0 wit inspect 2.5 1.0  22 220 0   0   - - error (invalid witness file) .49 .32 11   41 error (invalid witness file) 7.0 3.7 130 320
array-examples/relax_false-valid-deref.i error 0 wit inspect 2.7 1.1  22 220 0   0   error (invalid witness file) .50 .33 11   40 error (invalid witness file) 7.0 3.6 130 340 - -
array-examples/sanfoundry_24_false-valid-deref.i timeout 0 wit inspect 900   860    1700 2900 0   0   error (invalid witness file) .64 .40 9.7 42 error (invalid witness file) 7.2 3.8 82 300 - -
array-examples/standard_strcpy_false-valid-deref_ground.i timeout 0 wit inspect 900   860    12000 3700 0   0   error (invalid witness file) .60 .37 9.4 42 error (invalid witness file) 6.2 3.2 100 320 - -
array-examples/standard_strcpy_original_false-valid-deref.i timeout 0 wit inspect 900   860    11000 3700 0   0   error (invalid witness file) .58 .37 11   41 error (invalid witness file) 6.1 3.2 83 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 6 3800 3100   34000 36000 0   0   69 31 18 440 2000 69 150 80 2300 6600 69 25 16 460 1900   69 300 160 4600 14000  
    correct results 6 6 14 5.9 120 1400 0   0   6 23 13 290 1400 6 53 29 790 2000 0 0 0 0 0   0 0 0 0 0  
        correct true 0
        correct false 6 6 14 5.9 120 1400 0   0   6 23 13 290 1400 6 53 29 790 2000 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) 6
Run set sv-comp17.MemSafety-Arrays