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:52:13 CET [[ 2017-01-15 06:05:33 CET ]] [[ 2017-01-15 06:20:29 CET ]] [[ 2017-01-15 06:05:48 CET ]] [[ 2017-01-15 06:21:18 CET ]]
Run set sv-comp17.Systems_BusyBox_Overflows
Options [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/utaipan.2017-01-14_1652.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/utaipan.2017-01-14_1652.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_1652.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/utaipan.2017-01-14_1652.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   860   9500 2400 2.3 0   .51 .32 10 40 6.3 3.4 140 300
basename_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 900   860   9500 2400 2.3 0   .51 .32 11 40 5.8 3.1 130 290
chgrp-incomplete_true-no-overflow_false-valid-memtrack.i 0 6.1 1.8 48 320 2.5 0   .51 .34 13 40 6.5 3.4 120 310
chroot-incomplete_true-no-overflow_true-valid-memsafety.i 0 5.8 1.7 42 320 2.5 0   .53 .32 12 40 6.4 3.4 130 300
cut_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 6.5 1.8 49 340 2.5 0   .53 .36 10 40 6.5 3.4 130 300
date_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 6.2 1.7 44 330 2.5 0   .53 .35 12 40 7.4 3.9 150 320
dirname_true-no-overflow_true-valid-memsafety.i 0 400   360   3000 1100 2.5 0   .50 .33 11 39 6.6 3.5 130 310
du_true-no-overflow_true-valid-memsafety.i 0 5.8 1.8 49 310 2.5 0   .51 .34 11 39 7.2 3.8 120 300
echo_true-no-overflow_true-valid-memsafety.i 0 5.8 1.7 42 310 2.5 0   .51 .33 10 41 6.3 3.4 120 300
expand_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 5.7 1.7 47 310 2.5 0   .54 .35 11 39 7.2 3.8 130 310
fold_true-no-overflow_true-valid-memsafety.i 0 5.8 1.8 49 310 2.5 0   .49 .31 11 40 6.6 3.5 140 290
head_true-no-overflow_false-valid-deref.i 0 5.7 1.7 47 320 2.5 0   .52 .35 12 39 6.3 3.3 130 300
hostid_true-no-overflow_true-valid-memsafety.i 2 10   2.8 74 380 2.6 0   9.5  5.1  110 400 14   7.2 200 390
logname_true-no-overflow_true-valid-memsafety.i 0 5.8 1.7 43 320 2.5 0   .51 .31 11 40 6.0 3.2 130 290
ls-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 5.8 1.7 48 310 2.5 0   .59 .38 13 45 6.9 3.7 140 300
mkdir_true-no-overflow_true-valid-memsafety.i 0 5.7 1.7 43 310 2.5 0   .56 .37 12 41 6.6 3.5 130 290
mkfifo-incomplete_true-no-overflow_true-valid-memsafety.i 0 6.2 1.7 42 340 2.5 0   .58 .37 14 42 6.4 3.4 130 300
od_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 6.2 1.8 44 320 2.5 0   .54 .35 11 40 6.2 3.4 130 300
printf_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 6.9 1.9 51 320 2.5 0   .57 .38 14 44 6.6 3.5 120 310
readlink_true-no-overflow_true-valid-memsafety.i 0 5.6 1.7 45 310 2.5 0   .54 .35 12 40 7.3 3.8 140 310
realpath_true-no-overflow_true-valid-memsafety.i 0 5.4 1.6 42 310 2.5 0   .54 .35 13 39 6.5 3.4 120 290
rm_true-no-overflow_true-valid-memsafety.i 0 5.6 1.7 43 310 2.5 0   .53 .33 12 42 6.9 3.6 140 300
seq_true-no-overflow_true-valid-memsafety.i 0 6.0 1.7 41 320 2.5 0   .53 .33 12 39 6.2 3.3 120 300
sleep_true-no-overflow_false-valid-deref.i 0 5.9 1.8 41 320 2.5 0   .49 .33 11 40 6.5 3.4 130 300
stty_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 6.4 1.9 50 320 2.5 0   .51 .33 12 39 6.9 3.7 130 300
sync_true-no-overflow_true-valid-memsafety.i 0 5.6 1.7 40 320 2.5 0   .53 .35 10 41 6.1 3.2 120 310
tac_true-no-overflow_true-valid-memsafety.i 0 6.5 1.7 42 350 2.5 0   .52 .34 12 40 6.5 3.5 130 300
tee_true-no-overflow_true-valid-memsafety.i 0 5.5 1.7 47 300 2.5 0   .56 .38 12 43 6.4 3.4 130 300
test-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 5.6 1.7 43 310 2.5 0   .55 .35 11 40 6.6 3.5 140 300
touch_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 6.3 1.8 47 320 2.5 0   .56 .38 11 39 6.6 3.5 120 290
uname_true-no-overflow_true-valid-memsafety.i 0 6.6 1.8 50 330 2.5 0   .49 .32 11 39 6.6 3.5 130 290
uniq_true-no-overflow_true-valid-memsafety.i 0 5.9 1.7 48 320 2.5 0   .48 .32 10 39 6.7 3.5 120 300
usleep_true-no-overflow_true-valid-memsafety.i 0 5.2 1.6 41 300 2.5 0   .50 .32 11 40 6.6 3.5 120 300
uudecode_true-no-overflow_true-valid-memsafety.i 0 5.7 1.8 48 310 2.5 0   .51 .34 11 40 6.5 3.5 120 300
wc_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 5.8 1.8 45 300 2.5 0   .53 .34 12 42 6.7 3.6 130 300
who_true-no-overflow_true-valid-memsafety.i 0 5.8 1.8 44 310 2.5 0   .53 .34 12 40 6.8 3.6 120 300
whoami-incomplete_true-no-overflow_true-valid-memsafety.i 0 5.7 1.6 43 320 2.5 0   .52 .35 11 42 6.6 3.5 130 310
yes_true-no-overflow_true-valid-memsafety.i 0 5.7 1.6 43 330 2.5 0   .53 .36 12 42 6.9 3.6 120 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 2 2400 2100   24000 17000 95   0   38 38 38 29   18   540 1900 38 260 140   5000 12000
    correct results 1 2 10 2.8 74 380 2.6 0   0 0 0 9.5 5.1 110 400 1 14 7.2 200 390
        correct true 1 2 10 2.8 74 380 2.6 0   0 0 0 9.5 5.1 110 400 1 14 7.2 200 390
        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