Tool ULTIMATE Kojak 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 06:29:29 CET [[ 2017-01-15 05:44:30 CET ]] [[ 2017-01-15 05:59:35 CET ]] [[ 2017-01-15 05:44:48 CET ]] [[ 2017-01-15 06:00:32 CET ]]
Run set sv-comp17.MemSafety-Arrays
Options [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ukojak.2017-01-14_0629.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ukojak.2017-01-14_0629.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ukojak.2017-01-14_0629.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ukojak.2017-01-14_0629.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 6.6 2.1 53 320 2.9 0   error 4.5  2.5  75 260 false(valid-deref) 9.4 5.0 180 350 - -
array-memsafety/bubblesort_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 5.9 1.9 49 330 2.7 0   false(valid-deref) 4.0  2.2  37 270 false(valid-deref) 8.1 4.4 160 350 - -
array-memsafety/count_down_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 6.8 2.2 52 320 2.5 0   error 4.3  2.4  66 260 false(valid-deref) 9.3 5.0 190 350 - -
array-memsafety/cstrcat_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 5.7 1.8 47 320 2.5 0   true 3.0  1.7  26 250 false(valid-deref) 7.9 4.3 150 340 - -
array-memsafety/cstrchr_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 9.9 2.9 83 490 2.5 0   error 4.4  2.4  41 260 false(valid-deref) 11   5.7 190 360 - -
array-memsafety/cstrlen_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 11   3.3 85 480 2.5 0   error 4.3  2.4  42 260 false(valid-deref) 9.9 5.4 160 360 - -
array-memsafety/cstrncat_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 5.7 1.8 42 320 2.5 0   true 3.1  1.7  60 250 false(valid-deref) 8.2 4.4 150 350 - -
array-memsafety/cstrncpy_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 6.6 1.9 50 350 2.5 0   error (invalid witness file) 2.2  1.3  30 160 false(valid-deref) 7.3 3.9 150 320 - -
array-memsafety/cstrpbrk_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 11   3.4 83 480 2.5 0   error 4.3  2.4  39 260 false(valid-deref) 8.8 4.7 170 350 - -
array-memsafety/diff_usafe_false-valid-deref.i false(valid-deref) 1 wit inspect 6.2 2.0 49 320 2.5 0   true 3.8  2.1  75 250 false(valid-deref) 8.9 4.7 140 340 - -
array-memsafety/knapsack_alloca_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 8.1 2.4 58 380 2.5 0   error (invalid witness file) 2.9  1.6  54 190 true 13   7.3 180 420 - -
array-memsafety/lis_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 41   25   440 700 2.5 0   error (invalid witness file) 2.9  1.6  39 180 false(valid-deref) 11   5.8 190 360 - -
array-memsafety/mult_array_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 7.1 2.3 59 320 2.5 0   error 4.6  2.5  56 270 false(valid-deref) 12   6.6 130 350 - -
array-memsafety/reverse_array_alloca_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 11   3.2 89 510 2.5 0   error 4.5  2.4  42 260 true 14   7.8 230 460 - -
array-memsafety/reverse_array_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 7.5 2.2 64 350 2.5 0   error 4.3  2.3  39 270 false(valid-deref) 11   6.1 210 390 - -
array-memsafety/selectionsort_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 6.7 2.0 47 330 2.5 0   false(valid-deref) 4.5  2.5  34 260 false(valid-deref) 8.4 4.6 160 340 - -
array-memsafety/stroeder1_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 5.6 1.8 41 320 2.5 0   false(valid-deref) 3.5  1.9  60 260 false(valid-deref) 7.8 4.3 140 350 - -
array-memsafety/add_last-alloca_true-valid-memsafety.i timeout 0 wit inspect 900   820   14000 860 2.3 0   - - error (invalid witness file) .54 .35 11   40 error (invalid witness file) 6.4 3.4 120 310
array-memsafety/array01-alloca_true-valid-memsafety.i true 2 wit inspect 15   5.7 150 540 2.5 0   - - error 3.9  2.2  58   260 true 13   7.3 240 390
array-memsafety/array02-alloca_true-valid-memsafety.i true 2 wit inspect 19   6.9 180 530 2.5 0   - - error 4.0  2.2  81   250 true 13   7.1 230 410
array-memsafety/array03-alloca_true-valid-memsafety.i timeout 0 wit inspect 900   800   12000 1000 2.3 0   - - error (invalid witness file) .50 .32 13   40 error (invalid witness file) 6.2 3.3 130 290
array-memsafety/bubblesort-alloca_true-valid-memsafety.i true 2 wit inspect 38   23   380 880 2.5 0   - - error 3.9  2.2  35   250 true 14   7.6 210 400
array-memsafety/count_down-alloca_true-valid-memsafety.i true 2 wit inspect 46   30   550 700 2.5 0   - - error 3.7  2.1  47   250 true 16   9.2 290 530
array-memsafety/cstrcat-alloca_true-valid-memsafety.i timeout 0 wit inspect 900   840   15000 1300 2.3 0   - - error (invalid witness file) .51 .33 12   39 error (invalid witness file) 5.8 3.1 110 300
array-memsafety/cstrchr-alloca_true-valid-memsafety.i true 2 wit inspect 27   13   300 580 2.5 0   - - error 3.9  2.1  36   250 true 16   9.4 360 540
array-memsafety/cstrcmp-alloca_true-valid-memsafety.i true 2 wit inspect 230   200   3400 1000 2.5 0   - - error 3.9  2.1  47   260 true 35   25   540 710
array-memsafety/cstrcpy-alloca_true-valid-memsafety.i timeout 0 wit inspect 900   830   12000 1800 2.3 0   - - error (invalid witness file) .52 .32 9.7 41 error (invalid witness file) 5.6 3.0 120 290
array-memsafety/cstrcspn-alloca_true-valid-memsafety.i timeout 0 wit inspect 900   820   13000 1500 2.3 0   - - error (invalid witness file) .54 .35 12   40 error (invalid witness file) 6.1 3.2 120 300
array-memsafety/cstrlen-alloca_true-valid-memsafety.i true 2 wit inspect 17   7.6 160 520 2.5 0   - - error 3.7  2.1  50   240 true 16   8.9 260 520
array-memsafety/cstrncat-alloca_true-valid-memsafety.i timeout 0 wit inspect 900   840   11000 1400 2.5 0   - - error (invalid witness file) .52 .36 11   41 error (invalid witness file) 6.1 3.2 120 300
array-memsafety/cstrncmp-alloca_true-valid-memsafety.i true 2 wit inspect 410   360   5000 1300 2.5 0   - - error 3.8  2.1  42   250 true 34   24   530 620
array-memsafety/cstrncpy-alloca_true-valid-memsafety.i timeout 0 wit inspect 900   820   14000 2600 2.3 0   - - error (invalid witness file) .48 .31 9.0 39 error (invalid witness file) 6.1 3.3 120 300
array-memsafety/cstrpbrk-alloca_true-valid-memsafety.i timeout 0 wit inspect 900   830   12000 1600 2.3 0   - - error (invalid witness file) .53 .35 10   41 error (invalid witness file) 6.0 3.1 120 300
array-memsafety/cstrspn-alloca_true-valid-memsafety.i timeout 0 wit inspect 900   830   13000 1600 2.3 0   - - error (invalid witness file) .55 .36 9.9 39 error (invalid witness file) 5.7 3.1 120 290
array-memsafety/diff-alloca_true-valid-memsafety.i timeout 0 wit inspect 900   840   12000 1000 2.3 0   - - error (invalid witness file) .49 .32 9.3 40 error (invalid witness file) 6.9 3.6 130 320
array-memsafety/insertionsort-alloca_true-valid-memsafety.i true 2 wit inspect 30   17   270 610 2.5 0   - - error 4.0  2.2  80   260 true 17   9.7 340 510
array-memsafety/java_BubbleSort-alloca_true-valid-memsafety.i true 2 wit inspect 32   17   380 670 2.5 0   - - error 4.0  2.2  59   250 true 13   7.5 250 440
array-memsafety/lis-alloca_true-valid-memsafety.i timeout 0 wit inspect 900   830   11000 1400 2.3 0   - - error (invalid witness file) .51 .33 12   40 error (invalid witness file) 5.9 3.1 120 290
array-memsafety/mult_array-alloca_true-valid-memsafety.i timeout 0 wit inspect 900   880   13000 740 2.3 0   - - error (invalid witness file) .50 .32 10   39 error (invalid witness file) 6.3 3.3 130 300
array-memsafety/openbsd_cbzero-alloca_true-valid-memsafety.i true 2 wit inspect 18   7.7 180 540 2.5 0   - - error 3.6  2.0  33   240 true 17   9.8 350 570
array-memsafety/openbsd_cmemchr-alloca_true-valid-memsafety.i true 2 wit inspect 12   4.8 100 480 2.5 0   - - error 3.6  2.0  44   240 true 15   8.5 210 530
array-memsafety/openbsd_cmemrchr-alloca_true-valid-memsafety.i true 2 wit inspect 12   4.5 120 480 2.5 0   - - error 4.1  2.2  83   250 true 20   13   430 550
array-memsafety/openbsd_cmemset-alloca_true-valid-memsafety.i true 2 wit inspect 12   4.6 110 490 2.5 0   - - error 4.2  2.3  85   260 true 15   8.4 280 560
array-memsafety/openbsd_cstpcpy-alloca_true-valid-memsafety.i timeout 0 wit inspect 900   830   12000 1600 2.4 0   - - error (invalid witness file) .51 .32 12   39 error (invalid witness file) 5.5 3.0 120 290
array-memsafety/openbsd_cstpncpy-alloca_true-valid-memsafety.i timeout 0 wit inspect 900   830   14000 1100 2.3 0   - - error (invalid witness file) .54 .35 11   39 error (invalid witness file) 5.9 3.2 120 300
array-memsafety/openbsd_cstrcat-alloca_true-valid-memsafety.i timeout 0 wit inspect 900   840   11000 1400 2.3 0   - - error (invalid witness file) .49 .32 12   39 error (invalid witness file) 5.8 3.1 120 300
array-memsafety/openbsd_cstrcmp-alloca_true-valid-memsafety.i true 2 wit inspect 350   310   4800 1200 2.5 0   - - error 4.1  2.2  47   250 true 41   29   640 740
array-memsafety/openbsd_cstrcpy-alloca_true-valid-memsafety.i timeout 0 wit inspect 900   830   12000 1800 2.3 0   - - error (invalid witness file) .47 .30 10   40 error (invalid witness file) 5.7 3.0 130 300
array-memsafety/openbsd_cstrcspn-alloca_true-valid-memsafety.i timeout 0 wit inspect 900   830   12000 1600 2.3 0   - - error (invalid witness file) .49 .32 9.5 40 error (invalid witness file) 5.8 3.1 120 290
array-memsafety/openbsd_cstrlcpy-alloca_true-valid-memsafety.i timeout 0 wit inspect 900   830   11000 1200 2.3 0   - - error (invalid witness file) .51 .34 12   40 error (invalid witness file) 6.2 3.3 120 300
array-memsafety/openbsd_cstrlen-alloca_true-valid-memsafety.i true 2 wit inspect 16   7.6 140 590 2.5 0   - - error 4.0  2.2  48   260 true 16   9.1 270 490
array-memsafety/openbsd_cstrncat-alloca_true-valid-memsafety.i timeout 0 wit inspect 900   840   11000 1300 2.3 0   - - error (invalid witness file) .49 .32 13   39 error (invalid witness file) 6.0 3.2 110 300
array-memsafety/openbsd_cstrncmp-alloca_true-valid-memsafety.i true 2 wit inspect 310   270   4400 1300 2.5 0   - - error 3.7  2.1  45   250 true 44   30   800 650
array-memsafety/openbsd_cstrncpy-alloca_true-valid-memsafety.i timeout 0 wit inspect 900   820   11000 1600 2.3 0   - - error (invalid witness file) .54 .35 12   40 error (invalid witness file) 5.7 3.1 110 290
array-memsafety/openbsd_cstrnlen-alloca_true-valid-memsafety.i true 2 wit inspect 27   14   280 580 2.5 0   - - error 3.7  2.1  39   250 true 19   11   260 570
array-memsafety/openbsd_cstrpbrk-alloca_true-valid-memsafety.i timeout 0 wit inspect 900   840   13000 1400 2.3 0   - - error (invalid witness file) .52 .33 9.6 41 error (invalid witness file) 5.9 3.1 120 300
array-memsafety/openbsd_cstrspn-alloca_true-valid-memsafety.i timeout 0 wit inspect 900   840   12000 1700 2.4 0   - - error (invalid witness file) .49 .33 8.4 39 error (invalid witness file) 6.0 3.2 120 300
array-memsafety/openbsd_cstrstr-alloca_true-valid-memsafety.i timeout 0 wit inspect 900   830   12000 1500 2.3 0   - - error (invalid witness file) .48 .32 9.4 40 error (invalid witness file) 6.8 3.5 130 310
array-memsafety/rec_strlen-alloca_true-valid-memsafety.i true 2 wit inspect 17   7.7 150 510 2.5 0   - - error 3.7  2.1  36   250 true 30   23   530 550
array-memsafety/selectionsort-alloca_true-valid-memsafety.i timeout 0 wit inspect 900   830   12000 2100 2.7 0   - - error (invalid witness file) .57 .35 9.5 43 error (invalid witness file) 5.6 2.9 110 300
array-memsafety/stroeder1-alloca_true-valid-memsafety.i true 2 wit inspect 9.9 2.8 88 480 2.5 0   - - error 4.0  2.2  83   250 true 13   7.5 240 420
array-memsafety/stroeder2-alloca_true-valid-memsafety.i true 2 wit inspect 21   9.1 200 710 2.5 0   - - error 3.6  2.0  49   250 true 14   7.7 230 400
array-memsafety/strreplace-alloca_true-valid-memsafety.i true 2 wit inspect 26   13   240 590 2.5 0   - - error 3.9  2.1  60   260 true 29   19   450 560
array-memsafety/subseq-alloca_true-valid-memsafety.i true 2 wit inspect 470   420   5900 1600 2.5 0   - - error 3.8  2.1  48   270 true 52   42   1100 700
array-memsafety/substring-alloca_true-valid-memsafety.i timeout 0 wit inspect 900   830   11000 1500 2.3 0   - - error (invalid witness file) .51 .34 9.7 42 error (invalid witness file) 5.9 3.1 120 300
array-examples/relax_false-valid-deref.i false(valid-deref) 1 wit inspect 23   14   200 340 2.6 0   error 5.4  2.9  41 270 false(valid-deref) 9.5 5.1 180 360 - -
array-examples/sanfoundry_24_false-valid-deref.i timeout 0 wit inspect 900   760   14000 1300 2.3 0   error (invalid witness file) .56 .37 12 42 error (invalid witness file) 5.8 3.1 100 300 - -
array-examples/standard_strcpy_false-valid-deref_ground.i timeout 0 wit inspect 900   760   13000 1400 2.3 0   error (invalid witness file) .52 .34 10 39 error (invalid witness file) 6.6 3.4 130 310 - -
array-examples/standard_strcpy_original_false-valid-deref.i timeout 0 wit inspect 900   750   13000 1500 2.3 0   error (invalid witness file) .50 .32 11 40 error (invalid witness file) 6.3 3.3 110 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 64 28000 25000 370000 65000 170 0   69 72 40 890 4600   69 190 100 3400 7400   69 100 58 1500 6800   69 660 410 12000 20000  
    correct results 41 64 2400 1800 29000 24000 100 0   6 70 39 860 4400   18 180 95 3100 6500   0 89 49 1200 5800   23 510 330 9000 12000  
        correct true 23 46 2200 1800 27000 17000 58 0   3 0 0 0 0   2 0 0 0 0   0 89 49 1200 5800   23 510 330 9000 12000  
        correct false 18 18 190 77 1600 7000 46 0   3 70 39 860 4400   16 180 95 3100 6500   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) 64
Run set sv-comp17.MemSafety-Arrays