Tool Predator-HP
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 12:06:28 CET [[ 2017-01-15 02:02:31 CET ]] [[ 2017-01-15 02:04:15 CET ]] [[ 2017-01-15 02:04:05 CET ]] [[ 2017-01-15 02:06:30 CET ]]
Run set sv-comp17.MemSafety-Arrays
Options --witness error-witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/predatorhp.2017-01-13_1206.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/predatorhp.2017-01-13_1206.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/predatorhp.2017-01-13_1206.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/predatorhp.2017-01-13_1206.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 unknown 0 wit inspect .11 1.0 1.7 23 0     0     error (invalid witness file) .56 .35 9.5 39 error (invalid witness file) 7.1 3.8 87 300 - -
array-memsafety/bubblesort_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .16 1.1 1.9 22 .049 0     timeout 93    71    2100   4500 false(valid-deref) 7.6 4.1 150 330 - -
array-memsafety/count_down_unsafe_false-valid-deref.i unknown 0 wit inspect .11 1.0 1.8 23 0     0     error (invalid witness file) .73 .47 8.6 44 error (invalid witness file) 7.0 3.7 90 300 - -
array-memsafety/cstrcat_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .12 1.0 1.9 21 .049 0     false(valid-deref) 3.3  1.9  65   240 false(valid-deref) 9.8 5.2 100 340 - -
array-memsafety/cstrchr_unsafe_false-valid-deref.i unknown 0 wit inspect .14 1.1 1.7 23 .016 0     error (invalid witness file) .49 .31 11   39 error (invalid witness file) 6.2 3.3 100 300 - -
array-memsafety/cstrlen_unsafe_false-valid-deref.i unknown 0 wit inspect .14 1.1 1.8 23 .016 0     error (invalid witness file) .73 .45 8.3 42 error (invalid witness file) 6.1 3.2 82 310 - -
array-memsafety/cstrncat_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .13 1.0 1.8 22 .049 0     false(valid-deref) 3.2  1.8  62   230 false(valid-deref) 7.9 4.3 180 340 - -
array-memsafety/cstrncpy_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .12 1.0 1.9 21 .049 0     false(valid-deref) 4.5  2.5  50   240 false(valid-deref) 10   5.2 120 330 - -
array-memsafety/cstrpbrk_unsafe_false-valid-deref.i unknown 0 wit inspect .11 1.0 1.6 24 .016 .066 error (invalid witness file) .60 .39 10   40 error (invalid witness file) 7.3 3.8 95 300 - -
array-memsafety/diff_usafe_false-valid-deref.i false(valid-deref) 1 wit inspect .15 1.1 2.4 23 .074 0     false(valid-deref) 3.8  2.2  86   240 false(valid-deref) 7.8 4.1 110 320 - -
array-memsafety/knapsack_alloca_unsafe_false-valid-deref.i unknown 0 wit inspect .21 1.1 1.7 34 0     9.0   error (invalid witness file) .56 .36 9.9 40 error (invalid witness file) 6.7 3.5 94 300 - -
array-memsafety/lis_unsafe_false-valid-deref.i unknown 0 wit inspect .12 1.0 1.7 23 0     0     error (invalid witness file) .57 .37 10   40 error (invalid witness file) 7.7 4.0 86 310 - -
array-memsafety/mult_array_unsafe_false-valid-deref.i unknown 0 wit inspect .13 1.1 1.7 23 0     .086 error (invalid witness file) .55 .34 9.7 40 error (invalid witness file) 7.8 4.1 90 300 - -
array-memsafety/reverse_array_alloca_unsafe_false-valid-deref.i unknown 0 wit inspect .12 1.0 1.9 23 0     0     error (invalid witness file) .62 .41 7.6 39 error (invalid witness file) 7.4 3.9 81 300 - -
array-memsafety/reverse_array_unsafe_false-valid-deref.i unknown 0 wit inspect .11 1.0 2.0 25 0     1.2   error (invalid witness file) .58 .37 5.7 42 error (invalid witness file) 7.5 4.0 76 300 - -
array-memsafety/selectionsort_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .12 1.0 1.8 24 .049 .95  false(valid-deref) 3.5  1.9  73   230 false(valid-deref) 9.1 4.9 100 350 - -
array-memsafety/stroeder1_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .17 1.1 1.8 21 .049 0     false(valid-deref) 3.6  2.0  79   250 false(valid-deref) 9.2 4.9 120 350 - -
array-memsafety/add_last-alloca_true-valid-memsafety.i unknown 0 wit inspect .11 1.0 1.8 22 0     0     - - error (invalid witness file) .69 .43 9.0 41 error (invalid witness file) 7.4 3.9 76 290
array-memsafety/array01-alloca_true-valid-memsafety.i unknown 0 wit inspect .15 1.1 1.6 23 0     .45  - - error (invalid witness file) .63 .41 8.9 41 error (invalid witness file) 7.5 3.9 74 300
array-memsafety/array02-alloca_true-valid-memsafety.i unknown 0 wit inspect .15 1.0 1.7 23 0     .074 - - error (invalid witness file) .48 .31 7.9 40 error (invalid witness file) 5.9 3.2 110 300
array-memsafety/array03-alloca_true-valid-memsafety.i unknown 0 wit inspect .12 1.0 1.6 23 0     .15  - - error (invalid witness file) .54 .35 7.1 40 error (invalid witness file) 6.0 3.2 110 300
array-memsafety/bubblesort-alloca_true-valid-memsafety.i unknown 0 wit inspect .11 1.0 1.9 24 0     .53  - - error (invalid witness file) .53 .35 9.4 41 error (invalid witness file) 7.1 3.7 59 300
array-memsafety/count_down-alloca_true-valid-memsafety.i unknown 0 wit inspect .11 1.0 1.7 23 0     .14  - - error (invalid witness file) .50 .32 12   39 error (invalid witness file) 6.2 3.3 100 300
array-memsafety/cstrcat-alloca_true-valid-memsafety.i unknown 0 wit inspect .14 1.1 1.8 23 0     .086 - - error (invalid witness file) .49 .32 11   40 error (invalid witness file) 6.4 3.5 81 290
array-memsafety/cstrchr-alloca_true-valid-memsafety.i unknown 0 wit inspect .11 1.0 1.9 22 0     .066 - - error (invalid witness file) .67 .42 8.0 41 error (invalid witness file) 6.5 3.5 100 310
array-memsafety/cstrcmp-alloca_true-valid-memsafety.i unknown 0 wit inspect .16 1.1 1.8 33 0     9.1   - - error (invalid witness file) .60 .39 5.5 41 error (invalid witness file) 7.5 4.0 68 300
array-memsafety/cstrcpy-alloca_true-valid-memsafety.i unknown 0 wit inspect .21 1.1 1.6 33 0     9.0   - - error (invalid witness file) .53 .34 12   42 error (invalid witness file) 6.3 3.3 100 310
array-memsafety/cstrcspn-alloca_true-valid-memsafety.i unknown 0 wit inspect .11 1.0 1.8 24 0     .086 - - error (invalid witness file) .47 .30 9.0 39 error (invalid witness file) 6.5 3.4 94 300
array-memsafety/cstrlen-alloca_true-valid-memsafety.i unknown 0 wit inspect .13 1.1 1.7 24 0     .078 - - error (invalid witness file) .59 .37 9.6 39 error (invalid witness file) 7.5 3.9 74 300
array-memsafety/cstrncat-alloca_true-valid-memsafety.i unknown 0 wit inspect .11 1.0 1.8 24 0     0     - - error (invalid witness file) .53 .34 7.9 39 error (invalid witness file) 7.6 4.0 93 300
array-memsafety/cstrncmp-alloca_true-valid-memsafety.i unknown 0 wit inspect .15 1.1 1.6 22 0     0     - - error (invalid witness file) .49 .31 6.5 39 error (invalid witness file) 6.7 3.5 110 300
array-memsafety/cstrncpy-alloca_true-valid-memsafety.i unknown 0 wit inspect .11 1.0 1.8 24 0     .066 - - error (invalid witness file) .49 .33 7.6 39 error (invalid witness file) 6.8 3.6 86 310
array-memsafety/cstrpbrk-alloca_true-valid-memsafety.i unknown 0 wit inspect .14 1.1 1.7 24 0     0     - - error (invalid witness file) .65 .40 8.0 39 error (invalid witness file) 5.8 3.1 100 290
array-memsafety/cstrspn-alloca_true-valid-memsafety.i unknown 0 wit inspect .11 1.0 1.7 23 0     0     - - error (invalid witness file) .48 .30 9.8 39 error (invalid witness file) 6.2 3.3 110 300
array-memsafety/diff-alloca_true-valid-memsafety.i unknown 0 wit inspect .12 1.0 1.6 24 0     0     - - error (invalid witness file) .53 .33 12   41 error (invalid witness file) 8.1 4.3 80 300
array-memsafety/insertionsort-alloca_true-valid-memsafety.i unknown 0 wit inspect .11 1.0 1.7 24 0     .086 - - error (invalid witness file) .50 .33 10   39 error (invalid witness file) 6.4 3.3 82 290
array-memsafety/java_BubbleSort-alloca_true-valid-memsafety.i unknown 0 wit inspect .12 1.0 1.7 23 0     0     - - error (invalid witness file) .57 .36 8.7 39 error (invalid witness file) 7.6 4.0 70 300
array-memsafety/lis-alloca_true-valid-memsafety.i unknown 0 wit inspect .11 1.0 1.8 24 0     0     - - error (invalid witness file) .65 .41 8.8 39 error (invalid witness file) 7.4 4.0 74 300
array-memsafety/mult_array-alloca_true-valid-memsafety.i unknown 0 wit inspect .15 1.1 2.0 23 0     .086 - - error (invalid witness file) .64 .41 8.4 40 error (invalid witness file) 6.5 3.4 88 300
array-memsafety/openbsd_cbzero-alloca_true-valid-memsafety.i unknown 0 wit inspect .10 1.0 2.2 24 0     0     - - error (invalid witness file) .55 .35 9.6 39 error (invalid witness file) 6.6 3.5 100 300
array-memsafety/openbsd_cmemchr-alloca_true-valid-memsafety.i unknown 0 wit inspect .14 1.1 1.6 23 0     .15  - - error (invalid witness file) .60 .38 7.1 39 error (invalid witness file) 7.1 3.8 77 300
array-memsafety/openbsd_cmemrchr-alloca_true-valid-memsafety.i unknown 0 wit inspect .14 1.1 1.6 24 0     .086 - - error (invalid witness file) .58 .38 7.5 39 error (invalid witness file) 7.1 3.7 67 300
array-memsafety/openbsd_cmemset-alloca_true-valid-memsafety.i unknown 0 wit inspect .11 1.0 1.8 24 0     .15  - - error (invalid witness file) .64 .41 8.1 39 error (invalid witness file) 7.2 3.8 75 310
array-memsafety/openbsd_cstpcpy-alloca_true-valid-memsafety.i unknown 0 wit inspect .15 1.1 1.6 22 0     0     - - error (invalid witness file) .63 .39 8.2 39 error (invalid witness file) 6.0 3.2 110 300
array-memsafety/openbsd_cstpncpy-alloca_true-valid-memsafety.i unknown 0 wit inspect .12 1.0 2.0 25 0     1.1   - - error (invalid witness file) .50 .32 9.0 40 error (invalid witness file) 7.2 3.8 83 300
array-memsafety/openbsd_cstrcat-alloca_true-valid-memsafety.i unknown 0 wit inspect .11 1.0 2.0 24 0     0     - - error (invalid witness file) .51 .33 11   40 error (invalid witness file) 5.9 3.1 110 300
array-memsafety/openbsd_cstrcmp-alloca_true-valid-memsafety.i unknown 0 wit inspect .11 1.0 1.7 23 0     0     - - error (invalid witness file) .54 .35 11   44 error (invalid witness file) 5.9 3.1 97 300
array-memsafety/openbsd_cstrcpy-alloca_true-valid-memsafety.i unknown 0 wit inspect .10 1.0 1.9 24 0     0     - - error (invalid witness file) .49 .31 9.3 39 error (invalid witness file) 6.0 3.2 110 310
array-memsafety/openbsd_cstrcspn-alloca_true-valid-memsafety.i unknown 0 wit inspect .11 1.0 1.7 23 0     0     - - error (invalid witness file) .51 .32 12   40 error (invalid witness file) 6.0 3.2 96 300
array-memsafety/openbsd_cstrlcpy-alloca_true-valid-memsafety.i unknown 0 wit inspect .14 1.1 1.8 24 0     0     - - error (invalid witness file) .68 .43 7.2 39 error (invalid witness file) 6.8 3.7 82 290
array-memsafety/openbsd_cstrlen-alloca_true-valid-memsafety.i unknown 0 wit inspect .14 1.1 1.6 24 0     0     - - error (invalid witness file) .66 .41 7.9 41 error (invalid witness file) 5.5 3.0 84 290
array-memsafety/openbsd_cstrncat-alloca_true-valid-memsafety.i unknown 0 wit inspect .15 1.1 1.6 23 0     0     - - error (invalid witness file) .64 .41 8.6 42 error (invalid witness file) 7.3 3.8 52 300
array-memsafety/openbsd_cstrncmp-alloca_true-valid-memsafety.i unknown 0 wit inspect .11 1.0 1.7 24 0     0     - - error (invalid witness file) .53 .34 8.2 39 error (invalid witness file) 9.0 4.7 96 330
array-memsafety/openbsd_cstrncpy-alloca_true-valid-memsafety.i unknown 0 wit inspect .13 1.0 1.7 23 0     .15  - - error (invalid witness file) .65 .42 6.8 40 error (invalid witness file) 7.5 3.9 79 290
array-memsafety/openbsd_cstrnlen-alloca_true-valid-memsafety.i unknown 0 wit inspect .13 1.0 1.6 24 0     .086 - - error (invalid witness file) .63 .40 8.5 40 error (invalid witness file) 6.7 3.5 100 300
array-memsafety/openbsd_cstrpbrk-alloca_true-valid-memsafety.i unknown 0 wit inspect .11 1.0 1.8 23 0     0     - - error (invalid witness file) .55 .36 12   41 error (invalid witness file) 7.3 3.8 37 300
array-memsafety/openbsd_cstrspn-alloca_true-valid-memsafety.i unknown 0 wit inspect .11 1.0 1.8 23 0     0     - - error (invalid witness file) .48 .31 6.6 40 error (invalid witness file) 7.6 4.0 85 300
array-memsafety/openbsd_cstrstr-alloca_true-valid-memsafety.i unknown 0 wit inspect .13 1.0 1.8 25 0     .75  - - error (invalid witness file) .61 .39 5.8 39 error (invalid witness file) 6.5 3.4 96 290
array-memsafety/rec_strlen-alloca_true-valid-memsafety.i unknown 0 wit inspect .14 1.1 1.6 23 0     0     - - error (invalid witness file) .48 .31 12   39 error (invalid witness file) 6.2 3.3 100 290
array-memsafety/selectionsort-alloca_true-valid-memsafety.i unknown 0 wit inspect .11 1.0 1.8 23 0     .086 - - error (invalid witness file) .65 .41 6.1 39 error (invalid witness file) 7.4 3.9 150 320
array-memsafety/stroeder1-alloca_true-valid-memsafety.i unknown 0 wit inspect .13 1.0 1.7 22 0     .086 - - error (invalid witness file) .47 .30 9.9 40 error (invalid witness file) 6.1 3.3 130 300
array-memsafety/stroeder2-alloca_true-valid-memsafety.i unknown 0 wit inspect .15 1.1 2.0 25 0     .68  - - error (invalid witness file) .60 .38 11   44 error (invalid witness file) 5.8 3.1 120 300
array-memsafety/strreplace-alloca_true-valid-memsafety.i unknown 0 wit inspect .14 1.1 1.7 24 0     0     - - error (invalid witness file) .52 .34 8.7 43 error (invalid witness file) 7.8 4.1 63 300
array-memsafety/subseq-alloca_true-valid-memsafety.i unknown 0 wit inspect .10 1.0 1.8 24 0     0     - - error (invalid witness file) .52 .34 8.2 43 error (invalid witness file) 7.1 3.8 70 280
array-memsafety/substring-alloca_true-valid-memsafety.i unknown 0 wit inspect .11 1.0 1.8 27 0     2.5   - - error (invalid witness file) .52 .33 10   40 error (invalid witness file) 7.3 3.8 79 300
array-examples/relax_false-valid-deref.i unknown 0 wit inspect .15 1.1 1.7 24 0     0     error (invalid witness file) .57 .36 14   45 error (invalid witness file) 5.9 3.1 74 300 - -
array-examples/sanfoundry_24_false-valid-deref.i timeout 0 wit inspect 900    300   5300   2600 0     0     error (invalid witness file) .48 .31 11   39 error (invalid witness file) 7.9 4.1 84 310 - -
array-examples/standard_strcpy_false-valid-deref_ground.i timeout 0 wit inspect 900    300   9100   6000 0     .086 error (invalid witness file) .49 .31 8.9 40 error (invalid witness file) 6.5 3.4 70 300 - -
array-examples/standard_strcpy_original_false-valid-deref.i timeout 0 wit inspect 900    450   10000   5300 0     0     error (invalid witness file) .62 .40 6.4 40 error (invalid witness file) 6.6 3.5 130 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 7 2700    1100   25000 15000 .42 37    69 120 88 2600 6500 69 160 84 2100 6600 69 27 17 430 1900   69 330 170 4300 14000  
    correct results 7 7 .97 7.3 13 150 .37 .95 6 120 83 2500 5900 7 61 33 890 2400 0 0 0 0 0   0 0 0 0 0  
        correct true 0
        correct false 7 7 .97 7.3 13 150 .37 .95 6 120 83 2500 5900 7 61 33 890 2400 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) 7
Run set sv-comp17.MemSafety-Arrays