Tool DepthK 3.1 CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a CPA-witness2test 1.7-svn 29852 CProver witness2test 0.1 ULTIMATE Automizer 0.1.23-635dfa2a
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* [apollon001; apollon005; apollon039; apollon053; apollon087; apollon091] [apollon007; apollon009; apollon073; apollon078] apollon*
OS Linux 4.15.0-42-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB
Date of execution 2018-12-05 09:36:33 CET 2018-12-06 10:02:56 CET 2018-12-06 11:08:44 CET 2018-12-06 11:42:46 CET 2018-12-12 19:35:41 CET 2018-12-06 10:24:56 CET
Run set depthk.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety cpa-seq-validate-violation-witnesses-depthk.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety uautomizer-validate-violation-witnesses-depthk.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety cpa-witness2test-validate-violation-witnesses-depthk.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety fshell-witness2test-validate-violation-witnesses-depthk.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety uautomizer-validate-correctness-witnesses-depthk.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -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 -witness ../../results-verified/depthk.2018-12-05_0936.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/depthk.2018-12-05_0936.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true -witness ../../results-verified/depthk.2018-12-05_0936.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/depthk.2018-12-05_0936.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/depthk.2018-12-05_0936.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/busybox-1.22.0/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
basename_false-valid-deref.i false(valid-deref) 0 wit inspect 350 350 650 5300 310 0   error (invalid witness file) 0 --- inspect 3.7  2.0  200 0   0   true -32 --- inspect 15     8.6   470   .62 0   error (invalid witness file) 0 --- inspect 3.9  2.2  210 0   0   error (1) 0 --- inspect .072  .072  12    0   0   - --- inspect
head_false-valid-deref.i out of memory (false(valid-deref)) 0 --- inspect 22 22 15000 250 21 0   error (invalid witness file) 0 --- inspect .71 .44 41 0   0   error (2) 0 --- inspect .022 .024 5.7 0    0   error (invalid witness file) 0 --- inspect .97 .63 48 0   0   error (invalid witness file) 0 --- inspect .0022 .0031 .52 0   0   - --- inspect
sleep_false-valid-deref.i unknown 0 --- inspect 900 900 800 10000 52 0   error (invalid witness file) 0 --- inspect .70 .43 40 0   0   error (2) 0 --- inspect .023 .025 5.7 0    0   error (invalid witness file) 0 --- inspect .94 .60 47 0   0   error (invalid witness file) 0 --- inspect .0019 .0045 .53 0   0   - --- inspect
chgrp-incomplete_true-no-overflow_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 580 580 980 7000 310 0   error (invalid witness file) 0 --- inspect 3.7  2.0  210 0   0   unknown 0 --- inspect 7.6   4.3   300   .66 0   error (invalid witness file) 0 --- inspect 4.3  2.3  220 0   0   error (1) 0 --- inspect .070  .070  11    0   0   - --- inspect
basename_false-unreach-call_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 900 900 810 12000 320 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
chroot-incomplete_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 900 900 2200 7100 310 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.7 0    0  
cut_false-unreach-call_true-no-overflow_true-valid-memsafety.i out of memory (false(no-overflow)) 0 --- inspect 22 22 15000 280 21 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
date_false-unreach-call_true-no-overflow_true-valid-memsafety.i out of memory (false(no-overflow)) 0 --- inspect 22 22 15000 280 21 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .026 5.6 0    0  
dirname_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 900 900 920 11000 760 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .023 5.6 0    0  
du_true-no-overflow_true-valid-memsafety.i out of memory (false(no-overflow)) 0 --- inspect 22 22 15000 240 21 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.7 0    0  
echo_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 900 900 1700 10000 290 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .027 5.6 0    0  
expand_false-unreach-call_true-no-overflow_true-valid-memsafety.i out of memory (false(no-overflow)) 0 --- inspect 24 24 15000 290 21 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
fold_true-no-overflow_true-valid-memsafety.i out of memory (false(no-overflow)) 0 --- inspect 22 22 15000 270 21 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
head_true-no-overflow_true-valid-memsafety.i out of memory (false(no-overflow)) 0 --- inspect 22 22 15000 310 21 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
hostid_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 900 900 670 10000 560 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .024 5.6 0    0  
logname_true-no-overflow_true-valid-memsafety.i false(valid-deref) -16 wit inspect 830 830 1500 7200 310 0   - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 --- inspect 9.1   5.1   290   .62 0  
ls-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i out of memory (false(no-overflow)) 0 --- inspect 23 22 15000 300 21 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .024 5.6 0    0  
mkdir_true-no-overflow_true-valid-memsafety.i out of memory (false(no-overflow)) 0 --- inspect 22 22 15000 260 21 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0    0  
mkfifo-incomplete_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 900 900 1700 8500 270 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .024 5.6 0    0  
od_false-unreach-call_true-no-overflow_true-valid-memsafety.i out of memory (false(no-overflow)) 0 --- inspect 22 22 15000 250 21 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0    0  
printf_false-unreach-call_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 900 900 2000 7600 51 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .024 5.6 0    0  
readlink_true-no-overflow_true-valid-memsafety.i out of memory (false(no-overflow)) 0 --- inspect 22 22 15000 260 18 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .024 5.6 0    0  
realpath_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 900 900 1600 8700 200 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.5 0    0  
rm_true-no-overflow_true-valid-memsafety.i out of memory (false(no-overflow)) 0 --- inspect 22 22 15000 260 21 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0    0  
seq_true-no-overflow_true-valid-memsafety.i out of memory (false(no-overflow)) 0 --- inspect 22 22 15000 270 21 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .024 5.7 0    0  
sleep_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 900 900 870 12000 51 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .022 5.6 0    0  
stty_false-unreach-call_true-no-overflow_true-valid-memsafety.i out of memory (false(no-overflow)) 0 --- inspect 23 23 15000 270 21 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .020 5.6 0    0  
sync_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 900 900 610 13000 490 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.7 0    0  
tac_true-no-overflow_true-valid-memsafety.i out of memory (false(no-overflow)) 0 --- inspect 22 22 15000 290 21 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .025 5.6 0    0  
tee_true-no-overflow_true-valid-memsafety.i out of memory (false(no-overflow)) 0 --- inspect 22 22 15000 280 21 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .026 5.7 0    0  
test-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 900 900 15000 5900 52 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.8 0    0  
touch_false-unreach-call_true-no-overflow_true-valid-memsafety.i out of memory (false(no-overflow)) 0 --- inspect 22 22 15000 250 21 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .024 5.6 0    0  
uname_true-no-overflow_true-valid-memsafety.i out of memory (false(no-overflow)) 0 --- inspect 22 22 15000 250 21 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0    0  
uniq_true-no-overflow_true-valid-memsafety.i out of memory (false(no-overflow)) 0 --- inspect 22 22 15000 270 21 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0    0  
usleep_true-no-overflow_true-valid-memsafety.i false(valid-deref) -16 wit inspect 85 85 350 990 300 0   - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 --- inspect 7.5   4.4   290   .66 0  
uudecode_true-no-overflow_true-valid-memsafety.i out of memory (false(no-overflow)) 0 --- inspect 22 22 15000 270 21 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0    0  
wc_false-unreach-call_true-no-overflow_true-valid-memsafety.i out of memory (false(no-overflow)) 0 --- inspect 22 22 15000 250 21 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0    0  
who_true-no-overflow_true-valid-memsafety.i out of memory (false(no-overflow)) 0 --- inspect 22 22 15000 270 21 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
whoami-incomplete_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 900 900 700 9600 520 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .024 5.6 0    0  
yes_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 360 360 1200 3800 310 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .022 5.6 0    0  
sv-benchmarks/c/busybox-1.22.0/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
total 40 -32 14000 14000 360000 160000 5900 0   4 0 8.8 4.8 490 0   0   4 -32 22 13   780 1.3  0   4 0 10 5.8 520 0   0   4 0 .15 .15 24 0   0   36 0 17 10 780 1.3 0  
    correct results 0 0 0 0 0 0
        correct true 0 0 0 0 0 0
        correct false 0 0 0 0 0 0
    correct-unconfimed results 2 0 930 930 1600 12000 610 0   0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0
        correct-unconfirmed false 2 0 930 930 1600 12000 610 0   0 0 0 0 0
    incorrect results 2 -32 910 910 1900 8200 610 0   0 1 -32 15 8.6 470 .62 0   0 0 0
        incorrect true 0 0 1 -32 15 8.6 470 .62 0   0 0 0
        incorrect false 2 -32 910 910 1900 8200 610 0   0 0 0 0 0
score (40 tasks, max score: 76) -32 0 -32 0 0 0
Run set depthk.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety cpa-seq-validate-violation-witnesses-depthk.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety uautomizer-validate-violation-witnesses-depthk.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety cpa-witness2test-validate-violation-witnesses-depthk.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety fshell-witness2test-validate-violation-witnesses-depthk.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety uautomizer-validate-correctness-witnesses-depthk.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety