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