Tool ULTIMATE Taipan 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*
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 07:53:44 CET 2017-12-03 08:20:31 CET 2017-12-03 08:37:50 CET 2017-12-03 08:38:58 CET 2017-12-03 08:21:58 CET
Run set utaipan.sv-comp18.Systems_BusyBox_MemSafety cpa-seq-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.Systems_BusyBox_MemSafety uautomizer-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.Systems_BusyBox_MemSafety fshell-witness2test-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.Systems_BusyBox_MemSafety uautomizer-validate-correctness-witnesses-utaipan.sv-comp18-correctness-witness.Systems_BusyBox_MemSafety
Options --full-output -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/utaipan.2017-12-03_0753.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/utaipan.2017-12-03_0753.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/utaipan.2017-12-03_0753.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/utaipan.2017-12-03_0753.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 8.2 230 62 0 .57 43 0 .027 4.9 0 .0037 .33 -
head_false-valid-deref.i 0 900   5100 9500 0 .51 41 0 .048 4.8 0 .0013 .34 -
sleep_false-valid-deref.i 0 900   4700 9900 0 .59 42 0 .018 4.8 0 .0036 .36 -
chgrp-incomplete_true-no-overflow_false-valid-memtrack.i 0 900   4700 12000 0 .57 44 0 .025 4.8 0 .0037 .31 -
basename_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 7.7 230 66 - - - 0 .035 4.8
chroot-incomplete_true-no-overflow_true-valid-memsafety.i 0 900   4800 10000 - - - 0 .036 4.8
cut_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 900   5900 10000 - - - 0 .033 5.0
date_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 8.8 230 69 - - - 0 .042 4.9
dirname_true-no-overflow_true-valid-memsafety.i 0 7.7 230 65 - - - 0 .041 4.9
du_true-no-overflow_true-valid-memsafety.i 0 900   5200 9400 - - - 0 .019 4.8
echo_true-no-overflow_true-valid-memsafety.i 0 900   4800 10000 - - - 0 .047 5.0
expand_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 900   5600 9800 - - - 0 .031 4.9
fold_true-no-overflow_true-valid-memsafety.i 0 900   5000 13000 - - - 0 .048 4.8
hostid_true-no-overflow_true-valid-memsafety.i 0 900   2700 11000 - - - 0 .018 4.9
logname_true-no-overflow_true-valid-memsafety.i 0 900   3700 12000 - - - 0 .038 4.9
ls-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 9.6 240 75 - - - 0 .021 4.8
mkdir_true-no-overflow_true-valid-memsafety.i 0 900   5600 12000 - - - 0 .018 4.8
mkfifo-incomplete_true-no-overflow_true-valid-memsafety.i 0 900   3700 11000 - - - 0 .044 4.8
od_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 5.9 300 49 - - - 0 .049 5.0
printf_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 900   5100 10000 - - - 0 .031 4.8
readlink_true-no-overflow_true-valid-memsafety.i 0 900   4700 10000 - - - 0 .044 4.9
realpath_true-no-overflow_true-valid-memsafety.i 0 900   3600 8500 - - - 0 .018 4.8
rm_true-no-overflow_true-valid-memsafety.i 0 900   4800 11000 - - - 0 .019 4.8
seq_true-no-overflow_true-valid-memsafety.i 0 8.5 230 64 - - - 0 .020 5.0
stty_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 9.9 300 75 - - - 0 .023 4.9
sync_true-no-overflow_true-valid-memsafety.i 0 900   3600 12000 - - - 0 .044 4.9
tac_true-no-overflow_true-valid-memsafety.i 0 900   4900 12000 - - - 0 .027 4.8
tee_true-no-overflow_true-valid-memsafety.i 0 900   5200 9000 - - - 0 .019 4.9
test-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 9.2 240 81 - - - 0 .021 4.9
touch_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 900   5400 11000 - - - 0 .036 4.9
uname_true-no-overflow_true-valid-memsafety.i 0 900   5900 11000 - - - 0 .018 4.8
uniq_true-no-overflow_true-valid-memsafety.i 0 900   4800 9700 - - - 0 .023 4.8
usleep_true-no-overflow_true-valid-memsafety.i 0 900   3500 12000 - - - 0 .055 4.8
uudecode_true-no-overflow_true-valid-memsafety.i 0 8.9 240 74 - - - 0 .020 4.8
wc_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 900   5000 12000 - - - 0 .021 4.8
who_true-no-overflow_true-valid-memsafety.i 0 8.6 240 65 - - - 0 .027 4.9
whoami-incomplete_true-no-overflow_true-valid-memsafety.i 0 900   3900 11000 - - - 0 .018 4.9
yes_true-no-overflow_true-valid-memsafety.i 0 900   3600 9800 - - - 0 .050 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 130000 290000 4 0 2.2 170 4 0 .12 19 4 0 .012 1.3 34 0 1.1 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 utaipan.sv-comp18.Systems_BusyBox_MemSafety cpa-seq-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.Systems_BusyBox_MemSafety uautomizer-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.Systems_BusyBox_MemSafety fshell-witness2test-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.Systems_BusyBox_MemSafety uautomizer-validate-correctness-witnesses-utaipan.sv-comp18-correctness-witness.Systems_BusyBox_MemSafety