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*
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 11:17:40 CET 2017-12-03 11:52:51 CET 2017-12-03 12:03:01 CET 2017-12-03 12:03:17 CET 2017-12-03 11:54:19 CET
Run set ukojak.sv-comp18.Systems_BusyBox_NoOverflows cpa-seq-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.Systems_BusyBox_NoOverflows uautomizer-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.Systems_BusyBox_NoOverflows fshell-witness2test-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.Systems_BusyBox_NoOverflows uautomizer-validate-correctness-witnesses-ukojak.sv-comp18-correctness-witness.Systems_BusyBox_NoOverflows
Options --full-output -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/ukojak.2017-12-03_1117.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_1117.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/ukojak.2017-12-03_1117.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/ukojak.2017-12-03_1117.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 timeout 0 wit inspect 900   2500 12000 error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .047 5.0 error (invalid witness file) 0 wit inspect .0022 .31 - wit inspect
chroot-incomplete_false-no-overflow.i error (7) 0 wit inspect 310   3300 3900 error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0039 .35 - wit inspect
cut_false-no-overflow.i timeout 0 wit inspect 900   5200 11000 error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .046 5.0 error (invalid witness file) 0 wit inspect .0036 .26 - wit inspect
date_false-no-overflow.i error (7) 0 wit inspect 4.3 240 34 error (invalid witness file) 0 wit inspect .54 47 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0044 .26 - wit inspect
du_false-no-overflow.i timeout 0 wit inspect 900   4200 9800 error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .0036 .29 - wit inspect
echo_false-no-overflow.i timeout 0 wit inspect 900   5200 13000 error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .045 4.8 error (invalid witness file) 0 wit inspect .0044 .26 - wit inspect
expand_false-no-overflow.i timeout 0 wit inspect 900   5400 13000 error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .032 4.9 error (invalid witness file) 0 wit inspect .0049 .28 - wit inspect
fold_false-no-overflow.i timeout 0 wit inspect 900   5100 12000 error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .051 4.9 error (invalid witness file) 0 wit inspect .0041 .34 - wit inspect
head_false-no-overflow.i timeout 0 wit inspect 900   4900 11000 error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect
logname_false-no-overflow.i error 0 wit inspect 47   1000 430 error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .047 4.9 error (invalid witness file) 0 wit inspect .0011 .35 - wit inspect
ls-incomplete_false-no-overflow.i error (7) 0 wit inspect 4.5 230 40 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0045 .29 - wit inspect
mkdir_false-no-overflow.i timeout 0 wit inspect 900   5000 11000 error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .048 4.8 error (invalid witness file) 0 wit inspect .0043 .30 - wit inspect
mkfifo-incomplete_false-no-overflow.i error (7) 0 wit inspect 69   1500 690 error (invalid witness file) 0 wit inspect .54 45 error (2) 0 wit inspect .048 4.8 error (invalid witness file) 0 wit inspect .0035 .33 - wit inspect
od_false-no-overflow.i error (7) 0 wit inspect 5.7 290 41 error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .035 5.0 error (invalid witness file) 0 wit inspect .0036 .31 - wit inspect
printf_false-no-overflow.i timeout 0 wit inspect 900   4800 13000 error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0017 .36 - wit inspect
readlink_false-no-overflow.i timeout 0 wit inspect 900   5000 11000 error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .031 4.8 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect
realpath_false-no-overflow.i error (7) 0 wit inspect 110   2300 1200 error (invalid witness file) 0 wit inspect .58 44 error (2) 0 wit inspect .046 4.8 error (invalid witness file) 0 wit inspect .0011 .32 - wit inspect
rm_false-no-overflow.i timeout 0 wit inspect 900   6100 11000 error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .053 4.8 error (invalid witness file) 0 wit inspect .0041 .29 - wit inspect
seq_false-no-overflow.i error (7) 0 wit inspect 4.5 240 38 error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .048 4.8 error (invalid witness file) 0 wit inspect .0013 .29 - wit inspect
sleep_false-no-overflow.i error (7) 0 wit inspect 280   3600 3600 error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .041 4.8 error (invalid witness file) 0 wit inspect .0037 .34 - wit inspect
stty_false-no-overflow.i error (7) 0 wit inspect 4.4 290 36 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .030 4.8 error (invalid witness file) 0 wit inspect .0040 .26 - wit inspect
sync_false-no-overflow.i error (7) 0 wit inspect 110   1800 1400 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .048 4.9 error (invalid witness file) 0 wit inspect .0039 .26 - wit inspect
tac_false-no-overflow.i timeout 0 wit inspect 900   5000 12000 error (invalid witness file) 0 wit inspect .60 44 error (2) 0 wit inspect .049 4.8 error (invalid witness file) 0 wit inspect .0048 .29 - wit inspect
tee_false-no-overflow.i timeout 0 wit inspect 900   4500 11000 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .043 4.9 error (invalid witness file) 0 wit inspect .0037 .26 - wit inspect
test-incomplete_false-no-overflow.i error (7) 0 wit inspect 4.4 240 38 error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .032 4.9 error (invalid witness file) 0 wit inspect .0030 .32 - wit inspect
touch_false-no-overflow.i timeout 0 wit inspect 900   5300 13000 error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect
uname_false-no-overflow.i timeout 0 wit inspect 900   5400 10000 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .049 4.8 error (invalid witness file) 0 wit inspect .0033 .28 - wit inspect
uniq_false-no-overflow.i timeout 0 wit inspect 900   5000 13000 error (invalid witness file) 0 wit inspect .50 41 error (2) 0 wit inspect .047 5.0 error (invalid witness file) 0 wit inspect .0035 .34 - wit inspect
usleep_false-no-overflow.i error (7) 0 wit inspect 200   2900 2500 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .048 4.8 error (invalid witness file) 0 wit inspect .0044 .26 - wit inspect
uudecode_false-no-overflow.i error (7) 0 wit inspect 4.7 240 42 error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .042 4.9 error (invalid witness file) 0 wit inspect .0041 .34 - wit inspect
wc_false-no-overflow.i timeout 0 wit inspect 900   4900 13000 error (invalid witness file) 0 wit inspect .54 46 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .0044 .27 - wit inspect
who_false-no-overflow.i error (7) 0 wit inspect 4.4 230 35 error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .022 4.8 error (invalid witness file) 0 wit inspect .0046 .26 - wit inspect
whoami-incomplete_false-no-overflow.i - wit inspect error (1) 0 wit inspect .77 50 true -32 wit inspect 15     510   error (1) 0 wit inspect .12   9.7  - wit inspect
yes_false-no-overflow.i error (7) 0 wit inspect 53   1100 490 error (invalid witness file) 0 wit inspect .52 45 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0032 .27 - wit inspect
basename_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (7) 0 wit inspect 4.2 230 36 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
chgrp-incomplete_true-no-overflow_false-valid-memtrack.i timeout 0 wit inspect 900   2500 10000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
chroot-incomplete_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 .018 4.8
cut_false-unreach-call_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   5200 13000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
date_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (7) 0 wit inspect 4.2 230 37 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.8
dirname_true-no-overflow_true-valid-memsafety.i error (7) 0 wit inspect 3.9 230 36 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .017 4.8
du_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   4300 9800 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
echo_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   5300 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
expand_false-unreach-call_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   5100 13000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.9
fold_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   5000 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .017 4.8
head_true-no-overflow_true-valid-deref.i timeout 0 wit inspect 900   5000 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
hostid_true-no-overflow_true-valid-memsafety.i true 2 wit inspect 18   700 150 - wit inspect - wit inspect - wit inspect true 2 wit inspect 11     420  
logname_true-no-overflow_true-valid-memsafety.i error (7) 0 wit inspect 65   1200 640 - 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 (7) 0 wit inspect 4.9 250 39 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.8
mkdir_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   5100 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
mkfifo-incomplete_true-no-overflow_true-valid-memsafety.i error (7) 0 wit inspect 81   1700 830 - 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 5.9 300 51 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .017 4.9
printf_false-unreach-call_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   4800 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .017 4.8
readlink_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   5000 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .017 4.9
realpath_true-no-overflow_true-valid-memsafety.i error (7) 0 wit inspect 120   3500 1300 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
rm_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   5200 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
seq_true-no-overflow_true-valid-memsafety.i error (7) 0 wit inspect 4.4 230 35 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
sleep_true-no-overflow_true-valid-deref.i error (7) 0 wit inspect 280   3900 3900 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
stty_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (7) 0 wit inspect 5.0 290 39 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
sync_true-no-overflow_true-valid-memsafety.i error (7) 0 wit inspect 100   1700 1200 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
tac_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   5000 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .049 4.9
tee_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   4500 9800 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
test-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (7) 0 wit inspect 4.4 240 38 - 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 timeout 0 wit inspect 900   5300 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .040 4.8
uname_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   5300 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .049 4.9
uniq_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   5000 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
usleep_true-no-overflow_true-valid-memsafety.i error (7) 0 wit inspect 190   2900 2500 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
uudecode_true-no-overflow_true-valid-memsafety.i error (7) 0 wit inspect 4.3 240 38 - 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 timeout 0 wit inspect 900   5000 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
who_true-no-overflow_true-valid-memsafety.i error (7) 0 wit inspect 4.5 240 36 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .045 4.8
whoami-incomplete_true-no-overflow_true-valid-memsafety.i true 2 wit inspect 29   860 290 - wit inspect - wit inspect - wit inspect true 2 wit inspect 17     520  
yes_true-no-overflow_true-valid-memsafety.i error (7) 0 wit inspect 57   1100 550 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
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 4 34000 210000 430000 34 0 19 1500 34 -32 16 670 34 0 .23 19 37 4 28 1100
    correct results 2 4 47 1600 430 0 0 0 2 4 28 940
        correct true 2 4 47 1600 430 0 0 0 2 4 28 940
        correct false 0 0 0 0 0
    incorrect results 0 0 1 -32 15 510 0 0
        incorrect true 0 0 1 -32 15 510 0 0
        incorrect false 0 0 0 0 0
score (71 tasks, max score: 108) 4 0 -32 0 4
Run set ukojak.sv-comp18.Systems_BusyBox_NoOverflows cpa-seq-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.Systems_BusyBox_NoOverflows uautomizer-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.Systems_BusyBox_NoOverflows fshell-witness2test-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.Systems_BusyBox_NoOverflows uautomizer-validate-correctness-witnesses-ukojak.sv-comp18-correctness-witness.Systems_BusyBox_NoOverflows