Tool CBMC 5.6
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-11 10:20:18 CET [[ 2017-01-14 21:14:41 CET ]] [[ 2017-01-14 21:35:33 CET ]] [[ 2017-01-14 21:19:46 CET ]] [[ 2017-01-14 21:37:38 CET ]]
Run set sv-comp17.Systems_BusyBox_MemSafety
Options --graphml-witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cbmc.2017-01-11_1020.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cbmc.2017-01-11_1020.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cbmc.2017-01-11_1020.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cbmc.2017-01-11_1020.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 false(valid-deref) 1 wit inspect 9.1  9.2  110   690 .75  .033 error 8.5  4.5  93   320 out of memory 80   48   1200 7000 - -
head_true-no-overflow_false-valid-deref.i error (1) 0 wit inspect 3.4  3.4  41   65 .016 .14  error (invalid witness file) .50 .33 12   39 error (invalid witness file) 7.9 4.1 150 340 - -
sleep_true-no-overflow_false-valid-deref.i error (1) 0 wit inspect 1.0  1.0  11   36 .012 .32  error (invalid witness file) .56 .36 6.0 44 error (invalid witness file) 6.2 3.3 130 310 - -
chgrp-incomplete_true-no-overflow_false-valid-memtrack.i error (1) 0 wit inspect .38 .38 4.4 29 .012 0     error (invalid witness file) .70 .43 9.2 44 error (invalid witness file) 7.2 3.8 110 290 - -
basename_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (42) 0 wit inspect 850    850    6200   5300 16     .10  - - error (invalid witness file) .51 .33 10   39 error (invalid witness file) 6.8 3.6 79 300
chroot-incomplete_true-no-overflow_true-valid-memsafety.i error (1) 0 wit inspect .58 .58 5.2 30 .020 0     - - error (invalid witness file) .46 .30 7.8 40 error (invalid witness file) 7.2 3.8 140 310
cut_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (1) 0 wit inspect 6.2  6.2  84   110 .020 .14  - - error (invalid witness file) .51 .34 8.8 41 error (invalid witness file) 7.8 4.1 96 300
date_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (1) 0 wit inspect 2.8  2.8  34   210 .020 .020 - - error (invalid witness file) .48 .31 9.3 39 error (invalid witness file) 7.0 3.7 100 300
dirname_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect 350    350    4800   14000 4.0   .48  - - error (invalid witness file) .49 .32 9.7 40 error (invalid witness file) 7.2 3.8 120 310
du_true-no-overflow_true-valid-memsafety.i error (1) 0 wit inspect 20    20    260   150 .016 .43  - - error (invalid witness file) .62 .40 6.2 40 error (invalid witness file) 6.9 3.6 160 310
echo_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect 53    53    650   13000 .045 .51  - - error (invalid witness file) .54 .34 10   39 error (invalid witness file) 6.3 3.4 110 300
expand_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (1) 0 wit inspect 22    22    240   140 .020 .69  - - error (invalid witness file) .46 .30 5.9 39 error (invalid witness file) 6.9 3.6 130 300
fold_true-no-overflow_true-valid-memsafety.i error (1) 0 wit inspect 4.2  4.2  54   66 .020 .46  - - error (invalid witness file) .54 .34 8.4 40 error (invalid witness file) 7.5 4.0 86 300
hostid_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect 340    340    3800   14000 3.7   .074 - - error (invalid witness file) .52 .34 7.0 42 error (invalid witness file) 7.0 3.7 88 300
logname_true-no-overflow_true-valid-memsafety.i error (1) 0 wit inspect .32 .32 3.1 29 .012 .19  - - error (invalid witness file) .53 .35 7.3 40 error (invalid witness file) 6.5 3.4 120 300
ls-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (1) 0 wit inspect 25    25    260   180 .037 13     - - error (invalid witness file) .63 .40 7.7 39 error (invalid witness file) 7.7 4.1 91 300
mkdir_true-no-overflow_true-valid-memsafety.i error (1) 0 wit inspect 2.4  2.4  32   190 .016 .016 - - error (invalid witness file) .52 .33 6.5 40 error (invalid witness file) 6.3 3.3 110 300
mkfifo-incomplete_true-no-overflow_true-valid-memsafety.i error (1) 0 wit inspect .41 .40 3.6 30 .012 0     - - error (invalid witness file) .64 .40 8.9 40 error (invalid witness file) 7.0 3.7 93 300
od_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (1) 0 wit inspect 16    16    230   140 .020 .50  - - error (invalid witness file) .51 .32 9.6 39 error (invalid witness file) 7.3 3.8 130 310
printf_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (1) 0 wit inspect 20    20    230   130 .025 .43  - - error (invalid witness file) .63 .41 9.0 42 error (invalid witness file) 6.9 3.7 130 310
readlink_true-no-overflow_true-valid-memsafety.i error (1) 0 wit inspect .89 .89 11   43 .016 .32  - - error (invalid witness file) .50 .35 4.9 40 error (invalid witness file) 6.6 3.5 110 300
realpath_true-no-overflow_true-valid-memsafety.i error (1) 0 wit inspect .41 .41 3.8 31 .012 .13  - - error (invalid witness file) .51 .34 10   40 error (invalid witness file) 8.7 4.5 120 330
rm_true-no-overflow_true-valid-memsafety.i error (1) 0 wit inspect 33    33    370   150 .025 0     - - error (invalid witness file) .51 .34 10   41 error (invalid witness file) 5.7 3.0 130 290
seq_true-no-overflow_true-valid-memsafety.i error (1) 0 wit inspect .84 .84 9.2 53 .016 0     - - error (invalid witness file) .56 .34 12   42 error (invalid witness file) 6.6 3.5 120 300
stty_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (1) 0 wit inspect 40    40    460   180 .033 .63  - - error (invalid witness file) .57 .37 11   43 error (invalid witness file) 7.8 4.1 96 290
sync_true-no-overflow_true-valid-memsafety.i error (1) 0 wit inspect .30 .30 2.9 27 .012 0     - - error (invalid witness file) .51 .33 10   39 error (invalid witness file) 7.4 3.9 95 300
tac_true-no-overflow_true-valid-memsafety.i error (1) 0 wit inspect 2.6  2.6  32   62 .016 0     - - error (invalid witness file) .49 .32 10   40 error (invalid witness file) 6.8 3.6 140 310
tee_true-no-overflow_true-valid-memsafety.i error (1) 0 wit inspect 1.2  1.2  14   51 .016 0     - - error (invalid witness file) .53 .34 12   40 error (invalid witness file) 8.6 4.5 95 320
test-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (1) 0 wit inspect 18    18    250   150 .016 .15  - - error (invalid witness file) .49 .32 10   40 error (invalid witness file) 7.2 3.8 96 300
touch_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (1) 0 wit inspect 2.7  2.7  37   190 .020 .037 - - error (invalid witness file) .66 .42 8.6 42 error (invalid witness file) 6.2 3.3 140 300
uname_true-no-overflow_true-valid-memsafety.i error (1) 0 wit inspect 1.2  1.2  14   190 .016 0     - - error (invalid witness file) .48 .31 8.9 39 error (invalid witness file) 6.4 3.4 120 300
uniq_true-no-overflow_true-valid-memsafety.i error (1) 0 wit inspect 2.0  2.0  24   54 .016 .13  - - error (invalid witness file) .54 .35 9.8 41 error (invalid witness file) 8.2 4.3 110 310
usleep_true-no-overflow_true-valid-memsafety.i error (1) 0 wit inspect .35 .34 3.2 29 .012 .13  - - error (invalid witness file) .49 .32 9.7 41 error (invalid witness file) 7.2 3.8 86 300
uudecode_true-no-overflow_true-valid-memsafety.i error (1) 0 wit inspect 5.8  5.8  76   110 .020 .15  - - error (invalid witness file) .61 .39 8.1 40 error (invalid witness file) 8.2 4.4 84 310
wc_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (1) 0 wit inspect 2.6  2.6  31   65 .016 .49  - - error (invalid witness file) .57 .36 5.7 40 error (invalid witness file) 6.6 3.4 130 310
who_true-no-overflow_true-valid-memsafety.i error (1) 0 wit inspect .86 .86 9.4 41 .016 0     - - error (invalid witness file) .49 .32 7.5 42 error (invalid witness file) 7.2 3.8 110 310
whoami-incomplete_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect 340    340    3900   14000 3.9   .36  - - error (invalid witness file) .53 .34 12   39 error (invalid witness file) 6.0 3.2 120 310
yes_true-no-overflow_true-valid-memsafety.i error (1) 0 wit inspect .38 .39 3.0 33 .012 2.6   - - error (invalid witness file) .52 .33 11   41 error (invalid witness file) 6.8 3.6 84 310
../../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 1 2200   2200   22000 63000 29    23     38 10   5.6 120 450 38 100 60 1500 7900 38 18 12 300 1400   38 240 130 3800 10000  
    correct results 1 1 9.1 9.2 110 690 .75 .033 0 8.5 4.5 93 320 0 80 48 1200 7000 0 0 0 0 0   0 0 0 0 0  
        correct true 0
        correct false 1 1 9.1 9.2 110 690 .75 .033 0 8.5 4.5 93 320 0 80 48 1200 7000 0 0 0 0 0   0 0 0 0 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: 72) 1
Run set sv-comp17.Systems_BusyBox_MemSafety