Tool CBMC 5.8 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741 CProver witness2test 0.1 ULTIMATE Automizer 0.1.23-3204b741
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon* [apollon058; apollon077; apollon078; apollon114] [apollon077; apollon078; apollon135; apollon137; apollon144] apollon* [apollon039; apollon060; apollon077; apollon078]
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [4; 8], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33554 MB; 33553 MB] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-12-01 11:16:27 CET 2017-12-01 12:31:21 CET 2017-12-01 12:51:49 CET 2017-12-01 12:54:09 CET 2017-12-01 12:35:01 CET
Run set cbmc.sv-comp18.Systems_BusyBox_NoOverflows cpa-seq-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.Systems_BusyBox_NoOverflows uautomizer-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.Systems_BusyBox_NoOverflows fshell-witness2test-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.Systems_BusyBox_NoOverflows uautomizer-validate-correctness-witnesses-cbmc.sv-comp18-correctness-witness.Systems_BusyBox_NoOverflows
Options --graphml-witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cbmc.2017-12-01_1116.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const --full-output --validate ../../results-verified/cbmc.2017-12-01_1116.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/cbmc.2017-12-01_1116.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cbmc.2017-12-01_1116.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/busybox-1.22.0/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
chgrp-incomplete_false-no-overflow.i 0 .76 44 7.3 0 .54 43 0 .020 4.9 0 .0015 .30 -
chroot-incomplete_false-no-overflow.i 0 1.0  44 9.8 0 .55 43 0 .018 4.9 0 .0016 .26 -
cut_false-no-overflow.i 0 7.2  93 93   0 .52 41 0 .018 4.9 0 .0017 .27 -
date_false-no-overflow.i 0 3.5  150 39   0 .55 44 0 .046 4.9 0 .0015 .29 -
du_false-no-overflow.i 0 55    240 530   0 .54 43 0 .017 4.8 0 .0016 .26 -
echo_false-no-overflow.i 0 870    4600 4300   0 .54 43 0 .044 4.9 0 .0015 .29 -
expand_false-no-overflow.i 0 30    250 320   0 .50 44 0 .024 5.0 0 .0015 .30 -
fold_false-no-overflow.i 0 3.9  58 46   0 .54 43 0 .024 4.8 0 .0017 .29 -
head_false-no-overflow.i 0 4.3  61 54   0 .53 43 0 .023 4.8 0 .0013 .26 -
logname_false-no-overflow.i 0 .67 44 6.7 0 .55 43 0 .018 4.8 0 .0037 .31 -
ls-incomplete_false-no-overflow.i 0 870    710 3400   0 .59 44 0 .021 5.0 0 .0012 .26 -
mkdir_false-no-overflow.i 0 870    2200 2500   0 .55 44 0 .018 4.8 0 .0013 .26 -
mkfifo-incomplete_false-no-overflow.i 0 .74 43 7.6 0 .53 43 0 .048 4.9 0 .0018 .26 -
od_false-no-overflow.i 0 870    890 7700   0 .65 43 0 .048 4.8 0 .0014 .26 -
printf_false-no-overflow.i 0 20    130 260   0 .52 41 0 .018 4.8 0 .0015 .29 -
readlink_false-no-overflow.i 0 1.4  49 16   0 .54 42 0 .018 4.9 0 .0016 .26 -
realpath_false-no-overflow.i 0 .78 44 7.5 0 .47 43 0 .018 4.9 0 .0017 .26 -
rm_false-no-overflow.i 0 870    400 11000   0 .56 43 0 .018 4.8 0 .0016 .26 -
seq_false-no-overflow.i 0 1.3  57 13   0 .48 44 0 .023 4.8 0 .0015 .29 -
sleep_false-no-overflow.i 0 1.5  49 15   0 .49 44 0 .022 4.9 0 .0017 .30 -
stty_false-no-overflow.i 0 53    210 670   0 .50 43 0 .018 4.9 0 .0017 .27 -
sync_false-no-overflow.i 0 .65 42 6.9 0 .51 42 0 .018 5.0 0 .0018 .26 -
tac_false-no-overflow.i 0 3.2  52 37   0 .53 43 0 .018 4.9 0 .0014 .35 -
tee_false-no-overflow.i 0 1.7  52 19   0 .50 42 0 .018 4.8 0 .0016 .26 -
test-incomplete_false-no-overflow.i 0 870    760 7100   0 .50 41 0 .027 4.9 0 .0016 .26 -
touch_false-no-overflow.i 0 3.2  140 38   0 .54 43 0 .036 4.9 0 .0013 .28 -
uname_false-no-overflow.i 0 1.6  160 18   0 .51 43 0 .018 4.8 0 .0016 .30 -
uniq_false-no-overflow.i 0 2.6  50 29   0 .55 43 0 .024 4.9 0 .0014 .29 -
usleep_false-no-overflow.i 0 .70 45 6.5 0 .52 45 0 .018 4.8 0 .0016 .26 -
uudecode_false-no-overflow.i 0 6.9  98 73   0 .56 44 0 .024 4.8 0 .0016 .26 -
wc_false-no-overflow.i 0 870    780 5000   0 .53 44 0 .022 4.8 0 .0012 .30 -
who_false-no-overflow.i 0 1.3  50 16   0 .54 43 0 .018 4.8 0 .0016 .27 -
whoami-incomplete_false-no-overflow.i - 0 .58 44 0 .018 4.8 0 .0015 .26 -
yes_false-no-overflow.i 0 .70 44 6.4 0 .49 43 0 .019 4.8 0 .0014 .26 -
basename_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 870    6800 4700   - - - 0 .028 4.8
chgrp-incomplete_true-no-overflow_false-valid-memtrack.i 0 .75 44 7.3 - - - 0 .018 5.0
chroot-incomplete_true-no-overflow_true-valid-memsafety.i 0 1.0  44 11   - - - 0 .020 4.8
cut_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 7.2  93 75   - - - 0 .021 4.9
date_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 3.5  160 40   - - - 0 .019 4.9
dirname_true-no-overflow_true-valid-memsafety.i 0 550    12000 6400   - - - 0 .034 4.9
du_true-no-overflow_true-valid-memsafety.i 0 52    240 550   - - - 0 .024 4.8
echo_true-no-overflow_true-valid-memsafety.i 0 870    4600 3900   - - - 0 .020 4.9
expand_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 32    250 290   - - - 0 .020 4.9
fold_true-no-overflow_true-valid-memsafety.i 0 4.0  56 48   - - - 0 .019 4.9
head_true-no-overflow_true-valid-deref.i 0 4.3  61 49   - - - 0 .019 4.8
hostid_true-no-overflow_true-valid-memsafety.i 0 560    12000 7400   - - - 0 .024 4.8
logname_true-no-overflow_true-valid-memsafety.i 0 .68 44 6.3 - - - 0 .019 4.9
ls-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 870    700 4200   - - - 0 .018 5.0
mkdir_true-no-overflow_true-valid-memsafety.i 0 870    2400 4500   - - - 0 .023 4.8
mkfifo-incomplete_true-no-overflow_true-valid-memsafety.i 0 .73 43 8.4 - - - 0 .023 4.8
od_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 870    830 4300   - - - 0 .023 4.9
printf_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 20    130 220   - - - 0 .017 5.0
readlink_true-no-overflow_true-valid-memsafety.i 0 1.4  49 15   - - - 0 .020 4.9
realpath_true-no-overflow_true-valid-memsafety.i 0 .77 44 7.7 - - - 0 .018 4.9
rm_true-no-overflow_true-valid-memsafety.i 0 870    400 10000   - - - 0 .027 4.8
seq_true-no-overflow_true-valid-memsafety.i 0 1.3  57 14   - - - 0 .018 4.9
sleep_true-no-overflow_true-valid-deref.i 0 1.4  47 16   - - - 0 .018 4.9
stty_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 54    210 470   - - - 0 .018 4.8
sync_true-no-overflow_true-valid-memsafety.i 0 .66 42 6.4 - - - 0 .018 4.8
tac_true-no-overflow_true-valid-memsafety.i 0 3.2  51 40   - - - 0 .018 4.8
tee_true-no-overflow_true-valid-memsafety.i 0 1.7  53 16   - - - 0 .019 4.9
test-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 870    760 6400   - - - 0 .019 4.8
touch_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 3.2  140 37   - - - 0 .019 4.9
uname_true-no-overflow_true-valid-memsafety.i 0 1.6  160 17   - - - 0 .018 4.8
uniq_true-no-overflow_true-valid-memsafety.i 0 2.6  50 30   - - - 0 .018 4.8
usleep_true-no-overflow_true-valid-memsafety.i 0 .74 44 7.1 - - - 0 .018 4.9
uudecode_true-no-overflow_true-valid-memsafety.i 0 6.7  98 77   - - - 0 .019 4.8
wc_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 870    800 4800   - - - 0 .018 4.9
who_true-no-overflow_true-valid-memsafety.i 0 1.3  51 17   - - - 0 .023 4.9
whoami-incomplete_true-no-overflow_true-valid-memsafety.i 0 660    12000 6800   - - - 0 .019 4.9
yes_true-no-overflow_true-valid-memsafety.i 0 .74 45 6.6 - - - 0 .038 4.9
sv-benchmarks/c/busybox-1.22.0/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
total 70 0 15000 70000 110000 34 0 18 1500 34 0 .80 170 34 0 .054 9.4 37 0 .77 180
    correct results 0 0 0 0 0
        correct true 0 0 0 0 0
        correct false 0 0 0 0 0
    incorrect results 0 0 0 0 0
        incorrect true 0 0 0 0 0
        incorrect false 0 0 0 0 0
score (71 tasks, max score: 108) 0 0 0 0 0
Run set cbmc.sv-comp18.Systems_BusyBox_NoOverflows cpa-seq-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.Systems_BusyBox_NoOverflows uautomizer-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.Systems_BusyBox_NoOverflows fshell-witness2test-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.Systems_BusyBox_NoOverflows uautomizer-validate-correctness-witnesses-cbmc.sv-comp18-correctness-witness.Systems_BusyBox_NoOverflows