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* [apollon077; apollon078; apollon091] apollon*
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 08:19:34 CET 2017-12-01 08:48:13 CET 2017-12-01 09:05:59 CET 2017-12-01 09:09:10 CET 2017-12-01 08:49:56 CET
Run set cbmc.sv-comp18.Systems_BusyBox_MemSafety cpa-seq-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.Systems_BusyBox_MemSafety uautomizer-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.Systems_BusyBox_MemSafety fshell-witness2test-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.Systems_BusyBox_MemSafety uautomizer-validate-correctness-witnesses-cbmc.sv-comp18-correctness-witness.Systems_BusyBox_MemSafety
Options --graphml-witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cbmc.2017-12-01_0819.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_0819.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/cbmc.2017-12-01_0819.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cbmc.2017-12-01_0819.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
basename_false-valid-deref.i witness invalid (false(valid-deref)) 0 wit inspect 55    870 490   error 0 wit inspect 5.8  270 error (7) 0 wit inspect 8.1   210   error (invalid witness file) 0 wit inspect .70   20    - wit inspect
head_false-valid-deref.i error (6) 0 wit inspect 5.0  65 56   error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0035 .27 - wit inspect
sleep_false-valid-deref.i error (6) 0 wit inspect 1.7  49 23   error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect .0018 .26 - wit inspect
chgrp-incomplete_true-no-overflow_false-valid-memtrack.i error (6) 0 wit inspect .84 45 8.8 error (invalid witness file) 0 wit inspect .62 43 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .0011 .32 - wit inspect
basename_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (42) 0 wit inspect 870    2200 4300   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.9
chroot-incomplete_true-no-overflow_true-valid-memsafety.i error (6) 0 wit inspect 1.1  44 14   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
cut_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (6) 0 wit inspect 8.9  110 110   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .025 5.0
date_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (6) 0 wit inspect 4.3  160 51   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
dirname_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect 730    12000 9400   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
du_true-no-overflow_true-valid-memsafety.i error (6) 0 wit inspect 69    260 710   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
echo_true-no-overflow_true-valid-memsafety.i error (42) 0 wit inspect 870    9900 4100   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
expand_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (6) 0 wit inspect 38    270 420   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
fold_true-no-overflow_true-valid-memsafety.i error (6) 0 wit inspect 4.8  66 74   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
hostid_true-no-overflow_true-valid-memsafety.i error (42) 0 wit inspect 870    6500 10000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
logname_true-no-overflow_true-valid-memsafety.i error (6) 0 wit inspect .78 44 8.2 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
ls-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (1) 0 wit inspect 870    710 4000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
mkdir_true-no-overflow_true-valid-memsafety.i error (1) 0 wit inspect 870    1200 3800   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
mkfifo-incomplete_true-no-overflow_true-valid-memsafety.i error (6) 0 wit inspect .83 43 7.6 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.9
od_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (1) 0 wit inspect 870    800 4800   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
printf_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (6) 0 wit inspect 26    140 300   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
readlink_true-no-overflow_true-valid-memsafety.i error (6) 0 wit inspect 1.6  50 18   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
realpath_true-no-overflow_true-valid-memsafety.i error (6) 0 wit inspect .86 45 8.6 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
rm_true-no-overflow_true-valid-memsafety.i error (1) 0 wit inspect 870    340 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
seq_true-no-overflow_true-valid-memsafety.i error (6) 0 wit inspect 1.5  57 18   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
stty_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (6) 0 wit inspect 69    230 660   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
sync_true-no-overflow_true-valid-memsafety.i error (6) 0 wit inspect .66 42 8.4 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
tac_true-no-overflow_true-valid-memsafety.i error (6) 0 wit inspect 3.9  59 48   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
tee_true-no-overflow_true-valid-memsafety.i error (6) 0 wit inspect 2.0  53 24   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
test-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (1) 0 wit inspect 870    730 6700   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
touch_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (6) 0 wit inspect 4.0  150 51   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
uname_true-no-overflow_true-valid-memsafety.i error (6) 0 wit inspect 1.9  170 22   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
uniq_true-no-overflow_true-valid-memsafety.i error (6) 0 wit inspect 3.1  51 37   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
usleep_true-no-overflow_true-valid-memsafety.i error (6) 0 wit inspect .76 44 6.5 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
uudecode_true-no-overflow_true-valid-memsafety.i error (6) 0 wit inspect 8.4  110 110   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.8
wc_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (1) 0 wit inspect 870    750 6600   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
who_true-no-overflow_true-valid-memsafety.i error (6) 0 wit inspect 1.6  52 21   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
whoami-incomplete_true-no-overflow_true-valid-memsafety.i error (42) 0 wit inspect 870    5500 9300   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
yes_true-no-overflow_true-valid-memsafety.i error (6) 0 wit inspect .75 44 8.6 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 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 38 0 9800 44000 77000 4 0 7.5 390 4 0 8.2 220 4 0 .71 21 34 0 .66 170
    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 (38 tasks, max score: 72) 0 0 0 0 0
Run set cbmc.sv-comp18.Systems_BusyBox_MemSafety cpa-seq-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.Systems_BusyBox_MemSafety uautomizer-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.Systems_BusyBox_MemSafety fshell-witness2test-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.Systems_BusyBox_MemSafety uautomizer-validate-correctness-witnesses-cbmc.sv-comp18-correctness-witness.Systems_BusyBox_MemSafety