Tool ULTIMATE Kojak 0.1.23-3204b741 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* [apollon037; apollon054; apollon077; apollon078; apollon115] 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]
Date of execution 2017-12-03 04:40:15 CET 2017-12-03 05:43:12 CET 2017-12-03 06:07:12 CET 2017-12-03 06:08:25 CET 2017-12-03 05:47:35 CET
Run set ukojak.sv-comp18.Systems_BusyBox_MemSafety cpa-seq-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.Systems_BusyBox_MemSafety uautomizer-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.Systems_BusyBox_MemSafety fshell-witness2test-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.Systems_BusyBox_MemSafety uautomizer-validate-correctness-witnesses-ukojak.sv-comp18-correctness-witness.Systems_BusyBox_MemSafety
Options --full-output -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/ukojak.2017-12-03_0440.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/ukojak.2017-12-03_0440.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/ukojak.2017-12-03_0440.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/ukojak.2017-12-03_0440.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 0 7.6 230 64 0 .66 44 0 .018 4.8 0 .0034 .28 -
head_false-valid-deref.i 0 900   5500 12000 0 .53 43 0 .021 4.9 0 .0011 .29 -
sleep_false-valid-deref.i 0 900   3600 12000 0 .52 43 0 .019 4.9 0 .0011 .31 -
chgrp-incomplete_true-no-overflow_false-valid-memtrack.i 0 900   2900 12000 0 .60 43 0 .019 4.9 0 .0019 .28 -
basename_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 8.0 230 61 - - - 0 .019 4.8
chroot-incomplete_true-no-overflow_true-valid-memsafety.i 0 900   4100 15000 - - - 0 .019 5.0
cut_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 900   5600 13000 - - - 0 .024 4.8
date_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 8.9 230 72 - - - 0 .020 4.8
dirname_true-no-overflow_true-valid-memsafety.i 0 7.6 230 64 - - - 0 .019 4.8
du_true-no-overflow_true-valid-memsafety.i 0 900   5300 10000 - - - 0 .020 4.9
echo_true-no-overflow_true-valid-memsafety.i 0 900   3900 14000 - - - 0 .020 4.8
expand_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 900   5600 12000 - - - 0 .018 4.9
fold_true-no-overflow_true-valid-memsafety.i 0 900   4800 11000 - - - 0 .018 4.9
hostid_true-no-overflow_true-valid-memsafety.i 0 900   1900 11000 - - - 0 .019 4.9
logname_true-no-overflow_true-valid-memsafety.i 0 900   2100 12000 - - - 0 .019 4.9
ls-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 9.3 240 70 - - - 0 .018 4.9
mkdir_true-no-overflow_true-valid-memsafety.i 0 900   5100 13000 - - - 0 .018 4.9
mkfifo-incomplete_true-no-overflow_true-valid-memsafety.i 0 900   2200 11000 - - - 0 .018 4.9
od_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 5.6 280 42 - - - 0 .019 4.9
printf_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 900   5500 15000 - - - 0 .022 5.0
readlink_true-no-overflow_true-valid-memsafety.i 0 900   3500 11000 - - - 0 .023 4.9
realpath_true-no-overflow_true-valid-memsafety.i 0 900   2100 13000 - - - 0 .019 4.9
rm_true-no-overflow_true-valid-memsafety.i 0 900   3700 14000 - - - 0 .022 5.0
seq_true-no-overflow_true-valid-memsafety.i 0 8.6 240 79 - - - 0 .018 4.9
stty_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 9.5 310 73 - - - 0 .024 5.0
sync_true-no-overflow_true-valid-memsafety.i 0 900   2100 14000 - - - 0 .019 4.9
tac_true-no-overflow_true-valid-memsafety.i 0 900   4700 13000 - - - 0 .018 4.9
tee_true-no-overflow_true-valid-memsafety.i 0 900   5200 9200 - - - 0 .019 4.9
test-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 8.7 240 77 - - - 0 .018 4.9
touch_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 900   5600 12000 - - - 0 .019 4.9
uname_true-no-overflow_true-valid-memsafety.i 0 900   5500 12000 - - - 0 .022 4.9
uniq_true-no-overflow_true-valid-memsafety.i 0 900   4100 12000 - - - 0 .020 4.9
usleep_true-no-overflow_true-valid-memsafety.i 0 900   2500 14000 - - - 0 .019 4.8
uudecode_true-no-overflow_true-valid-memsafety.i 0 9.1 240 76 - - - 0 .017 4.9
wc_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 900   4400 14000 - - - 0 .019 4.9
who_true-no-overflow_true-valid-memsafety.i 0 8.6 240 67 - - - 0 .021 4.8
whoami-incomplete_true-no-overflow_true-valid-memsafety.i 0 900   1900 12000 - - - 0 .030 4.8
yes_true-no-overflow_true-valid-memsafety.i 0 900   2000 12000 - - - 0 .018 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 24000 110000 340000 4 0 2.3 170 4 0 .077 19 4 0 .0075 1.2 34 0 .68 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 ukojak.sv-comp18.Systems_BusyBox_MemSafety cpa-seq-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.Systems_BusyBox_MemSafety uautomizer-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.Systems_BusyBox_MemSafety fshell-witness2test-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.Systems_BusyBox_MemSafety uautomizer-validate-correctness-witnesses-ukojak.sv-comp18-correctness-witness.Systems_BusyBox_MemSafety