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* [apollon023; apollon077; apollon078; apollon117; apollon126] [apollon077; apollon078; apollon101; apollon157] [apollon045; apollon077; apollon078; apollon158] [apollon007; apollon009; apollon077; apollon078; apollon119]
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] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [4; 8], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33554 MB; 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 09:05:19 CET 2017-12-01 09:58:48 CET 2017-12-01 10:19:41 CET 2017-12-01 10:22:00 CET 2017-12-01 10:02:39 CET
Run set depthk.sv-comp18.Systems_BusyBox_MemSafety cpa-seq-validate-violation-witnesses-depthk.sv-comp18-violation-witness.Systems_BusyBox_MemSafety uautomizer-validate-violation-witnesses-depthk.sv-comp18-violation-witness.Systems_BusyBox_MemSafety fshell-witness2test-validate-violation-witnesses-depthk.sv-comp18-violation-witness.Systems_BusyBox_MemSafety uautomizer-validate-correctness-witnesses-depthk.sv-comp18-correctness-witness.Systems_BusyBox_MemSafety
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/depthk.2017-12-01_0905.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_0905.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/depthk.2017-12-01_0905.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/depthk.2017-12-01_0905.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 unknown 0 wit inspect 900 1300 5900 error (invalid witness file) 0 wit inspect .40 43 error (2) 0 wit inspect .024 4.9 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect
head_false-valid-deref.i unknown 0 wit inspect 900 2900 9900 error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .042 4.9 error (invalid witness file) 0 wit inspect .0020 .31 - wit inspect
sleep_false-valid-deref.i unknown 0 wit inspect 900 2500 11000 error (invalid witness file) 0 wit inspect .40 44 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0036 .29 - wit inspect
chgrp-incomplete_true-no-overflow_false-valid-memtrack.i unknown 0 wit inspect 900 3100 6000 error (invalid witness file) 0 wit inspect .41 43 error (2) 0 wit inspect .017 5.0 error (invalid witness file) 0 wit inspect .0037 .28 - wit inspect
basename_false-unreach-call_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 890 1300 6000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
chroot-incomplete_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 900 880 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 unknown 0 wit inspect 44 46 550 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
date_false-unreach-call_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 49 50 640 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .017 4.9
dirname_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 890 980 5100 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .037 5.0
du_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 45 47 570 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
echo_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 890 750 12000 - 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 46 47 620 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
fold_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 42 45 570 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .039 4.9
hostid_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 890 1100 7900 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
logname_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 900 920 10000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .044 4.9
ls-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 58 59 670 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
mkdir_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 43 45 510 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
mkfifo-incomplete_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 900 3000 11000 - 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 unknown 0 wit inspect 61 56 720 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .017 4.8
printf_false-unreach-call_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 900 2600 9600 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
readlink_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 40 43 470 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
realpath_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 900 3900 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
rm_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 43 46 570 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .038 4.8
seq_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 39 43 480 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .027 4.8
stty_false-unreach-call_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 900 2500 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
sync_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 890 1300 6300 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .065 4.8
tac_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 40 43 560 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .049 4.8
tee_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 40 43 480 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
test-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 890 1600 6200 - 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 46 47 690 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
uname_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 40 43 540 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .036 4.9
uniq_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 41 44 540 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
usleep_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 890 1400 7100 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
uudecode_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 46 48 620 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
wc_false-unreach-call_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 41 44 520 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
who_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 40 44 480 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
whoami-incomplete_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 890 1200 6100 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
yes_true-no-overflow_true-valid-memsafety.i unknown 0 wit inspect 900 1200 10000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
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 18000 35000 170000 4 0 1.8 170 4 0 .10 20 4 0 .010 1.1 34 0 .82 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 depthk.sv-comp18.Systems_BusyBox_MemSafety cpa-seq-validate-violation-witnesses-depthk.sv-comp18-violation-witness.Systems_BusyBox_MemSafety uautomizer-validate-violation-witnesses-depthk.sv-comp18-violation-witness.Systems_BusyBox_MemSafety fshell-witness2test-validate-violation-witnesses-depthk.sv-comp18-violation-witness.Systems_BusyBox_MemSafety uautomizer-validate-correctness-witnesses-depthk.sv-comp18-correctness-witness.Systems_BusyBox_MemSafety