Tool ULTIMATE Automizer 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:34:03 CET [[ 2017-01-15 06:02:28 CET ]] [[ 2017-01-15 06:17:25 CET ]] [[ 2017-01-15 06:02:42 CET ]] [[ 2017-01-15 06:18:28 CET ]]
Run set sv-comp17.Systems_BusyBox_Overflows
Options [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/uautomizer.2017-01-14_0734.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/uautomizer.2017-01-14_0734.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/uautomizer.2017-01-14_0734.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/uautomizer.2017-01-14_0734.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   740   12000 5500 2.3 0   .55 .35 11   46 6.2 3.3 120 300
basename_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 900   750   12000 5500 2.3 0   .56 .38 11   42 7.0 3.6 150 320
chgrp-incomplete_true-no-overflow_false-valid-memtrack.i 0 6.2 1.7 51 330 2.5 0   .53 .34 8.2 40 6.5 3.4 140 300
chroot-incomplete_true-no-overflow_true-valid-memsafety.i 0 5.4 1.7 40 310 2.5 0   .52 .33 7.9 39 6.7 3.5 140 300
cut_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 5.5 1.7 42 310 2.5 0   .57 .36 12   44 7.9 4.1 150 320
date_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 5.8 1.8 46 310 2.5 0   .49 .31 5.4 40 7.0 3.7 140 290
dirname_true-no-overflow_true-valid-memsafety.i 0 160   120   1500 1100 2.5 0   .53 .35 9.0 39 6.7 3.5 120 300
du_true-no-overflow_true-valid-memsafety.i 0 6.2 1.8 46 330 2.5 0   .50 .34 5.2 41 6.7 3.6 140 310
echo_true-no-overflow_true-valid-memsafety.i 0 5.4 1.7 42 310 2.5 0   .53 .34 9.7 40 6.8 3.6 130 310
expand_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 5.8 1.7 47 320 2.5 0   .54 .35 11   40 6.9 3.6 140 290
fold_true-no-overflow_true-valid-memsafety.i 0 5.6 1.7 43 320 2.5 0   .52 .34 12   41 6.6 3.5 130 300
head_true-no-overflow_false-valid-deref.i 0 5.3 1.7 41 310 2.5 0   .53 .34 8.3 40 6.9 3.7 140 310
hostid_true-no-overflow_true-valid-memsafety.i 2 10   2.9 70 380 2.6 0   10    5.3  110   400 13   7.0 180 410
logname_true-no-overflow_true-valid-memsafety.i 0 6.4 1.7 50 330 2.5 0   .48 .32 9.3 40 6.4 3.4 140 300
ls-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 6.1 1.7 53 320 2.5 0   .56 .36 9.1 44 6.6 3.5 120 300
mkdir_true-no-overflow_true-valid-memsafety.i 0 6.0 1.8 42 310 2.5 0   .51 .33 12   41 6.4 3.4 120 300
mkfifo-incomplete_true-no-overflow_true-valid-memsafety.i 0 6.0 1.7 39 320 2.5 0   .48 .32 9.7 41 6.6 3.5 140 300
od_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 7.5 2.0 48 340 2.5 0   .50 .33 12   40 6.7 3.5 120 310
printf_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 6.2 1.7 46 340 2.5 0   .50 .34 8.7 40 6.7 3.5 140 310
readlink_true-no-overflow_true-valid-memsafety.i 0 6.4 1.7 54 330 2.5 0   .50 .32 9.8 41 7.0 3.7 140 310
realpath_true-no-overflow_true-valid-memsafety.i 0 5.5 1.7 42 310 2.5 0   .48 .30 7.0 40 6.2 3.3 120 300
rm_true-no-overflow_true-valid-memsafety.i 0 5.5 1.8 40 310 2.5 0   .50 .31 9.4 40 7.4 3.9 150 320
seq_true-no-overflow_true-valid-memsafety.i 0 6.0 1.8 40 310 2.5 0   .50 .34 4.9 40 6.9 3.6 140 300
sleep_true-no-overflow_false-valid-deref.i 0 6.1 1.7 52 330 2.5 0   .57 .36 10   43 6.7 3.5 140 300
stty_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 6.2 1.8 52 320 2.5 0   .51 .32 9.9 41 6.3 3.4 130 300
sync_true-no-overflow_true-valid-memsafety.i 0 5.6 1.7 45 310 2.5 0   .51 .33 9.6 40 6.6 3.5 130 300
tac_true-no-overflow_true-valid-memsafety.i 0 5.6 1.7 44 320 2.5 0   .49 .33 5.8 41 6.7 3.5 140 290
tee_true-no-overflow_true-valid-memsafety.i 0 6.4 1.8 48 330 2.5 0   .52 .33 9.0 42 6.5 3.4 110 320
test-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 5.5 1.7 43 300 2.6 0   .55 .34 11   42 6.7 3.6 130 300
touch_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 5.7 1.7 46 310 2.5 0   .58 .37 9.5 40 7.7 4.0 150 310
uname_true-no-overflow_true-valid-memsafety.i 0 5.9 1.8 49 310 2.7 0   .52 .35 12   41 6.5 3.4 130 300
uniq_true-no-overflow_true-valid-memsafety.i 0 6.2 1.8 46 330 2.5 0   .49 .31 8.8 39 6.3 3.3 130 300
usleep_true-no-overflow_true-valid-memsafety.i 0 6.1 1.7 45 350 2.5 0   .50 .34 14   41 6.8 3.6 130 300
uudecode_true-no-overflow_true-valid-memsafety.i 0 5.6 1.8 45 310 2.5 0   .52 .36 10   39 6.1 3.3 38 290
wc_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 5.4 1.7 43 310 2.5 0   .51 .33 11   42 6.2 3.3 110 290
who_true-no-overflow_true-valid-memsafety.i 0 6.7 1.7 49 350 2.5 0   .52 .34 8.3 40 6.4 3.4 130 300
whoami-incomplete_true-no-overflow_true-valid-memsafety.i 0 6.1 1.7 44 330 2.5 0   .49 .32 7.3 42 6.4 3.4 120 300
yes_true-no-overflow_true-valid-memsafety.i 0 5.1 1.6 37 310 2.5 0   .52 .33 8.4 41 6.3 3.3 140 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 1700   27000 23000 96   0   38 38 38 29 18   450 1900 38 260 140   5000 12000
    correct results 1 2 10 2.9 70 380 2.6 0   0 0 0 10 5.3 110 400 1 13 7.0 180 410
        correct true 1 2 10 2.9 70 380 2.6 0   0 0 0 10 5.3 110 400 1 13 7.0 180 410
        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