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 05:56:27 CET [[ 2017-01-15 04:08:20 CET ]] [[ 2017-01-15 04:18:47 CET ]] [[ 2017-01-15 04:12:29 CET ]] [[ 2017-01-15 04:25:58 CET ]]
Run set sv-comp17.Systems_BusyBox_MemSafety
Options -w error-witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/smack.2017-01-14_0556.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/smack.2017-01-14_0556.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_0556.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/smack.2017-01-14_0556.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 (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)
basename_false-unreach-call_true-no-overflow_false-valid-deref.i timeout 0 wit inspect 880   930   11000 290   3.0 0     error (invalid witness file) .48 .31 4.1 39 error (invalid witness file) 6.5 3.4 110 290 - -
head_true-no-overflow_false-valid-deref.i timeout 0 wit inspect 900   900   12000 7.5 0   0     error (invalid witness file) .49 .32 7.9 39 error (invalid witness file) 6.5 3.5 120 300 - -
sleep_true-no-overflow_false-valid-deref.i false(valid-deref) 1 wit inspect 7.7 7.5 98 130   2.3 0     error (invalid witness file) .46 .30 3.8 39 error (invalid witness file) 7.8 4.1 150 320 - -
chgrp-incomplete_true-no-overflow_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 840   830   8400 400   3.1 0     error (invalid witness file) .48 .32 6.9 39 error (invalid witness file) 6.0 3.2 94 280 - -
basename_false-unreach-call_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 880   930   12000 230   3.0 0     - - error (invalid witness file) .51 .33 3.9 40 error (invalid witness file) 6.8 3.6 110 300
chroot-incomplete_true-no-overflow_true-valid-memsafety.i false(valid-deref) -16 wit inspect 530   530   6400 310   2.2 0     - - error (invalid witness file) .51 .33 13   40 error (invalid witness file) 6.8 3.6 120 300
cut_false-unreach-call_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   900   12000 7.5 0   0     - - error (invalid witness file) .53 .35 12   43 error (invalid witness file) 6.9 3.6 150 310
date_false-unreach-call_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   900   11000 9.4 0   0     - - error (invalid witness file) .51 .34 6.1 39 error (invalid witness file) 7.1 3.7 130 300
dirname_true-no-overflow_true-valid-memsafety.i true 2 wit inspect 880   880   7500 330   2.5 0     - - error (invalid witness file) .51 .33 9.2 40 error (invalid witness file) 6.2 3.3 130 310
du_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 880   930   11000 3400   14   0     - - error (invalid witness file) .49 .32 9.2 40 error (invalid witness file) 6.4 3.4 130 300
echo_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 880   930   8700 480   3.9 0     - - error (invalid witness file) .54 .35 13   41 error (invalid witness file) 6.7 3.5 140 300
expand_false-unreach-call_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   900   10000 7.7 0   0     - - error (invalid witness file) .53 .35 13   41 error (invalid witness file) 6.6 3.5 120 290
fold_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   900   11000 7.5 0   0     - - error (invalid witness file) .48 .31 5.1 40 error (invalid witness file) 6.4 3.4 120 300
hostid_true-no-overflow_true-valid-memsafety.i true 2 wit inspect 880   880   7600 320   2.3 0     - - error (invalid witness file) .53 .35 12   40 error (invalid witness file) 6.3 3.3 130 290
logname_true-no-overflow_true-valid-memsafety.i true 2 wit inspect 880   880   8600 330   3.0 0     - - error (invalid witness file) .50 .33 5.8 39 error (invalid witness file) 6.3 3.4 120 300
ls-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 880   930   11000 3600   24   0     - - error (invalid witness file) .49 .32 7.7 39 error (invalid witness file) 7.5 3.9 140 310
mkdir_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   900   13000 7.4 0   0     - - error (invalid witness file) .50 .32 9.8 41 error (invalid witness file) 6.4 3.4 120 300
mkfifo-incomplete_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 880   930   11000 300   3.1 0     - - error (invalid witness file) .52 .34 9.4 40 error (invalid witness file) 6.6 3.5 120 300
od_false-unreach-call_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   900   12000 7.6 0   0     - - error (invalid witness file) .52 .34 14   42 error (invalid witness file) 7.0 3.8 150 310
printf_false-unreach-call_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 880   930   7300 550   7.3 0     - - error (invalid witness file) .49 .32 7.6 40 error (invalid witness file) 6.4 3.4 130 310
readlink_true-no-overflow_true-valid-memsafety.i true 2 wit inspect 880   880   7900 730   6.1 0     - - error (invalid witness file) .51 .34 4.9 40 error (invalid witness file) 6.8 3.6 120 300
realpath_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 880   930   12000 320   3.1 0     - - error (invalid witness file) .52 .33 12   39 error (invalid witness file) 6.7 3.5 120 320
rm_true-no-overflow_true-valid-memsafety.i true 2 wit inspect 880   880   7600 740   7.0 0     - - error (invalid witness file) .51 .33 9.7 40 error (invalid witness file) 7.7 4.0 150 320
seq_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   900   12000 7.4 0   0     - - error (invalid witness file) .49 .33 7.8 39 error (invalid witness file) 6.0 3.2 99 300
stty_false-unreach-call_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 890   930   7200 540   21   0     - - error (invalid witness file) .54 .34 12   42 error (invalid witness file) 6.5 3.5 130 300
sync_true-no-overflow_true-valid-memsafety.i true 2 wit inspect 880   880   11000 340   3.0 0     - - error (invalid witness file) .49 .31 6.6 39 error (invalid witness file) 6.0 3.2 110 290
tac_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 880   930   8900 570   6.3 0     - - error (invalid witness file) .54 .36 9.8 40 error (invalid witness file) 6.9 3.6 130 300
tee_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 880   930   11000 3300   13   0     - - error (invalid witness file) .53 .34 9.8 40 error (invalid witness file) 6.3 3.4 120 290
test-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 880   930   11000 440   6.4 0     - - error (invalid witness file) .56 .37 4.9 44 error (invalid witness file) 7.5 3.9 150 320
touch_false-unreach-call_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   900   12000 7.4 0   0     - - error (invalid witness file) .59 .38 13   42 error (invalid witness file) 6.9 3.6 140 310
uname_true-no-overflow_true-valid-memsafety.i true 2 wit inspect 880   880   9000 730   6.0 0     - - error (invalid witness file) .59 .38 10   39 error (invalid witness file) 6.6 3.5 120 300
uniq_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   900   13000 7.4 0   0     - - error (invalid witness file) .50 .33 11   40 error (invalid witness file) 9.5 4.9 110 310
usleep_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 880   930   10000 390   3.4 0     - - error (invalid witness file) .48 .32 4.0 40 error (invalid witness file) 7.0 3.7 130 310
uudecode_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   900   13000 7.4 0   0     - - error (invalid witness file) .50 .33 7.5 41 error (invalid witness file) 6.5 3.5 140 290
wc_false-unreach-call_true-no-overflow_true-valid-memsafety.i true 2 wit inspect 880   880   8400 800   6.9 0     - - error (invalid witness file) .53 .35 4.7 40 error (invalid witness file) 7.6 4.0 110 320
who_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 880   930   6400 630   6.7 0     - - error (invalid witness file) .49 .32 11   39 error (invalid witness file) 6.3 3.3 98 290
whoami-incomplete_true-no-overflow_true-valid-memsafety.i true 2 wit inspect 880   880   8000 360   3.1 0     - - error (invalid witness file) .49 .33 6.3 40 error (invalid witness file) 6.3 3.3 100 290
yes_true-no-overflow_true-valid-memsafety.i true 2 wit inspect 830   830   8000 370   3.1 .098 - - error (invalid witness file) .47 .30 6.3 40 error (invalid witness file) 6.6 3.5 140 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 (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 38 6 32000 33000 370000 21000 170   .098 38 1.9  1.2  23 160   38 27 14   470 1200   38 18    11    300 1400   38 230   120   4300 10000  
    correct results 12 22 9600 9600 92000 5600 48   .098 0 .94 .62 11 79   0 14 7.3 240 600   0 5.1  3.3  76 400   0 66   35   1200 3000  
        correct true 10 20 8800 8800 83000 5000 43   .098 0 0    0    0 0   0 0 0   0 0   0 5.1  3.3  76 400   0 66   35   1200 3000  
        correct false 2 2 840 840 8500 530 5.4 0     0 .94 .62 11 79   0 14 7.3 240 600   0 0    0    0 0   0 0   0   0 0  
    correct-unconfimed results 0
        correct-unconfirmed true 0
        correct-unconfirmed false 0
    incorrect results 1 -16 530 530 6400 310 2.2 0     0 0    0    0 0   0 0 0   0 0   0 .51 .33 13 40   0 6.8 3.6 120 300  
        incorrect true 0
        incorrect false 1 -16 530 530 6400 310 2.2 0     0 0    0    0 0   0 0 0   0 0   0 .51 .33 13 40   0 6.8 3.6 120 300  
score (38 tasks, max score: 72) 6
Run set sv-comp17.Systems_BusyBox_MemSafety