Tool symbiotic 6.0.3-77d4af47 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* [apollon013; apollon098] 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-07 21:42:05 CET 2018-12-08 23:40:56 CET 2018-12-09 00:46:04 CET 2018-12-09 01:29:54 CET 2018-12-12 21:10:03 CET 2018-12-08 23:47:25 CET
Run set symbiotic.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety cpa-seq-validate-violation-witnesses-symbiotic.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety uautomizer-validate-violation-witnesses-symbiotic.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety cpa-witness2test-validate-violation-witnesses-symbiotic.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety fshell-witness2test-validate-violation-witnesses-symbiotic.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety uautomizer-validate-correctness-witnesses-symbiotic.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety
Options --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/symbiotic.2018-12-07_2142.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/symbiotic.2018-12-07_2142.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/symbiotic.2018-12-07_2142.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/symbiotic.2018-12-07_2142.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/symbiotic.2018-12-07_2142.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 .65 .64 23 8.6 0     0     false(valid-deref) 1 wit inspect 5.9  3.2  270 0   0   true -32 --- inspect 15     8.9   490   .62 0   timeout 0 --- inspect 5.8  130    270 .029 .16 false(valid-deref) 1 --- inspect .84   .86   20    .21  1.8 - --- inspect
head_false-valid-deref.i error(unknown, slicing-finished) 0 --- inspect 1.8  1.8  96 19   0     .012 error (invalid witness file) 0 --- inspect .60 .41 41 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .95 .63 49 0     0    error (invalid witness file) 0 --- inspect .0019 .0027 .41 0     0   - --- inspect
sleep_false-valid-deref.i error(returned 1, instr-finished) 0 --- inspect .38 .37 21 3.7 0     .012 error (invalid witness file) 0 --- inspect .72 .45 41 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .93 .61 47 0     0    error (invalid witness file) 0 --- inspect .0018 .0022 .52 0     0   - --- inspect
chgrp-incomplete_true-no-overflow_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 1.2  1.2  22 14   0     0     error 0 wit inspect 8.6  4.5  270 0   0   unknown 0 --- inspect 7.6   4.3   290   .62 0   error 0 --- inspect 6.1  3.3  270 0     0    error (1) 0 --- inspect .58   .58   20    .074 0   - --- inspect
basename_false-unreach-call_true-no-overflow_true-valid-memsafety.i timeout (verification) 0 --- inspect 900    900    470 9300   .025 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .027 5.6 0   0  
chroot-incomplete_true-no-overflow_true-valid-memsafety.i timeout (verification) 0 --- inspect 900    900    68 14000   .012 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .024 5.7 0   0  
cut_false-unreach-call_true-no-overflow_true-valid-memsafety.i error(unknown, slicing-finished) 0 --- inspect 14    14    180 120   0     .012 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0   0  
date_false-unreach-call_true-no-overflow_true-valid-memsafety.i error(unknown, slicing-finished) 0 --- inspect 16    16    330 170   0     .012 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.6 0   0  
dirname_true-no-overflow_true-valid-memsafety.i error(unknown, cex-confirmation) 0 --- inspect .65 .64 27 8.1 0     0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
du_true-no-overflow_true-valid-memsafety.i error(unknown, slicing-finished) 0 --- inspect 41    41    210 440   0     0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .022 5.6 0   0  
echo_true-no-overflow_true-valid-memsafety.i timeout (verification) 0 --- inspect 900    900    680 7900   .025 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .022 5.6 0   0  
expand_false-unreach-call_true-no-overflow_true-valid-memsafety.i error(unknown, slicing-finished) 0 --- inspect 25    25    270 220   0     .025 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .024 5.6 0   0  
fold_true-no-overflow_true-valid-memsafety.i error(unknown, slicing-finished) 0 --- inspect 8.9  8.9  170 77   0     .012 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0   0  
head_true-no-overflow_true-valid-memsafety.i error(unknown, slicing-finished) 0 --- inspect 1.8  1.7  97 19   0     .012 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .026 5.7 0   0  
hostid_true-no-overflow_true-valid-memsafety.i timeout (verification) 0 --- inspect 900    900    2000 13000   .025 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
logname_true-no-overflow_true-valid-memsafety.i error(unknown, cex-confirmation) 0 --- inspect .67 .65 24 8.2 0     0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0   0  
ls-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i error(unknown, slicing-finished) 0 --- inspect 210    210    1000 1900   0     .012 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
mkdir_true-no-overflow_true-valid-memsafety.i error(unknown, slicing-finished) 0 --- inspect 14    14    180 120   0     .012 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
mkfifo-incomplete_true-no-overflow_true-valid-memsafety.i timeout (verification) 0 --- inspect 900    900    64 11000   .012 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .023 5.6 0   0  
od_false-unreach-call_true-no-overflow_true-valid-memsafety.i error(unknown, slicing-finished) 0 --- inspect 90    90    860 670   0     .012 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .026 5.6 0   0  
printf_false-unreach-call_true-no-overflow_true-valid-memsafety.i error(returned 1, instr-finished) 0 --- inspect 2.5  2.5  110 29   0     .012 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0   0  
readlink_true-no-overflow_true-valid-memsafety.i error(unknown, slicing-finished) 0 --- inspect 5.6  5.6  95 66   0     .012 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0   0  
realpath_true-no-overflow_true-valid-memsafety.i timeout (verification) 0 --- inspect 900    900    76 11000   .012 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .027 5.6 0   0  
rm_true-no-overflow_true-valid-memsafety.i error(unknown, slicing-finished) 0 --- inspect 44    44    210 450   0     .012 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0   0  
seq_true-no-overflow_true-valid-memsafety.i error(returned 1, instr-finished) 0 --- inspect 4.5  4.5  83 53   0     .012 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
sleep_true-no-overflow_true-valid-memsafety.i error(returned 1, instr-finished) 0 --- inspect .35 .34 21 3.5 0     .012 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .024 5.5 0   0  
stty_false-unreach-call_true-no-overflow_true-valid-memsafety.i timeout (instrumentation) 0 --- inspect 900    900    520 12000   .012 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0   0  
sync_true-no-overflow_true-valid-memsafety.i timeout (verification) 0 --- inspect 900    900    160 8300   .025 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .022 5.6 0   0  
tac_true-no-overflow_true-valid-memsafety.i error(unknown, slicing-finished) 0 --- inspect 7.1  7.1  110 86   0     .16  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .025 5.6 0   0  
tee_true-no-overflow_true-valid-memsafety.i error(unknown, slicing-finished) 0 --- inspect 6.2  6.2  110 66   0     .012 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.7 0   0  
test-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i error(unknown, slicing-finished) 0 --- inspect 2.7  2.7  87 21   0     0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .025 5.6 0   0  
touch_false-unreach-call_true-no-overflow_true-valid-memsafety.i error(unknown, slicing-finished) 0 --- inspect 11    11    270 100   0     .16  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.7 0   0  
uname_true-no-overflow_true-valid-memsafety.i error(unknown, slicing-finished) 0 --- inspect 5.7  5.7  110 54   0     4.9   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0   0  
uniq_true-no-overflow_true-valid-memsafety.i error(unknown, slicing-finished) 0 --- inspect 9.7  9.7  140 110   0     .012 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .026 5.6 0   0  
usleep_true-no-overflow_true-valid-memsafety.i timeout (verification) 0 --- inspect 900    900    180 8000   .012 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0   0  
uudecode_true-no-overflow_true-valid-memsafety.i error(unknown, slicing-finished) 0 --- inspect 22    22    250 180   0     .012 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.7 0   0  
wc_false-unreach-call_true-no-overflow_true-valid-memsafety.i error(unknown, slicing-finished) 0 --- inspect 7.9  7.9  130 68   0     .012 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0   0  
who_true-no-overflow_true-valid-memsafety.i error(unknown, slicing-finished) 0 --- inspect 5.9  5.9  100 58   0     0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .039 .040 5.5 0   0  
whoami-incomplete_true-no-overflow_true-valid-memsafety.i timeout (verification) 0 --- inspect 900    900    150 8700   .016 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.8 0   0  
yes_true-no-overflow_true-valid-memsafety.i timeout (verification) 0 --- inspect 900    900    110 11000   .012 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 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 10000    10000    9900 120000   .19 5.5 4 1 16   8.5 620 0   0   4 -32 23 13   790 1.2  0   4 0 14 130 630 .029 .16 4 1 1.4  1.4  42 .28 1.8 36 0 .85 .88 200 0   0  
    correct results 1 1 .65 .64 23 8.6 0    0   1 1 5.9 3.2 270 0   0   0 0 1 1 .84 .86 20 .21 1.8 0
        correct true 0 0 0 0 0 0
        correct false 1 1 .65 .64 23 8.6 0    0   1 1 5.9 3.2 270 0   0   0 0 1 1 .84 .86 20 .21 1.8 0
    correct-unconfimed results 1 0 1.2  1.2  22 14   0    0   0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0
        correct-unconfirmed false 1 0 1.2  1.2  22 14   0    0   0 0 0 0 0
    incorrect results 0 0 1 -32 15 8.9 490 .62 0   0 0 0
        incorrect true 0 0 1 -32 15 8.9 490 .62 0   0 0 0
        incorrect false 0 0 0 0 0 0
score (40 tasks, max score: 76) 1 1 -32 0 1 0
Run set symbiotic.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety cpa-seq-validate-violation-witnesses-symbiotic.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety uautomizer-validate-violation-witnesses-symbiotic.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety cpa-witness2test-validate-violation-witnesses-symbiotic.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety fshell-witness2test-validate-violation-witnesses-symbiotic.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety uautomizer-validate-correctness-witnesses-symbiotic.sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety