Tool DepthK DepthK version 3.0 - Fri Jan 6 18:14:20 AMT 2017 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* [apollon075; apollon077; apollon078] [apollon016; apollon038; apollon064; apollon078; apollon084; apollon107] [apollon016; apollon038; apollon078; apollon084; apollon107] 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-01 13:07:37 CET 2017-12-01 14:46:42 CET 2017-12-01 15:12:32 CET 2017-12-01 15:13:50 CET 2017-12-01 14:48:36 CET
Run set depthk.sv-comp18.Systems_BusyBox_NoOverflows cpa-seq-validate-violation-witnesses-depthk.sv-comp18-violation-witness.Systems_BusyBox_NoOverflows uautomizer-validate-violation-witnesses-depthk.sv-comp18-violation-witness.Systems_BusyBox_NoOverflows fshell-witness2test-validate-violation-witnesses-depthk.sv-comp18-violation-witness.Systems_BusyBox_NoOverflows uautomizer-validate-correctness-witnesses-depthk.sv-comp18-correctness-witness.Systems_BusyBox_NoOverflows
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/depthk.2017-12-01_1307.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/depthk.2017-12-01_1307.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/depthk.2017-12-01_1307.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/depthk.2017-12-01_1307.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 unknown 0 wit inspect 900 2700 6500 error (invalid witness file) 0 wit inspect .50 44 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0012 .32 - wit inspect
chroot-incomplete_false-no-overflow.i unknown 0 wit inspect 900 930 8200 error (invalid witness file) 0 wit inspect .48 45 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0014 .29 - wit inspect
cut_false-no-overflow.i unknown 0 wit inspect 48 500 660 error (invalid witness file) 0 wit inspect .50 41 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .0013 .29 - wit inspect
date_false-no-overflow.i unknown 0 wit inspect 51 500 660 error (invalid witness file) 0 wit inspect .40 41 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .0011 .27 - wit inspect
du_false-no-overflow.i unknown 0 wit inspect 46 500 700 error (invalid witness file) 0 wit inspect .50 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect
echo_false-no-overflow.i unknown 0 wit inspect 890 700 9400 error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0012 .30 - wit inspect
expand_false-no-overflow.i unknown 0 wit inspect 60 940 730 error (invalid witness file) 0 wit inspect .49 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect
fold_false-no-overflow.i unknown 0 wit inspect 46 550 630 error (invalid witness file) 0 wit inspect .50 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .0011 .31 - wit inspect
head_false-no-overflow.i unknown 0 wit inspect 900 2400 10000 error (invalid witness file) 0 wit inspect .44 41 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect
logname_false-no-overflow.i unknown 0 wit inspect 900 1000 13000 error (invalid witness file) 0 wit inspect .48 44 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0013 .30 - wit inspect
ls-incomplete_false-no-overflow.i unknown 0 wit inspect 58 59 710 error (invalid witness file) 0 wit inspect .48 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .0012 .27 - wit inspect
mkdir_false-no-overflow.i unknown 0 wit inspect 47 500 560 error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0011 .27 - wit inspect
mkfifo-incomplete_false-no-overflow.i unknown 0 wit inspect 900 1200 9600 error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0012 .33 - wit inspect
od_false-no-overflow.i unknown 0 wit inspect 63 1700 750 error (invalid witness file) 0 wit inspect .49 44 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0013 .30 - wit inspect
printf_false-no-overflow.i unknown 0 wit inspect 900 2000 12000 error (invalid witness file) 0 wit inspect .41 41 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .0013 .33 - wit inspect
readlink_false-no-overflow.i unknown 0 wit inspect 39 43 470 error (invalid witness file) 0 wit inspect .50 41 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .0012 .29 - wit inspect
realpath_false-no-overflow.i unknown 0 wit inspect 900 1200 13000 error (invalid witness file) 0 wit inspect .48 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .0012 .34 - wit inspect
rm_false-no-overflow.i unknown 0 wit inspect 44 500 520 error (invalid witness file) 0 wit inspect .56 42 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .0011 .27 - wit inspect
seq_false-no-overflow.i unknown 0 wit inspect 42 500 630 error (invalid witness file) 0 wit inspect .50 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect
sleep_false-no-overflow.i unknown 0 wit inspect 900 1000 9100 error (invalid witness file) 0 wit inspect .49 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect
stty_false-no-overflow.i unknown 0 wit inspect 900 2000 10000 error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect
sync_false-no-overflow.i unknown 0 wit inspect 890 1300 5700 error (invalid witness file) 0 wit inspect .50 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect
tac_false-no-overflow.i unknown 0 wit inspect 42 500 560 error (invalid witness file) 0 wit inspect .44 44 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect
tee_false-no-overflow.i unknown 0 wit inspect 43 500 620 error (invalid witness file) 0 wit inspect .49 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0012 .31 - wit inspect
test-incomplete_false-no-overflow.i unknown 0 wit inspect 890 1600 8000 error (invalid witness file) 0 wit inspect .49 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect
touch_false-no-overflow.i unknown 0 wit inspect 47 500 630 error (invalid witness file) 0 wit inspect .39 41 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect
uname_false-no-overflow.i unknown 0 wit inspect 43 510 610 error (invalid witness file) 0 wit inspect .50 41 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .0015 .28 - wit inspect
uniq_false-no-overflow.i unknown 0 wit inspect 44 510 550 error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0014 .29 - wit inspect
usleep_false-no-overflow.i unknown 0 wit inspect 890 1400 5800 error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .044 4.8 error (invalid witness file) 0 wit inspect .0011 .35 - wit inspect
uudecode_false-no-overflow.i unknown 0 wit inspect 50 500 710 error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect
wc_false-no-overflow.i unknown 0 wit inspect 45 510 550 error (invalid witness file) 0 wit inspect .39 41 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect
who_false-no-overflow.i unknown 0 wit inspect 40 44 510 error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect
whoami-incomplete_false-no-overflow.i - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0013 .28 - wit inspect
yes_false-no-overflow.i unknown 0 wit inspect 900 1200 9900 error (invalid witness file) 0 wit inspect .50 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0013 .29 - wit inspect
basename_false-unreach-call_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 890 1300 5800 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.8
chgrp-incomplete_true-no-overflow_false-valid-memtrack.i unknown 0 wit inspect 900 2700 7600 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
chroot-incomplete_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 900 930 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.9
cut_false-unreach-call_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 48 500 650 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
date_false-unreach-call_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 49 49 630 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
dirname_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 890 960 7500 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
du_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 47 510 540 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
echo_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 890 700 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
expand_false-unreach-call_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 61 940 750 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
fold_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 46 550 550 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
head_true-no-overflow_true-valid-deref.i unknown 0 wit inspect 900 2400 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
hostid_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 900 1100 5300 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
logname_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 900 1000 9900 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
ls-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 58 59 680 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
mkdir_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 47 510 670 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
mkfifo-incomplete_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 900 1200 13000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
od_false-unreach-call_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 64 1700 760 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
printf_false-unreach-call_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 900 2000 9500 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
readlink_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 40 45 500 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
realpath_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 900 1200 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
rm_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 45 510 540 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.8
seq_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 42 500 490 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
sleep_true-no-overflow_true-valid-deref.i unknown 0 wit inspect 900 1500 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
stty_false-unreach-call_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 900 2000 9300 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
sync_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 890 1300 5700 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.9
tac_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 43 510 490 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
tee_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 43 510 550 - 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 unknown 0 wit inspect 890 1600 8300 - 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 unknown 0 wit inspect 48 510 650 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
uname_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 43 500 470 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
uniq_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 44 500 650 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
usleep_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 890 1400 8500 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
uudecode_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 51 500 700 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .042 4.8
wc_false-unreach-call_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 45 500 650 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
who_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 40 44 560 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.8
whoami-incomplete_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 890 1200 8500 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
yes_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 900 1200 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .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 70 0 30000 66000 320000 34 0 17 1400 34 0 .67 170 34 0 .043 9.7 37 0 .74 180
    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 (71 tasks, max score: 108) 0 0 0 0 0
Run set depthk.sv-comp18.Systems_BusyBox_NoOverflows cpa-seq-validate-violation-witnesses-depthk.sv-comp18-violation-witness.Systems_BusyBox_NoOverflows uautomizer-validate-violation-witnesses-depthk.sv-comp18-violation-witness.Systems_BusyBox_NoOverflows fshell-witness2test-validate-violation-witnesses-depthk.sv-comp18-violation-witness.Systems_BusyBox_NoOverflows uautomizer-validate-correctness-witnesses-depthk.sv-comp18-correctness-witness.Systems_BusyBox_NoOverflows