Tool SMACK+Corral 1.7.2
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 07:19:02 CET [[ 2017-01-15 04:32:52 CET ]] [[ 2017-01-15 05:00:11 CET ]] [[ 2017-01-15 04:38:10 CET ]] [[ 2017-01-15 05:08:13 CET ]]
Run set sv-comp17.Systems_BusyBox_Overflows
Options -w error-witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/smack.2017-01-14_0719.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/smack.2017-01-14_0719.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/smack.2017-01-14_0719.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/smack.2017-01-14_0719.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]
../../sv-benchmarks/c/busybox-1.22.0/ 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 wall energy mem validator uautomizer violation t<90s status cpu wall energy mem 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)
basename_false-unreach-call_true-no-overflow_false-valid-deref.i timeout 0 wit inspect 880    930    7400   540 1.4 0    - - error (invalid witness file) .50 .33 9.4 39 error (invalid witness file) 5.8 3.1 100 290
basename_false-unreach-call_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 880    930    8600   840 1.4 0    - - error (invalid witness file) .53 .36 7.6 42 error (invalid witness file) 6.3 3.3 95 300
chgrp-incomplete_true-no-overflow_false-valid-memtrack.i true 1 wit inspect 880    880    9600   440 1.5 0    - - exception 13    6.8  200   510 unknown 7.1 3.7 77 310
chroot-incomplete_true-no-overflow_true-valid-memsafety.i true 1 wit inspect 880    880    7500   480 1.6 0    - - error 34    18    480   680 unknown 6.5 3.4 92 300
cut_false-unreach-call_true-no-overflow_true-valid-memsafety.i true 1 wit inspect 880    880    7500   620 3.8 0    - - timeout 900    830    20000   5700 unknown 6.9 3.6 87 310
date_false-unreach-call_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 880    930    7600   800 6.2 0    - - error (invalid witness file) .54 .35 12   44 error (invalid witness file) 6.6 3.5 130 300
dirname_true-no-overflow_true-valid-memsafety.i true 1 wit inspect 880    880    10000   630 1.2 0    - - exception 9.4  5.0  180   370 error (1) 180   150   2200 1100
du_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 880    930    9500   3400 4.9 .14 - - error (invalid witness file) .49 .34 3.8 39 error (invalid witness file) 6.4 3.4 100 300
echo_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 880    930    8000   570 1.8 0    - - error (invalid witness file) .49 .32 9.4 40 error (invalid witness file) 6.3 3.4 79 300
expand_false-unreach-call_true-no-overflow_true-valid-memsafety.i true 1 wit inspect 880    880    7900   550 3.5 0    - - timeout 900    810    14000   5700 unknown 8.9 4.8 100 310
fold_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 880    930    7100   620 2.9 0    - - error (invalid witness file) .54 .35 7.6 40 error (invalid witness file) 6.3 3.3 70 300
head_true-no-overflow_false-valid-deref.i true 1 wit inspect 880    880    10000   400 2.1 0    - - out of memory 480    380    5500   7000 unknown 7.0 3.7 110 310
hostid_true-no-overflow_true-valid-memsafety.i true 2 wit inspect 880    880    12000   650 1.1 0    - - exception 10    5.4  190   410 true 13   6.9 190 400
logname_true-no-overflow_true-valid-memsafety.i true 1 wit inspect 880    880    10000   440 1.5 0    - - exception 15    7.9  280   530 unknown 6.8 3.6 73 310
ls-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 880    930    9600   3500 8.4 0    - - error (invalid witness file) .52 .33 13   42 error (invalid witness file) 6.2 3.3 90 300
mkdir_true-no-overflow_true-valid-memsafety.i true 1 wit inspect 880    880    7200   560 3.3 0    - - timeout 900    830    17000   5800 unknown 7.2 3.8 93 310
mkfifo-incomplete_true-no-overflow_true-valid-memsafety.i true 1 wit inspect 880    880    11000   440 1.5 0    - - exception 20    10    270   540 unknown 6.8 3.6 89 320
od_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (1) 0 wit inspect 1.2  1.2  17   63 5.7 0    - - error (invalid witness file) .53 .34 7.6 43 error (invalid witness file) 6.5 3.4 100 310
printf_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (1) 0 wit inspect .66 .65 7.7 41 3.2 0    - - error (invalid witness file) .47 .31 7.8 40 error (invalid witness file) 6.2 3.3 46 320
readlink_true-no-overflow_true-valid-memsafety.i true 1 wit inspect 880    880    9400   420 2.6 0    - - timeout 900    820    13000   5700 unknown 6.6 3.5 79 300
realpath_true-no-overflow_true-valid-memsafety.i true 1 wit inspect 880    880    7400   440 1.5 0    - - exception 21    11    270   570 unknown 6.8 3.6 93 310
rm_true-no-overflow_true-valid-memsafety.i true 1 wit inspect 880    880    6500   540 3.0 0    - - error (recursion) 7.3  3.9  160   340 unknown 7.1 3.8 120 300
seq_true-no-overflow_true-valid-memsafety.i true 1 wit inspect 880    880    7500   460 2.6 0    - - timeout 900    820    16000   5700 error (1) 7.0 3.7 110 310
sleep_true-no-overflow_false-valid-deref.i error (1) 0 wit inspect .55 .55 7.0 31 1.8 0    - - error (invalid witness file) .51 .32 9.3 40 error (invalid witness file) 6.4 3.4 87 300
stty_false-unreach-call_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 890    930    6400   640 6.5 0    - - error (invalid witness file) .50 .33 6.3 45 error (invalid witness file) 6.9 3.6 98 310
sync_true-no-overflow_true-valid-memsafety.i true 1 wit inspect 880    880    8800   450 1.4 0    - - exception 12    6.0  210   420 unknown 6.3 3.3 89 300
tac_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 880    930    8000   520 2.7 0    - - error (invalid witness file) .52 .35 7.9 41 error (invalid witness file) 6.4 3.4 92 300
tee_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 880    930    11000   3400 5.3 0    - - error (invalid witness file) .53 .33 12   39 error (invalid witness file) 6.5 3.4 97 300
test-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i true 1 wit inspect 880    880    7200   470 2.7 0    - - error (recursion) 7.8  4.1  140   350 unknown 6.7 3.6 74 300
touch_false-unreach-call_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 880    930    8100   640 3.4 0    - - error (invalid witness file) .50 .33 4.3 40 error (invalid witness file) 6.5 3.4 120 300
uname_true-no-overflow_true-valid-memsafety.i true 1 wit inspect 880    880    6200   490 2.6 0    - - timeout 900    820    11000   5700 unknown 7.0 3.6 89 310
uniq_true-no-overflow_true-valid-memsafety.i true 1 wit inspect 880    880    11000   550 2.8 0    - - timeout 900    820    18000   5700 unknown 8.3 4.4 110 310
usleep_true-no-overflow_true-valid-memsafety.i true 1 wit inspect 880    880    10000   1200 1.6 0    - - exception 19    9.8  290   440 unknown 6.0 3.2 94 300
uudecode_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 880    930    8000   1200 4.4 0    - - error (invalid witness file) .51 .33 9.7 41 error (invalid witness file) 7.0 3.7 95 310
wc_false-unreach-call_true-no-overflow_true-valid-memsafety.i true 1 wit inspect 880    880    7400   500 2.9 0    - - timeout 900    820    14000   5700 unknown 6.7 3.6 92 300
who_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 880    930    6200   540 2.7 0    - - error (invalid witness file) .51 .34 4.5 42 error (invalid witness file) 6.5 3.4 88 310
whoami-incomplete_true-no-overflow_true-valid-memsafety.i true 1 wit inspect 880    880    12000   660 1.5 0    - - exception 13    6.7  190   490 unknown 6.5 3.4 99 300
yes_true-no-overflow_true-valid-memsafety.i true 1 wit inspect 880    880    8600   520 1.5 0    - - exception 17    9.1  270   530 unknown 7.8 4.1 85 300
../../sv-benchmarks/c/busybox-1.22.0/ 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 wall energy mem validator uautomizer violation t<90s status cpu wall energy mem 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 38 23 31000 31000 300000 29000 110   .14 38 38 38 7900 7000   130000 59000 38 440 280   5800 12000
    correct results 1 2 880 880 12000 650 1.1 0    0 0 0 10 5.4 190 410 1 13 6.9 190 400
        correct true 1 2 880 880 12000 650 1.1 0    0 0 0 10 5.4 190 410 1 13 6.9 190 400
        correct false 0
    correct-unconfimed results 21 21 19000 18000 180000 11000 47   0    0 0 0 7900 7000   130000 58000 0 320 220   4100 7300
        correct-unconfirmed true 21 21 19000 18000 180000 11000 47   0    0 0 0 7900 7000   130000 58000 0 320 220   4100 7300
        correct-unconfirmed false 0
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (38 tasks, max score: 76) 23
Run set sv-comp17.Systems_BusyBox_Overflows