Tool Ceagle Ceagle 1.3 @ 53cfa89
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-11 09:49:51 CET [[ 2017-01-14 20:52:01 CET ]] [[ 2017-01-14 21:02:28 CET ]] [[ 2017-01-14 20:57:34 CET ]] [[ 2017-01-14 21:06:31 CET ]]
Run set sv-comp17.MemSafety-Arrays
Options --compiler clang-3.7 [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ceagle.2017-01-11_0949.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ceagle.2017-01-11_0949.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ceagle.2017-01-11_0949.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ceagle.2017-01-11_0949.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 .028 .028 .17 8.0 0   0     error 5.9  3.2  68   260 false(valid-deref) 8.2 4.4 150 340 - -
array-memsafety/bubblesort_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .022 .022 .15 7.9 0   0     timeout 93    68    1700   4300 false(valid-deref) 7.8 4.2 130 320 - -
array-memsafety/count_down_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .029 .029 .18 7.8 0   0     error 4.8  2.6  100   260 true 8.4 4.5 130 330 - -
array-memsafety/cstrcat_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .027 .027 .11 7.5 0   0     false(valid-deref) 3.3  1.9  74   240 false(valid-deref) 7.8 4.2 130 320 - -
array-memsafety/cstrchr_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .064 .14  .48 33   0   25     error 5.8  3.1  65   250 true 8.3 4.5 150 350 - -
array-memsafety/cstrlen_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .027 .027 .16 8.0 0   0     error 6.1  3.3  81   250 true 8.5 4.5 150 350 - -
array-memsafety/cstrncat_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .035 .037 .13 8.0 0   0     false(valid-deref) 4.1  2.3  55   240 false(valid-deref) 8.3 4.4 140 330 - -
array-memsafety/cstrncpy_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .026 .026 .12 7.7 0   0     false(valid-deref) 3.6  2.0  75   250 false(valid-deref) 7.7 4.1 150 320 - -
array-memsafety/cstrpbrk_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .043 .044 .21 8.0 0   0     error 4.3  2.4  97   240 true 9.8 5.3 150 360 - -
array-memsafety/diff_usafe_false-valid-deref.i false(valid-deref) 1 wit inspect .035 .036 .13 7.9 0   .18  false(valid-deref) 3.6  2.1  75   240 false(valid-deref) 7.7 4.1 140 320 - -
array-memsafety/knapsack_alloca_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .029 .029 .15 8.0 0   0     error 4.8  2.6  95   260 true 7.7 4.1 140 320 - -
array-memsafety/lis_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .034 .034 .21 7.8 0   0     error 5.4  2.9  82   260 true 8.2 4.4 150 330 - -
array-memsafety/mult_array_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .039 .040 .19 8.1 0   .22  error 5.6  3.1  77   260 true 7.4 4.0 140 320 - -
array-memsafety/reverse_array_alloca_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .052 .17  .74 43   0   35     error 5.0  2.7  56   260 true 8.7 4.7 170 350 - -
array-memsafety/reverse_array_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .027 .027 .20 7.9 0   0     error 4.6  2.5  72   280 false(valid-deref) 9.1 4.9 180 350 - -
array-memsafety/selectionsort_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .021 .021 .10 7.8 0   0     false(valid-deref) 3.6  2.0  73   240 false(valid-deref) 7.4 4.1 140 340 - -
array-memsafety/stroeder1_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .067 .18  .45 43   0   35     false(valid-deref) 3.3  1.8  49   240 false(valid-deref) 7.5 4.0 130 330 - -
array-memsafety/add_last-alloca_true-valid-memsafety.i true 2 wit inspect .030 .030 .17 8.2 0   0     - - error 4.3 2.3 78 250 timeout 960 880   20000 2400
array-memsafety/array01-alloca_true-valid-memsafety.i true 2 wit inspect .028 .028 .19 8.1 0   .11  - - error 3.7 2.1 86 250 true 13 7.3 190 370
array-memsafety/array02-alloca_true-valid-memsafety.i true 2 wit inspect .026 .026 .23 7.9 0   0     - - error 4.2 2.3 59 250 true 14 7.5 200 400
array-memsafety/array03-alloca_true-valid-memsafety.i true 2 wit inspect .041 .16  .94 44   0   36     - - error 3.9 2.1 60 250 true 13 7.2 170 410
array-memsafety/bubblesort-alloca_true-valid-memsafety.i true 2 wit inspect .066 .18  .40 44   0   36     - - error 4.1 2.3 71 250 true 16 8.8 280 380
array-memsafety/count_down-alloca_true-valid-memsafety.i true 2 wit inspect .029 .029 .21 7.9 0   0     - - error 3.9 2.2 63 250 true 19 11   390 490
array-memsafety/cstrcat-alloca_true-valid-memsafety.i true 2 wit inspect .030 .032 .18 8.1 0   0     - - error 4.1 2.3 48 260 timeout 960 880   18000 4600
array-memsafety/cstrchr-alloca_true-valid-memsafety.i true 2 wit inspect .028 .028 .18 7.9 0   0     - - error 4.0 2.3 87 250 true 16 9.4 320 570
array-memsafety/cstrcmp-alloca_true-valid-memsafety.i true 2 wit inspect .028 .028 .20 7.8 0   0     - - error 4.1 2.2 76 240 true 36 25   400 700
array-memsafety/cstrcpy-alloca_true-valid-memsafety.i true 2 wit inspect .059 .059 .15 8.0 0   0     - - error 4.3 2.3 58 260 timeout 960 840   26000 1900
array-memsafety/cstrcspn-alloca_true-valid-memsafety.i true 2 wit inspect .028 .028 .20 8.3 0   .22  - - error 4.0 2.2 77 260 true 33 22   590 630
array-memsafety/cstrlen-alloca_true-valid-memsafety.i true 2 wit inspect .030 .030 .16 7.9 0   0     - - error 3.7 2.0 65 250 true 16 8.9 270 530
array-memsafety/cstrncat-alloca_true-valid-memsafety.i true 2 wit inspect .039 .039 .17 8.0 0   0     - - error 4.9 2.7 42 270 timeout 960 910   19000 1500
array-memsafety/cstrncmp-alloca_true-valid-memsafety.i true 2 wit inspect .079 .20  .55 43   0   35     - - error 4.1 2.3 75 250 true 35 24   680 680
array-memsafety/cstrncpy-alloca_true-valid-memsafety.i true 2 wit inspect .027 .028 .19 7.8 0   0     - - error 4.1 2.3 94 250 timeout 960 860   28000 4600
array-memsafety/cstrpbrk-alloca_true-valid-memsafety.i true 2 wit inspect .029 .029 .17 7.9 0   0     - - error 4.2 2.4 79 250 true 53 40   1100 730
array-memsafety/cstrspn-alloca_true-valid-memsafety.i true 2 wit inspect .082 .20  .47 43   0   35     - - error 6.0 3.3 61 250 true 65 50   1100 710
array-memsafety/diff-alloca_true-valid-memsafety.i true 2 wit inspect .038 .038 .19 8.0 0   0     - - error 3.8 2.1 35 260 true 26 15   460 520
array-memsafety/insertionsort-alloca_true-valid-memsafety.i true 2 wit inspect .026 .029 .15 8.0 0   0     - - error 4.6 2.5 48 260 true 19 11   280 510
array-memsafety/java_BubbleSort-alloca_true-valid-memsafety.i true 2 wit inspect .023 .024 .17 8.2 0   .22  - - error 3.7 2.1 31 250 true 15 8.4 280 400
array-memsafety/lis-alloca_true-valid-memsafety.i true 2 wit inspect .030 .031 .18 8.1 0   0     - - error 3.7 2.0 50 250 true 22 12   330 610
array-memsafety/mult_array-alloca_true-valid-memsafety.i true 2 wit inspect .040 .042 .16 8.1 0   .22  - - error 5.0 2.8 60 260 true 33 25   680 530
array-memsafety/openbsd_cbzero-alloca_true-valid-memsafety.i true 2 wit inspect .081 .20  .65 44   0   36     - - error 5.1 2.8 50 260 true 17 9.6 250 560
array-memsafety/openbsd_cmemchr-alloca_true-valid-memsafety.i true 2 wit inspect .026 .026 .23 8.2 0   0     - - error 4.4 2.4 99 250 true 17 9.4 240 540
array-memsafety/openbsd_cmemrchr-alloca_true-valid-memsafety.i true 2 wit inspect .030 .031 .15 7.8 0   0     - - error 4.4 2.4 77 250 true 21 13   330 540
array-memsafety/openbsd_cmemset-alloca_true-valid-memsafety.i true 2 wit inspect .030 .030 .16 7.8 0   0     - - error 3.8 2.1 45 250 true 15 8.5 200 530
array-memsafety/openbsd_cstpcpy-alloca_true-valid-memsafety.i true 2 wit inspect .027 .028 .23 8.2 0   .098 - - error 4.8 2.6 44 250 timeout 960 830   20000 2400
array-memsafety/openbsd_cstpncpy-alloca_true-valid-memsafety.i true 2 wit inspect .042 .043 .18 8.3 0   .18  - - error 3.9 2.2 85 250 timeout 960 840   19000 1500
array-memsafety/openbsd_cstrcat-alloca_true-valid-memsafety.i true 2 wit inspect .029 .029 .18 7.9 0   0     - - error 5.1 2.8 64 250 timeout 960 870   19000 4600
array-memsafety/openbsd_cstrcmp-alloca_true-valid-memsafety.i true 2 wit inspect .031 .031 .15 7.9 0   0     - - error 4.3 2.4 72 260 true 46 32   550 540
array-memsafety/openbsd_cstrcpy-alloca_true-valid-memsafety.i true 2 wit inspect .080 .20  .49 44   0   36     - - error 4.3 2.4 50 250 timeout 960 840   23000 2300
array-memsafety/openbsd_cstrcspn-alloca_true-valid-memsafety.i true 2 wit inspect .065 .18  .49 44   0   36     - - error 4.2 2.3 95 260 true 33 21   430 700
array-memsafety/openbsd_cstrlcpy-alloca_true-valid-memsafety.i true 2 wit inspect .032 .032 .16 8.0 0   0     - - error 4.0 2.2 33 260 timeout 960 830   21000 2100
array-memsafety/openbsd_cstrlen-alloca_true-valid-memsafety.i true 2 wit inspect .027 .027 .19 8.0 0   0     - - error 3.7 2.0 56 250 true 16 9.3 260 550
array-memsafety/openbsd_cstrncat-alloca_true-valid-memsafety.i true 2 wit inspect .040 .041 .20 8.3 0   0     - - error 4.0 2.2 59 260 timeout 960 920   16000 2400
array-memsafety/openbsd_cstrncmp-alloca_true-valid-memsafety.i true 2 wit inspect .041 .043 .16 7.9 0   0     - - error 4.2 2.3 68 250 true 43 30   560 740
array-memsafety/openbsd_cstrncpy-alloca_true-valid-memsafety.i true 2 wit inspect .032 .032 .17 8.0 0   0     - - error 4.2 2.4 88 250 timeout 960 830   26000 1800
array-memsafety/openbsd_cstrnlen-alloca_true-valid-memsafety.i true 2 wit inspect .030 .031 .21 8.2 0   0     - - error 4.2 2.3 58 260 true 19 11   260 530
array-memsafety/openbsd_cstrpbrk-alloca_true-valid-memsafety.i true 2 wit inspect .039 .039 .18 8.0 0   0     - - error 4.0 2.2 76 270 true 47 34   720 670
array-memsafety/openbsd_cstrspn-alloca_true-valid-memsafety.i true 2 wit inspect .078 .19  .44 44   0   36     - - error 4.1 2.3 86 250 true 44 32   520 710
array-memsafety/openbsd_cstrstr-alloca_true-valid-memsafety.i true 2 wit inspect .029 .029 .19 8.2 0   0     - - error 4.3 2.4 78 260 timeout 960 870   24000 1600
array-memsafety/rec_strlen-alloca_true-valid-memsafety.i true 2 wit inspect .033 .033 .14 8.1 0   0     - - error 3.6 2.0 44 240 true 22 15   430 560
array-memsafety/selectionsort-alloca_true-valid-memsafety.i true 2 wit inspect .023 .024 .16 8.1 0   .22  - - error 4.1 2.2 84 250 true 18 10   240 530
array-memsafety/stroeder1-alloca_true-valid-memsafety.i true 2 wit inspect .029 .029 .16 7.9 0   0     - - error 4.5 2.5 66 260 true 15 8.4 210 390
array-memsafety/stroeder2-alloca_true-valid-memsafety.i true 2 wit inspect .040 .042 .18 8.2 0   .22  - - error 3.8 2.1 63 250 true 14 8.0 260 410
array-memsafety/strreplace-alloca_true-valid-memsafety.i true 2 wit inspect .052 .16  .44 43   0   35     - - error 4.7 2.6 52 240 true 25 16   520 610
array-memsafety/subseq-alloca_true-valid-memsafety.i true 2 wit inspect .031 .031 .15 8.0 0   0     - - error 4.0 2.2 67 240 true 68 57   1900 700
array-memsafety/substring-alloca_true-valid-memsafety.i true 2 wit inspect .030 .032 .17 8.2 0   0     - - error 4.2 2.3 71 260 true 82 66   1100 810
array-examples/relax_false-valid-deref.i unknown 0 wit inspect .028 .028 .16 8.0 0   0     error (invalid witness file) .48 .32 7.2 39 error (invalid witness file) 7.0 3.7 100 300 - -
array-examples/sanfoundry_24_false-valid-deref.i false(valid-deref) 1 wit inspect .027 .027 .15 7.9 0   0     timeout 94    76    1500   3800 true 8.4 4.5 140 330 - -
array-examples/standard_strcpy_false-valid-deref_ground.i false(valid-deref) 1 wit inspect .024 .025 .13 7.9 0   0     timeout 94    67    900   3200 true 7.3 4.0 150 330 - -
array-examples/standard_strcpy_original_false-valid-deref.i false(valid-deref) 1 wit inspect .023 .024 .11 7.8 0   0     timeout 95    69    1400   3300 true 7.7 4.2 130 330 - -
../../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 116 2.6  3.9  16   970 0   420 69 450 320 6700 19000   69 170 91 3000 6900   69 200 110 3100 12000   69 13000 12000 300000 53000  
    correct results 68 116 2.5  3.9  16   960 0   420 6 450 320 6700 19000   20 160 87 2900 6600   0 200 110 3100 12000   35 13000 12000 300000 53000  
        correct true 48 96 1.9  2.9  12   710 0   320 0 0 0 0 0   11 0 0 0 0   0 200 110 3100 12000   35 13000 12000 300000 53000  
        correct false 20 20 .68 .99 4.3 250 0   95 6 450 320 6700 19000   9 160 87 2900 6600   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) 116
Run set sv-comp17.MemSafety-Arrays