Tool ESBMC version 6.0.0 64-bit x86_64 linux 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* [apollon004; apollon069; apollon137; apollon154] 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-06 11:03:31 CET 2018-12-08 04:49:09 CET 2018-12-08 07:45:10 CET 2018-12-08 09:00:44 CET 2018-12-12 20:28:15 CET 2018-12-08 05:09:23 CET
Run set esbmc-kind.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety cpa-seq-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety uautomizer-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety cpa-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety fshell-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety uautomizer-validate-correctness-witnesses-esbmc-kind.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety
Options -s kinduction -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/esbmc-kind.2018-12-06_1103.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/esbmc-kind.2018-12-06_1103.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/esbmc-kind.2018-12-06_1103.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/esbmc-kind.2018-12-06_1103.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/esbmc-kind.2018-12-06_1103.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) 1 wit inspect 540    540    1000 7900   .85 0   true -32 wit inspect 7.1  3.8  270 0   0   true -32 --- inspect 13     7.8   510   .62 0   unknown 0 --- inspect 5.5  3.0  270 0   0   false(valid-deref) 1 --- inspect .82   .83   21    .21 1.7 - --- inspect
head_false-valid-deref.i out of memory 0 --- inspect 22    21    15000 260   .93 0   error (invalid witness file) 0 --- inspect .58 .35 41 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .91 .58 47 0   0   error (invalid witness file) 0 --- inspect .0047 .0061 .40 0    0   - --- inspect
sleep_false-valid-deref.i unknown 0 --- inspect .22 .22 32 3.2 .85 0   error (invalid witness file) 0 --- inspect .74 .46 41 0   0   error (2) 0 --- inspect .021 .022 5.7 0    0   error (invalid witness file) 0 --- inspect .94 .60 48 0   0   error (invalid witness file) 0 --- inspect .0054 .0064 .39 0    0   - --- inspect
chgrp-incomplete_true-no-overflow_false-valid-memtrack.i unknown 0 --- inspect .20 .20 30 2.5 .85 0   error (invalid witness file) 0 --- inspect .71 .43 41 0   0   error (2) 0 --- inspect .020 .031 5.7 0    0   error (invalid witness file) 0 --- inspect .98 .63 48 0   0   error (invalid witness file) 0 --- inspect .0019 .0025 .53 0    0   - --- inspect
basename_false-unreach-call_true-no-overflow_true-valid-memsafety.i timeout 0 --- inspect 900    900    1100 11000   1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
chroot-incomplete_true-no-overflow_true-valid-memsafety.i timeout 0 --- inspect 900    900    4400 7900   .86 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 out of memory 0 --- inspect 22    22    15000 230   1.1  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .026 5.6 0   0  
date_false-unreach-call_true-no-overflow_true-valid-memsafety.i out of memory 0 --- inspect 22    21    15000 270   1.1  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.7 0   0  
dirname_true-no-overflow_true-valid-memsafety.i timeout 0 --- inspect 900    900    4400 11000   .86 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
du_true-no-overflow_true-valid-memsafety.i out of memory 0 --- inspect 22    21    15000 320   .94 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .026 5.6 0   0  
echo_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect .23 .23 32 2.8 1.0  0   - --- 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 out of memory 0 --- inspect 22    21    15000 280   .98 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .023 5.6 0   0  
fold_true-no-overflow_true-valid-memsafety.i out of memory 0 --- inspect 22    21    15000 280   .93 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .025 5.6 0   0  
head_true-no-overflow_true-valid-memsafety.i out of memory 0 --- inspect 22    22    15000 260   1.1  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.7 0   0  
hostid_true-no-overflow_true-valid-memsafety.i timeout 0 --- inspect 900    900    1600 9200   .86 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .028 .028 5.6 0   0  
logname_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect .19 .19 30 2.7 .85 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.7 0   0  
ls-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i out of memory 0 --- inspect 22    21    15000 260   .93 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .022 5.6 0   0  
mkdir_true-no-overflow_true-valid-memsafety.i out of memory 0 --- inspect 22    21    15000 300   1.1  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 .19 .19 30 2.7 1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0   0  
od_false-unreach-call_true-no-overflow_true-valid-memsafety.i out of memory 0 --- inspect 22    22    15000 280   .94 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .025 5.6 0   0  
printf_false-unreach-call_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect .24 .24 36 3.0 1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0   0  
readlink_true-no-overflow_true-valid-memsafety.i out of memory 0 --- inspect 22    21    15000 290   .93 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .024 5.7 0   0  
realpath_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect .22 .22 31 2.2 1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .027 5.6 0   0  
rm_true-no-overflow_true-valid-memsafety.i out of memory 0 --- inspect 22    21    15000 260   1.1  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0   0  
seq_true-no-overflow_true-valid-memsafety.i out of memory 0 --- inspect 22    21    15000 260   1.1  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.7 0   0  
sleep_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect .23 .23 32 2.6 .85 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .029 .030 5.6 0   0  
stty_false-unreach-call_true-no-overflow_true-valid-memsafety.i out of memory 0 --- inspect 22    21    15000 310   1.1  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0   0  
sync_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect .19 .19 30 2.7 1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .026 5.7 0   0  
tac_true-no-overflow_true-valid-memsafety.i out of memory 0 --- inspect 22    21    15000 300   1.1  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .022 5.6 0   0  
tee_true-no-overflow_true-valid-memsafety.i out of memory 0 --- inspect 22    21    15000 320   1.1  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .023 5.6 0   0  
test-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect .24 .24 37 2.8 1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
touch_false-unreach-call_true-no-overflow_true-valid-memsafety.i out of memory 0 --- inspect 22    21    15000 290   .92 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.6 0   0  
uname_true-no-overflow_true-valid-memsafety.i out of memory 0 --- inspect 22    21    15000 300   .93 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.7 0   0  
uniq_true-no-overflow_true-valid-memsafety.i out of memory 0 --- inspect 22    21    15000 290   1.1  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0   0  
usleep_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect .23 .23 31 2.3 1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.6 0   0  
uudecode_true-no-overflow_true-valid-memsafety.i out of memory 0 --- inspect 22    21    15000 290   .93 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.7 0   0  
wc_false-unreach-call_true-no-overflow_true-valid-memsafety.i out of memory 0 --- inspect 22    21    15000 240   1.1  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.6 0   0  
who_true-no-overflow_true-valid-memsafety.i out of memory 0 --- inspect 23    23    15000 350   1.1  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .026 5.7 0   0  
whoami-incomplete_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect .20 .20 31 2.3 1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .025 5.6 0   0  
yes_true-no-overflow_true-valid-memsafety.i unknown 0 --- inspect .21 .21 30 2.5 .85 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 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 1 4600 4600 340000 53000 39    0   4 -32 9.2 5.0 390 0   0   4 -32 13 7.9 530 .62 0   4 0 8.3 4.8 410 0   0   4 1 .83 .84 22 .21 1.7 36 0 .84 .87 200 0   0  
    correct results 1 1 540 540 1000 7900 .85 0   0 0 0 1 1 .82 .83 21 .21 1.7 0
        correct true 0 0 0 0 0 0
        correct false 1 1 540 540 1000 7900 .85 0   0 0 0 1 1 .82 .83 21 .21 1.7 0
    incorrect results 0 1 -32 7.1 3.8 270 0   0   1 -32 13 7.8 510 .62 0   0 0 0
        incorrect true 0 1 -32 7.1 3.8 270 0   0   1 -32 13 7.8 510 .62 0   0 0 0
        incorrect false 0 0 0 0 0 0
score (40 tasks, max score: 76) 1 -32 -32 0 1 0
Run set esbmc-kind.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety cpa-seq-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety uautomizer-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety cpa-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety fshell-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety uautomizer-validate-correctness-witnesses-esbmc-kind.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety