Tool ULTIMATE Taipan f7c3ed31
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 16:15:06 CET [[ 2017-01-15 05:45:52 CET ]] [[ 2017-01-15 06:00:59 CET ]] [[ 2017-01-15 05:46:10 CET ]] [[ 2017-01-15 06:02:27 CET ]]
Run set sv-comp17.MemSafety-Arrays
Options [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/utaipan.2017-01-14_1615.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/utaipan.2017-01-14_1615.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/utaipan.2017-01-14_1615.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/utaipan.2017-01-14_1615.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 6.1 2.0 49 320 2.5 0   4.8  2.6  62   270 9.2 4.9 160 350
array-memsafety/bubblesort_unsafe_false-valid-deref.i 1 6.2 2.1 45 320 2.5 0   3.5  2.0  63   250 8.1 4.3 160 340
array-memsafety/count_down_unsafe_false-valid-deref.i 1 6.4 2.0 49 350 2.5 0   4.8  2.6  63   270 9.1 4.9 170 350
array-memsafety/cstrcat_unsafe_false-valid-deref.i 1 5.9 1.7 43 330 2.5 0   3.1  1.7  57   250 8.0 4.3 170 340
array-memsafety/cstrchr_unsafe_false-valid-deref.i 1 14   4.3 120 490 2.5 0   4.7  2.6  71   270 11   5.8 200 370
array-memsafety/cstrlen_unsafe_false-valid-deref.i 1 7.9 2.5 61 380 2.5 0   4.5  2.5  49   270 14   7.7 150 360
array-memsafety/cstrncat_unsafe_false-valid-deref.i 1 5.8 1.9 43 320 2.9 0   3.2  1.7  36   250 8.1 4.3 160 350
array-memsafety/cstrncpy_unsafe_false-valid-deref.i 1 6.0 1.8 50 340 2.5 0   2.4  1.4  31   160 7.7 4.1 150 310
array-memsafety/cstrpbrk_unsafe_false-valid-deref.i 1 180   170   2000 690 2.5 0   4.9  2.7  79   270 8.8 4.7 160 350
array-memsafety/diff_usafe_false-valid-deref.i 1 6.1 1.9 46 330 2.5 0   4.0  2.3  58   250 7.3 3.9 140 300
array-memsafety/knapsack_alloca_unsafe_false-valid-deref.i 1 11   5.4 90 380 2.5 0   2.9  1.6  35   180 12   6.5 200 380
array-memsafety/lis_unsafe_false-valid-deref.i 1 18   6.7 150 460 2.6 0   2.9  1.6  52   190 13   7.3 200 420
array-memsafety/mult_array_unsafe_false-valid-deref.i 1 7.2 2.9 63 330 2.5 0   5.3  2.9  56   270 9.0 4.8 170 350
array-memsafety/reverse_array_alloca_unsafe_false-valid-deref.i 1 7.0 2.2 55 360 2.5 0   4.9  2.7  76   270 14   7.7 220 460
array-memsafety/reverse_array_unsafe_false-valid-deref.i 1 7.1 2.2 53 350 2.5 0   4.4  2.4  65   260 10   5.6 160 360
array-memsafety/selectionsort_unsafe_false-valid-deref.i 1 6.1 1.9 55 330 2.5 0   3.9  2.1  66   260 9.8 5.3 120 340
array-memsafety/stroeder1_unsafe_false-valid-deref.i 1 6.6 1.9 54 350 2.5 0   3.1  1.7  29   250 8.8 4.7 180 340
array-memsafety/add_last-alloca_true-valid-memsafety.i 0 900   860   9600 4700 2.3 0   .54 .34 12   40 6.3 3.3 120 310
array-memsafety/array01-alloca_true-valid-memsafety.i 2 10   3.1 86 450 2.5 0   3.6  2.0  54   240 14   7.5 210 400
array-memsafety/array02-alloca_true-valid-memsafety.i 2 11   3.5 90 480 2.5 0   3.8  2.1  53   250 13   7.3 250 420
array-memsafety/array03-alloca_true-valid-memsafety.i 2 11   3.4 99 500 2.5 0   4.0  2.2  82   250 13   7.4 200 410
array-memsafety/bubblesort-alloca_true-valid-memsafety.i 2 11   3.4 85 440 2.5 0   4.1  2.3  91   250 14   7.7 190 400
array-memsafety/count_down-alloca_true-valid-memsafety.i 2 13   4.1 100 500 2.5 0   4.0  2.2  70   250 16   9.1 210 550
array-memsafety/cstrcat-alloca_true-valid-memsafety.i 0 900   820   11000 2900 2.3 0   .49 .31 9.5 40 6.3 3.4 130 310
array-memsafety/cstrchr-alloca_true-valid-memsafety.i 2 15   5.0 130 520 2.7 0   4.0  2.2  82   250 16   9.3 260 580
array-memsafety/cstrcmp-alloca_true-valid-memsafety.i 2 44   26   420 830 2.5 0   3.9  2.2  70   250 34   24   360 670
array-memsafety/cstrcpy-alloca_true-valid-memsafety.i 0 900   830   13000 1200 2.3 0   .51 .33 12   41 6.0 3.2 120 300
array-memsafety/cstrcspn-alloca_true-valid-memsafety.i 2 36   19   340 610 2.6 0   3.8  2.1  74   250 30   20   340 720
array-memsafety/cstrlen-alloca_true-valid-memsafety.i 2 14   4.4 110 500 2.5 0   3.9  2.1  79   250 16   8.8 230 550
array-memsafety/cstrncat-alloca_true-valid-memsafety.i 0 900   810   11000 1600 2.3 0   .49 .32 9.5 40 6.5 3.5 120 300
array-memsafety/cstrncmp-alloca_true-valid-memsafety.i 2 37   22   420 770 2.6 0   4.2  2.3  62   250 33   23   460 650
array-memsafety/cstrncpy-alloca_true-valid-memsafety.i 0 900   800   12000 1500 2.3 0   .51 .33 10   40 6.5 3.4 140 300
array-memsafety/cstrpbrk-alloca_true-valid-memsafety.i 2 61   43   650 880 2.5 0   4.2  2.3  82   250 53   40   700 730
array-memsafety/cstrspn-alloca_true-valid-memsafety.i 2 62   44   740 700 2.5 0   4.3  2.4  86   250 56   42   790 710
array-memsafety/diff-alloca_true-valid-memsafety.i 2 33   21   340 690 2.5 0   4.1  2.3  71   250 23   13   360 570
array-memsafety/insertionsort-alloca_true-valid-memsafety.i 2 15   4.9 110 500 2.5 0   4.1  2.2  83   250 18   10   220 540
array-memsafety/java_BubbleSort-alloca_true-valid-memsafety.i 2 11   3.3 78 440 2.5 0   4.1  2.2  74   260 14   7.7 240 440
array-memsafety/lis-alloca_true-valid-memsafety.i 0 900   870   9200 790 2.5 0   .62 .40 8.0 41 5.7 3.0 110 300
array-memsafety/mult_array-alloca_true-valid-memsafety.i 2 65   54   800 530 2.5 0   4.0  2.2  78   260 25   17   390 530
array-memsafety/openbsd_cbzero-alloca_true-valid-memsafety.i 2 15   5.1 110 570 2.5 0   4.2  2.3  75   250 17   9.7 250 520
array-memsafety/openbsd_cmemchr-alloca_true-valid-memsafety.i 2 14   4.5 110 510 2.5 0   4.1  2.3  75   250 15   8.6 220 540
array-memsafety/openbsd_cmemrchr-alloca_true-valid-memsafety.i 2 27   17   260 530 2.5 0   3.8  2.1  74   240 27   18   270 530
array-memsafety/openbsd_cmemset-alloca_true-valid-memsafety.i 2 14   4.5 120 500 2.5 0   4.3  2.3  93   260 15   8.6 270 520
array-memsafety/openbsd_cstpcpy-alloca_true-valid-memsafety.i 0 900   820   12000 1500 2.3 0   .50 .33 13   39 6.3 3.3 130 300
array-memsafety/openbsd_cstpncpy-alloca_true-valid-memsafety.i 0 910   500   7700 9900 2.5 0   .49 .31 7.5 39 6.2 3.3 120 300
array-memsafety/openbsd_cstrcat-alloca_true-valid-memsafety.i 0 900   810   11000 3100 2.7 0   .51 .31 12   40 7.2 3.8 87 300
array-memsafety/openbsd_cstrcmp-alloca_true-valid-memsafety.i 2 67   49   770 620 2.5 0   4.1  2.3  71   250 38   27   720 670
array-memsafety/openbsd_cstrcpy-alloca_true-valid-memsafety.i 0 900   820   12000 1700 2.3 0   .48 .32 9.4 40 5.9 3.1 120 300
array-memsafety/openbsd_cstrcspn-alloca_true-valid-memsafety.i 0 900   860   11000 1500 2.5 0   .52 .35 9.6 41 6.4 3.4 130 300
array-memsafety/openbsd_cstrlcpy-alloca_true-valid-memsafety.i 0 900   840   12000 930 2.3 0   .52 .35 11   40 5.7 3.0 110 300
array-memsafety/openbsd_cstrlen-alloca_true-valid-memsafety.i 2 14   4.5 120 550 2.5 0   3.8  2.1  60   250 15   8.7 230 550
array-memsafety/openbsd_cstrncat-alloca_true-valid-memsafety.i 0 900   500   5900 11000 2.3 0   .49 .31 6.8 40 8.3 4.3 110 320
array-memsafety/openbsd_cstrncmp-alloca_true-valid-memsafety.i 2 94   78   1100 800 2.5 0   4.0  2.2  84   250 48   34   830 690
array-memsafety/openbsd_cstrncpy-alloca_true-valid-memsafety.i 0 900   840   12000 910 2.3 0   .50 .32 5.5 39 6.2 3.3 110 310
array-memsafety/openbsd_cstrnlen-alloca_true-valid-memsafety.i 2 16   5.4 130 640 2.5 0   4.1  2.2  78   250 18   10   230 490
array-memsafety/openbsd_cstrpbrk-alloca_true-valid-memsafety.i 2 49   34   540 720 2.5 0   3.9  2.2  51   260 40   30   460 670
array-memsafety/openbsd_cstrspn-alloca_true-valid-memsafety.i 2 85   68   1100 660 2.5 0   3.9  2.2  70   250 44   32   530 710
array-memsafety/openbsd_cstrstr-alloca_true-valid-memsafety.i 0 900   870   10000 1200 2.3 0   .54 .36 12   43 6.1 3.2 120 300
array-memsafety/rec_strlen-alloca_true-valid-memsafety.i 2 19   9.5 170 510 2.5 0   3.8  2.1  67   250 21   14   380 550
array-memsafety/selectionsort-alloca_true-valid-memsafety.i 2 14   4.2 110 570 2.5 0   3.9  2.2  80   250 15   8.3 200 530
array-memsafety/stroeder1-alloca_true-valid-memsafety.i 2 10   3.2 80 470 2.5 0   3.9  2.1  64   250 13   7.1 220 410
array-memsafety/stroeder2-alloca_true-valid-memsafety.i 2 12   3.4 83 480 2.5 0   3.8  2.1  60   250 14   7.6 220 420
array-memsafety/strreplace-alloca_true-valid-memsafety.i 2 19   6.6 140 590 2.5 0   3.8  2.1  57   270 34   22   380 510
array-memsafety/subseq-alloca_true-valid-memsafety.i 2 91   75   1000 730 2.5 0   3.9  2.2  68   250 58   46   1000 660
array-memsafety/substring-alloca_true-valid-memsafety.i 2 50   33   520 820 2.5 0   4.0  2.2  72   250 82   67   920 800
array-examples/relax_false-valid-deref.i 1 6.4 2.0 53 320 2.5 0   3.2  1.8  58   210 10   5.4 180 350
array-examples/sanfoundry_24_false-valid-deref.i 0 900   740   14000 1700 2.3 0   .48 .31 6.9 39 6.1 3.2 110 300
array-examples/standard_strcpy_false-valid-deref_ground.i 0 900   740   14000 1900 2.7 0   .51 .32 11   40 6.4 3.3 130 300
array-examples/standard_strcpy_original_false-valid-deref.i 0 900   730   14000 1700 2.4 0   .53 .34 12   40 5.5 3.0 100 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 84 18000 15000 220000 76000 170 0   69 72 40 1000 4500   69 200 110 3400 7300   69 140 78 2500 8900   69 1000 660 15000 23000  
    correct results 51 84 1400 880 14000 26000 130 0   13 71 39 1000 4400   18 180 96 3100 6400   0 130 73 2400 8300   33 900 610 13000 19000  
        correct true 33 66 1100 670 11000 20000 84 0   10 0 0 0 0   1 0 0 0 0   0 130 73 2400 8300   33 900 610 13000 19000  
        correct false 18 18 310 210 3100 6800 46 0   3 71 39 1000 4400   17 180 96 3100 6400   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) 84
Run set sv-comp17.MemSafety-Arrays