Tool ULTIMATE Automizer 0.1.23-635dfa2a 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*
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-08 07:42:40 CET 2018-12-09 20:30:54 CET 2018-12-09 21:05:03 CET 2018-12-09 21:08:07 CET 2018-12-12 21:10:19 CET 2018-12-09 20:42:29 CET
Run set uautomizer.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety cpa-seq-validate-violation-witnesses-uautomizer.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety uautomizer-validate-violation-witnesses-uautomizer.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety cpa-witness2test-validate-violation-witnesses-uautomizer.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety fshell-witness2test-validate-violation-witnesses-uautomizer.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety uautomizer-validate-correctness-witnesses-uautomizer.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety
Options --full-output -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/uautomizer.2018-12-08_0742.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/uautomizer.2018-12-08_0742.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/uautomizer.2018-12-08_0742.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/uautomizer.2018-12-08_0742.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/uautomizer.2018-12-08_0742.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 unknown 0 --- inspect 820   750   2600 9300 .68 .086  error (invalid witness file) 0 --- inspect .78 .48 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0   error (invalid witness file) 0 --- inspect 1.0  .65 48 0   0   error (invalid witness file) 0 --- inspect .0046 .0056 .40 0   0   - --- inspect
head_false-valid-deref.i unknown 0 --- inspect 8.8 3.0 340 61 .66 0      error (invalid witness file) 0 --- inspect .60 .36 41 0   0   error (2) 0 --- inspect .022 .024 5.6 0   0   error (invalid witness file) 0 --- inspect .98 .64 48 0   0   error (invalid witness file) 0 --- inspect .0056 .0068 .53 0   0   - --- inspect
sleep_false-valid-deref.i unknown 0 --- inspect 8.6 2.6 360 69 .66 0      error (invalid witness file) 0 --- inspect .60 .36 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0   0   error (invalid witness file) 0 --- inspect 1.2  .79 48 0   0   error (invalid witness file) 0 --- inspect .0019 .0024 .53 0   0   - --- inspect
chgrp-incomplete_true-no-overflow_false-valid-memtrack.i unknown 0 --- inspect 9.1 3.2 360 75 .66 0      error (invalid witness file) 0 --- inspect .59 .36 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0   0   error (invalid witness file) 0 --- inspect .97 .61 47 0   0   error (invalid witness file) 0 --- inspect .0019 .0023 .52 0   0   - --- inspect
basename_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (7) 0 --- inspect 170   140   2900 2000 .68 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.7 0   0  
chroot-incomplete_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 8.9 2.7 340 72 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0   0  
cut_false-unreach-call_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 8.4 2.7 350 64 .66 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 unknown 0 --- inspect 9.4 3.3 350 68 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .026 5.6 0   0  
dirname_true-no-overflow_true-valid-memsafety.i timeout 0 --- inspect 900   840   3200 11000 .70 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .024 5.6 0   0  
du_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 9.4 2.8 370 82 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.6 0   0  
echo_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 7.7 3.1 330 71 .66 .0082 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0   0  
expand_false-unreach-call_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 8.6 2.7 360 70 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .022 5.6 0   0  
fold_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 9.1 3.3 360 80 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.6 0   0  
head_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 8.3 3.1 340 72 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .025 5.6 0   0  
hostid_true-no-overflow_true-valid-memsafety.i timeout 0 --- inspect 900   800   2200 11000 .82 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .026 5.6 0   0  
logname_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 8.6 2.7 370 69 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0   0  
ls-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (7) 0 --- inspect 18   6.8 350 140 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0   0  
mkdir_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 8.8 3.3 360 69 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .026 5.6 0   0  
mkfifo-incomplete_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 8.8 2.9 350 68 .66 .012  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .036 .039 5.6 0   0  
od_false-unreach-call_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 9.4 3.4 350 80 .66 .20   - --- 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 8.8 2.9 370 79 .66 .0082 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0   0  
readlink_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 8.6 3.2 350 79 .66 .012  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.8 0   0  
realpath_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 8.7 2.9 350 63 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
rm_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 9.2 2.9 360 79 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
seq_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 8.5 3.2 360 78 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0   0  
sleep_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 8.9 3.2 360 77 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
stty_false-unreach-call_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 9.5 3.2 350 77 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .029 5.7 0   0  
sync_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 8.1 2.5 350 65 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.7 0   0  
tac_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 9.1 3.1 370 73 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .024 5.6 0   0  
tee_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 8.0 2.9 320 66 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .024 5.6 0   0  
test-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 9.3 3.5 360 80 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .024 5.6 0   0  
touch_false-unreach-call_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 9.0 3.5 320 75 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .025 5.7 0   0  
uname_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 8.6 2.6 370 67 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.5 0   0  
uniq_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 9.0 3.0 360 76 .66 .012  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.5 0   0  
usleep_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 8.6 2.6 360 78 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.7 0   0  
uudecode_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 8.8 3.3 350 72 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .025 5.6 0   0  
wc_false-unreach-call_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 8.6 3.1 340 72 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .031 .033 5.6 0   0  
who_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 8.6 3.3 350 64 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .024 5.5 0   0  
whoami-incomplete_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 8.4 2.9 360 64 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0   0  
yes_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect 8.1 3.1 320 63 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .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 0 3100 2600 24000 36000 27 .34 4 0 2.6 1.6 160 0   0   4 0 .084 .089 22 0   0   4 0 4.2 2.7 190 0   0   4 0 .014 .017 2.0 0   0   36 0 .85 .89 200 0   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
    incorrect results 0 0 0 0 0 0
        incorrect true 0 0 0 0 0 0
        incorrect false 0 0 0 0 0 0
score (40 tasks, max score: 76) 0 0 0 0 0 0
Run set uautomizer.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety cpa-seq-validate-violation-witnesses-uautomizer.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety uautomizer-validate-violation-witnesses-uautomizer.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety cpa-witness2test-validate-violation-witnesses-uautomizer.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety fshell-witness2test-validate-violation-witnesses-uautomizer.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety uautomizer-validate-correctness-witnesses-uautomizer.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety