Tool CBMC 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-04 22:48:40 CET 2018-12-06 08:59:15 CET 2018-12-06 10:10:50 CET 2018-12-06 10:22:39 CET 2018-12-12 19:29:48 CET 2018-12-06 09:23:57 CET
Run set cbmc.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety cpa-seq-validate-violation-witnesses-cbmc.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety uautomizer-validate-violation-witnesses-cbmc.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety cpa-witness2test-validate-violation-witnesses-cbmc.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety fshell-witness2test-validate-violation-witnesses-cbmc.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety uautomizer-validate-correctness-witnesses-cbmc.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety
Options --graphml-witness witness.graphml -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/cbmc.2018-12-04_2248.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cbmc.2018-12-04_2248.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/cbmc.2018-12-04_2248.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/cbmc.2018-12-04_2248.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cbmc.2018-12-04_2248.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 12    12    770 130   .57  0      error 0 wit inspect 7.4  3.9  280 0   0   true -32 --- inspect 15     8.1   560   .62 0   error 0 --- inspect 5.6  3.1  280 0   0   error (2) 0 --- inspect .78   .78   21    .090 0   - --- inspect
head_false-valid-deref.i error (134) 0 --- inspect 3.5  3.5  53 50   .025 0      error (invalid witness file) 0 --- inspect .64 .40 41 0   0   error (2) 0 --- inspect .022 .024 5.7 0    0   error (invalid witness file) 0 --- inspect .93 .61 47 0   0   error (invalid witness file) 0 --- inspect .0044 .0055 .41 0     0   - --- inspect
sleep_false-valid-deref.i error (134) 0 --- inspect .88 .88 27 11   .016 0      error (invalid witness file) 0 --- inspect .73 .46 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .98 .63 46 0   0   error (invalid witness file) 0 --- inspect .0043 .0055 .53 0     0   - --- inspect
chgrp-incomplete_true-no-overflow_false-valid-memtrack.i error (134) 0 --- inspect .29 .29 13 3.5 .016 0      error (invalid witness file) 0 --- inspect .58 .37 41 0   0   error (2) 0 --- inspect .022 .023 5.7 0    0   error (invalid witness file) 0 --- inspect .99 .63 48 0   0   error (invalid witness file) 0 --- inspect .0047 .0063 .53 0     0   - --- inspect
basename_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (42) 0 --- inspect 880    880    6400 9800   24     0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.7 0   0  
chroot-incomplete_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect .39 .39 16 4.9 .020 .045  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
cut_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect 7.1  7.1  84 87   .025 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .029 5.7 0   0  
date_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect 3.0  3.0  130 40   .025 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
dirname_true-no-overflow_true-valid-memsafety.i out of memory 0 --- inspect 590    590    13000 6700   6.4   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .027 5.5 0   0  
du_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect 62    62    220 710   .020 .61   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .022 5.6 0   0  
echo_true-no-overflow_true-valid-memsafety.i error (42) 0 --- inspect 880    880    7200 7200   4.8   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.8 0   0  
expand_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect 34    34    210 460   .029 .045  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
fold_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect 3.7  3.7  50 49   .025 .053  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .025 5.6 0   0  
head_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect 3.5  3.5  54 44   .025 .12   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.7 0   0  
hostid_true-no-overflow_true-valid-memsafety.i out of memory 0 --- inspect 570    570    13000 6600   5.8   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
logname_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect .25 .25 14 3.7 .016 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.7 0   0  
ls-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect 3.6  3.6  55 45   .037 .18   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .028 .030 5.6 0   0  
mkdir_true-no-overflow_true-valid-memsafety.i error 0 --- inspect 880    880    1100 3300   .094 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .028 .029 5.6 0   0  
mkfifo-incomplete_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect .28 .28 14 3.9 .016 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .029 5.6 0   0  
od_false-unreach-call_true-no-overflow_true-valid-memsafety.i error 0 --- inspect 880    880    670 4700   .11  0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .029 .029 5.6 0   0  
printf_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect 23    23    110 290   .025 .17   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .023 5.6 0   0  
readlink_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect .82 .82 27 13   .020 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0   0  
realpath_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect .30 .29 14 5.4 .016 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0   0  
rm_true-no-overflow_true-valid-memsafety.i error 0 --- inspect 880    880    270 12000   .098 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .028 .028 5.6 0   0  
seq_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect .71 .71 21 10   .020 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
sleep_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect .90 .90 27 12   .016 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .030 .031 5.5 0   0  
stty_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect 66    66    180 800   .033 .36   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .024 5.6 0   0  
sync_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect .21 .21 11 2.6 .016 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .028 .029 5.7 0   0  
tac_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect 2.6  2.6  44 35   .020 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .027 5.5 0   0  
tee_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect 1.2  1.2  32 15   .025 .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .025 5.7 0   0  
test-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i error 0 --- inspect 880    880    690 5900   .094 .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0   0  
touch_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect 2.8  2.8  110 36   .025 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .026 5.6 0   0  
uname_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect 1.1  1.1  120 16   .020 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .026 5.5 0   0  
uniq_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect 2.0  2.0  39 25   .025 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.6 0   0  
usleep_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect .25 .25 13 3.5 .016 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .028 5.7 0   0  
uudecode_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect 6.1  6.1  85 69   .025 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
wc_false-unreach-call_true-no-overflow_true-valid-memsafety.i error 0 --- inspect 880    880    580 6000   .098 .045  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0   0  
who_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect .78 .78 27 12   .020 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.7 0   0  
whoami-incomplete_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect .22 .22 12 3.3 .016 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0   0  
yes_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect .24 .24 12 3.1 .016 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.7 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 7500 7500 46000 66000 42    1.6 4 0 9.4 5.1 400 0   0   4 -32 15 8.2 580 .62 0   4 0 8.5 4.9 420 0   0   4 0 .79 .80 23 .090 0   36 0 .88 .92 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
    correct-unconfimed results 1 0 12 12 770 130 .57 0   0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0
        correct-unconfirmed false 1 0 12 12 770 130 .57 0   0 0 0 0 0
    incorrect results 0 0 1 -32 15 8.1 560 .62 0   0 0 0
        incorrect true 0 0 1 -32 15 8.1 560 .62 0   0 0 0
        incorrect false 0 0 0 0 0 0
score (40 tasks, max score: 76) 0 0 -32 0 0 0
Run set cbmc.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety cpa-seq-validate-violation-witnesses-cbmc.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety uautomizer-validate-violation-witnesses-cbmc.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety cpa-witness2test-validate-violation-witnesses-cbmc.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety fshell-witness2test-validate-violation-witnesses-cbmc.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety uautomizer-validate-correctness-witnesses-cbmc.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety