Tool CBMC Path 5.10 () 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:45:10 CET 2018-12-06 08:53:36 CET 2018-12-06 10:12:52 CET 2018-12-06 10:22:39 CET 2018-12-12 19:23:37 CET 2018-12-06 09:28:06 CET
Run set cbmc-path.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety cpa-seq-validate-violation-witnesses-cbmc-path.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety uautomizer-validate-violation-witnesses-cbmc-path.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety cpa-witness2test-validate-violation-witnesses-cbmc-path.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety fshell-witness2test-validate-violation-witnesses-cbmc-path.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety uautomizer-validate-correctness-witnesses-cbmc-path.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-path.2018-12-04_2245.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cbmc-path.2018-12-04_2245.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-path.2018-12-04_2245.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/cbmc-path.2018-12-04_2245.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cbmc-path.2018-12-04_2245.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 error (134) 0 --- inspect 28    28    340 340   24     0      error (invalid witness file) 0 --- inspect .77 .47 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0   error (invalid witness file) 0 --- inspect .94 .60 47 0   0   error (invalid witness file) 0 --- inspect .0045 .0056 .41 0   0   - --- inspect
head_false-valid-deref.i error (134) 0 --- inspect .76 .76 29 10   .56  0      error (invalid witness file) 0 --- inspect .63 .40 40 0   0   error (2) 0 --- inspect .024 .025 5.6 0   0   error (invalid witness file) 0 --- inspect .99 .65 49 0   0   error (invalid witness file) 0 --- inspect .0059 .0085 .40 0   0   - --- inspect
sleep_false-valid-deref.i error (134) 0 --- inspect .63 .63 27 8.5 .43  0      error (invalid witness file) 0 --- inspect .60 .38 42 0   0   error (2) 0 --- inspect .024 .024 5.7 0   0   error (invalid witness file) 0 --- inspect .97 .64 47 0   0   error (invalid witness file) 0 --- inspect .0060 .0077 .41 0   0   - --- inspect
chgrp-incomplete_true-no-overflow_false-valid-memtrack.i error (134) 0 --- inspect .39 .39 20 5.7 .24  0      error (invalid witness file) 0 --- inspect .77 .48 41 0   0   error (2) 0 --- inspect .026 .026 5.6 0   0   error (invalid witness file) 0 --- inspect .92 .61 47 0   0   error (invalid witness file) 0 --- inspect .0055 .0069 .53 0   0   - --- inspect
basename_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect 21    21    290 320   22     0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0   0  
chroot-incomplete_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect .43 .43 23 6.5 .24  .32   - --- 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 error (134) 0 --- inspect 1.3  1.3  47 16   1.4   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .029 .030 5.7 0   0  
date_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect 2.8  2.8  79 39   4.2   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .027 5.6 0   0  
dirname_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect 1.1  1.1  32 15   1.2   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
du_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect .70 .70 40 8.4 4.1   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .026 5.5 0   0  
echo_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect .50 .49 22 7.1 .34  0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .019 .020 5.6 0   0  
expand_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect .51 .51 29 6.9 .15  0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.7 0   0  
fold_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect .45 .45 26 5.6 .14  .18   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .041 .043 5.6 0   0  
head_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect .74 .74 27 9.3 .59  0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .022 5.6 0   0  
hostid_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect .26 .26 16 3.1 .11  0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .022 5.6 0   0  
logname_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect .30 .30 19 2.9 .11  0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .024 5.6 0   0  
ls-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect 1.1  1.1  58 13   5.1   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0   0  
mkdir_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect 2.4  2.4  64 31   3.2   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
mkfifo-incomplete_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect .22 .22 17 2.6 .041 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .023 5.6 0   0  
od_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect 3.1  3.1  90 42   4.5   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.6 0   0  
printf_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect .46 .45 25 4.9 .086 .041  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0   0  
readlink_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect 1.9  1.9  53 25   2.3   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
realpath_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect .38 .38 20 4.7 .23  0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .024 5.7 0   0  
rm_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect 1.2  1.2  45 17   1.2   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .025 5.6 0   0  
seq_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect 1.1  1.1  41 12   1.0   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .034 5.5 0   0  
sleep_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect .67 .67 26 9.8 .44  0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.6 0   0  
stty_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect 1.3  1.3  63 18   18     .45   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
sync_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect .37 .37 21 4.6 .20  0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.6 0   0  
tac_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect 1.0  1.0  40 15   .89  0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0   0  
tee_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect 1.1  1.1  46 14   .99  0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0   0  
test-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect .99 .99 35 15   .68  .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0   0  
touch_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect 2.5  2.5  69 31   3.4   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
uname_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect 2.3  2.3  62 29   3.1   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0   0  
uniq_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect 1.2  1.2  43 15   1.2   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
usleep_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect .73 .72 26 9.2 .55  0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .027 5.6 0   0  
uudecode_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect 2.0  2.0  58 29   2.2   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .025 5.5 0   0  
wc_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect .45 .44 25 6.2 .15  .19   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.7 0   0  
who_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect 1.7  1.7  50 21   2.0   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0   0  
whoami-incomplete_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect .33 .33 19 3.2 .11  0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .024 5.6 0   0  
yes_true-no-overflow_true-valid-memsafety.i error (134) 0 --- inspect .30 .30 19 3.9 .11  0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .024 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 88 88 2100 1200 110 1.2 4 0 2.8 1.7 160 0   0   4 0 .094 .096 23 0   0   4 0 3.8 2.5 190 0   0   4 0 .022 .029 1.7 0   0   36 0 .86 .90 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 cbmc-path.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety cpa-seq-validate-violation-witnesses-cbmc-path.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety uautomizer-validate-violation-witnesses-cbmc-path.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety cpa-witness2test-validate-violation-witnesses-cbmc-path.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety fshell-witness2test-validate-violation-witnesses-cbmc-path.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety uautomizer-validate-correctness-witnesses-cbmc-path.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety