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 07:32:15 CET [[ 2017-01-15 06:03:36 CET ]] [[ 2017-01-15 06:19:08 CET ]] [[ 2017-01-15 06:04:26 CET ]] [[ 2017-01-15 06:20:07 CET ]]
Run set sv-comp17.Systems_BusyBox_Overflows
Options [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ukojak.2017-01-14_0732.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ukojak.2017-01-14_0732.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_0732.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ukojak.2017-01-14_0732.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 0 900   770   12000 4600 2.3 0   .63 .40 8.9 40 6.3 3.3 140 300
basename_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 900   770   15000 5100 2.3 0   .52 .35 11   42 6.9 3.6 130 310
chgrp-incomplete_true-no-overflow_false-valid-memtrack.i 0 5.9 1.7 45 330 2.5 0   .54 .35 12   40 6.8 3.6 140 300
chroot-incomplete_true-no-overflow_true-valid-memsafety.i 0 5.3 1.6 46 310 2.9 0   .51 .33 4.7 40 7.3 3.8 140 300
cut_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 5.6 1.6 48 310 2.5 0   .53 .35 9.5 40 6.9 3.7 130 300
date_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 6.2 1.8 48 330 2.5 0   .48 .31 9.8 40 6.9 3.6 130 300
dirname_true-no-overflow_true-valid-memsafety.i 0 190   160   2100 11000 2.5 0   .56 .37 13   42 6.4 3.4 130 310
du_true-no-overflow_true-valid-memsafety.i 0 5.7 1.7 46 320 2.6 0   .51 .32 12   40 6.3 3.4 120 290
echo_true-no-overflow_true-valid-memsafety.i 0 5.2 1.6 36 310 2.5 0   .49 .32 11   40 6.7 3.6 130 300
expand_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 5.4 1.7 47 310 2.5 0   .52 .33 9.1 40 6.5 3.5 130 300
fold_true-no-overflow_true-valid-memsafety.i 0 5.9 1.8 43 320 2.5 0   .54 .36 13   40 6.0 3.2 98 310
head_true-no-overflow_false-valid-deref.i 0 6.3 1.7 49 340 2.5 0   .56 .34 13   42 6.2 3.3 130 290
hostid_true-no-overflow_true-valid-memsafety.i 2 15   4.5 110 500 2.6 0   10    5.3  150   410 15   7.8 220 420
logname_true-no-overflow_true-valid-memsafety.i 0 5.4 1.7 42 310 2.5 0   .50 .32 11   39 6.7 3.5 130 300
ls-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 6.0 1.8 45 320 2.5 0   .47 .32 9.9 40 6.6 3.5 140 300
mkdir_true-no-overflow_true-valid-memsafety.i 0 6.0 1.7 42 310 2.5 0   .54 .35 12   40 6.5 3.4 130 300
mkfifo-incomplete_true-no-overflow_true-valid-memsafety.i 0 5.3 1.6 41 300 2.5 0   .55 .36 11   42 6.6 3.5 130 300
od_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 6.3 1.9 50 310 2.5 0   .52 .35 12   39 6.8 3.6 130 310
printf_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 6.5 1.8 53 330 2.5 0   .52 .34 12   39 6.8 3.6 140 300
readlink_true-no-overflow_true-valid-memsafety.i 0 5.8 1.7 46 310 2.5 0   .55 .35 12   40 6.9 3.6 140 300
realpath_true-no-overflow_true-valid-memsafety.i 0 6.3 1.7 44 320 2.5 0   .53 .35 13   39 6.7 3.6 130 300
rm_true-no-overflow_true-valid-memsafety.i 0 5.7 1.7 40 320 2.9 0   .52 .34 7.2 40 6.5 3.4 130 300
seq_true-no-overflow_true-valid-memsafety.i 0 5.6 1.7 43 320 2.5 0   .58 .37 14   43 6.6 3.5 120 310
sleep_true-no-overflow_false-valid-deref.i 0 6.3 1.7 46 330 2.5 0   .54 .36 11   42 6.2 3.3 90 300
stty_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 6.2 1.7 50 330 2.5 0   .65 .41 9.0 40 6.7 3.5 140 300
sync_true-no-overflow_true-valid-memsafety.i 0 6.2 1.8 46 330 2.5 0   .54 .35 11   43 6.2 3.3 120 300
tac_true-no-overflow_true-valid-memsafety.i 0 5.6 1.7 47 310 2.5 0   .50 .33 11   39 6.9 3.7 140 300
tee_true-no-overflow_true-valid-memsafety.i 0 5.8 1.7 42 310 2.5 0   .49 .31 8.7 40 6.6 3.5 120 300
test-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 5.6 1.7 44 310 2.5 0   .49 .32 11   41 6.7 3.5 130 300
touch_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 6.3 1.9 46 340 2.5 0   .52 .33 7.8 40 7.1 3.7 140 300
uname_true-no-overflow_true-valid-memsafety.i 0 5.7 1.8 51 310 2.5 0   .52 .34 13   40 6.9 3.6 140 310
uniq_true-no-overflow_true-valid-memsafety.i 0 5.6 1.7 48 320 2.5 0   .49 .32 12   40 6.5 3.4 130 300
usleep_true-no-overflow_true-valid-memsafety.i 0 5.4 1.6 36 310 2.5 0   .51 .31 12   39 6.5 3.5 120 310
uudecode_true-no-overflow_true-valid-memsafety.i 0 5.7 1.7 49 310 2.5 0   .53 .33 11   40 6.6 3.5 120 310
wc_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 6.0 1.7 51 320 2.5 0   .52 .34 13   40 7.0 3.7 140 300
who_true-no-overflow_true-valid-memsafety.i 0 5.5 1.7 43 320 2.5 0   .51 .32 13   40 6.7 3.5 130 310
whoami-incomplete_true-no-overflow_true-valid-memsafety.i 0 5.8 1.7 47 320 2.5 0   .54 .35 11   44 6.6 3.5 130 300
yes_true-no-overflow_true-valid-memsafety.i 0 5.3 1.6 43 310 2.5 0   .52 .34 13   40 6.4 3.4 130 290
../../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 2 2200 1800   31000 32000 96   0   38 38 38 30 18   560 1900 38 260 140   5000 12000
    correct results 1 2 15 4.5 110 500 2.6 0   0 0 0 10 5.3 150 410 1 15 7.8 220 420
        correct true 1 2 15 4.5 110 500 2.6 0   0 0 0 10 5.3 150 410 1 15 7.8 220 420
        correct false 0
    correct-unconfimed results 0
        correct-unconfirmed true 0
        correct-unconfirmed false 0
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (38 tasks, max score: 76) 2
Run set sv-comp17.Systems_BusyBox_Overflows