Tool ULTIMATE Automizer 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 04:39:25 CET 2017-12-03 05:43:13 CET 2017-12-03 06:05:52 CET 2017-12-03 06:06:56 CET 2017-12-03 05:47:48 CET
Run set uautomizer.sv-comp18.Systems_BusyBox_MemSafety cpa-seq-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.Systems_BusyBox_MemSafety uautomizer-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.Systems_BusyBox_MemSafety fshell-witness2test-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.Systems_BusyBox_MemSafety uautomizer-validate-correctness-witnesses-uautomizer.sv-comp18-correctness-witness.Systems_BusyBox_MemSafety
Options --full-output -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/uautomizer.2017-12-03_0439.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/uautomizer.2017-12-03_0439.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/uautomizer.2017-12-03_0439.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/uautomizer.2017-12-03_0439.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 error (7) 0 wit inspect 7.6 230 61 error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .022 4.8 error (invalid witness file) 0 wit inspect .0012 .34 - wit inspect
head_false-valid-deref.i timeout 0 wit inspect 900   4700 10000 error (invalid witness file) 0 wit inspect .56 45 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .0027 .30 - wit inspect
sleep_false-valid-deref.i timeout 0 wit inspect 900   2000 10000 error (invalid witness file) 0 wit inspect .77 41 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0020 .26 - wit inspect
chgrp-incomplete_true-no-overflow_false-valid-memtrack.i timeout 0 wit inspect 900   1800 10000 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0037 .28 - wit inspect
basename_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (7) 0 wit inspect 7.8 220 64 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
chroot-incomplete_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   2200 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
cut_false-unreach-call_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   2600 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
date_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (7) 0 wit inspect 8.5 230 70 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
dirname_true-no-overflow_true-valid-memsafety.i error (7) 0 wit inspect 7.7 230 68 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
du_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   13000 7200 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
echo_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   2500 10000 - 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 timeout 0 wit inspect 900   3600 10000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
fold_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   2500 7200 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
hostid_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   1800 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .025 4.8
logname_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   2300 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
ls-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (7) 0 wit inspect 9.5 240 73 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
mkdir_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   3200 6300 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
mkfifo-incomplete_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   3200 9800 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
od_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (7) 0 wit inspect 6.1 310 52 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
printf_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (7) 0 wit inspect 290   2900 3000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
readlink_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   2100 9100 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
realpath_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   2000 10000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
rm_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   2400 9200 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
seq_true-no-overflow_true-valid-memsafety.i error (7) 0 wit inspect 8.5 230 76 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .028 4.9
stty_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (7) 0 wit inspect 9.3 310 79 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
sync_true-no-overflow_true-valid-memsafety.i error (7) 0 wit inspect 360   2100 4300 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
tac_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   4700 10000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
tee_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   13000 5800 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
test-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (7) 0 wit inspect 8.5 240 78 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
touch_false-unreach-call_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   3500 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
uname_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   4800 9600 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
uniq_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   2500 8200 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
usleep_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   1800 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.9
uudecode_true-no-overflow_true-valid-memsafety.i error (7) 0 wit inspect 8.9 240 70 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
wc_false-unreach-call_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   1900 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
who_true-no-overflow_true-valid-memsafety.i error (7) 0 wit inspect 9.0 230 77 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
whoami-incomplete_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   4900 10000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
yes_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   2300 10000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 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 23000 99000 250000 4 0 2.5 170 4 0 .077 19 4 0 .0096 1.2 34 0 .67 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 uautomizer.sv-comp18.Systems_BusyBox_MemSafety cpa-seq-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.Systems_BusyBox_MemSafety uautomizer-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.Systems_BusyBox_MemSafety fshell-witness2test-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.Systems_BusyBox_MemSafety uautomizer-validate-correctness-witnesses-uautomizer.sv-comp18-correctness-witness.Systems_BusyBox_MemSafety