Tool symbiotic 5.0.0-KLEE:1faddfe0-dg:12c34aac-symbiotic:5e14b94d-minisat:3db58943-llvm-instrumentation:cd767593-stp:17249213 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741 CProver witness2test 0.1 ULTIMATE Automizer 0.1.23-3204b741
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.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-12-02 23:08:57 CET 2017-12-03 00:45:11 CET 2017-12-03 01:25:52 CET 2017-12-03 01:32:11 CET 2017-12-03 00:52:42 CET
Run set symbiotic.sv-comp18.Systems_BusyBox_MemSafety cpa-seq-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.Systems_BusyBox_MemSafety uautomizer-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.Systems_BusyBox_MemSafety fshell-witness2test-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.Systems_BusyBox_MemSafety uautomizer-validate-correctness-witnesses-symbiotic.sv-comp18-correctness-witness.Systems_BusyBox_MemSafety
Options --witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/symbiotic.2017-12-02_2308.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -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 --full-output --validate ../../results-verified/symbiotic.2017-12-02_2308.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/symbiotic.2017-12-02_2308.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/symbiotic.2017-12-02_2308.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/busybox-1.22.0/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
basename_false-valid-deref.i false(valid-deref) 1 wit inspect 2.0  310 23   false(valid-deref) 1 wit inspect 5.9  260 error (7) 0 wit inspect 10     210   false(valid-deref) 1 wit inspect .95   30    - wit inspect
head_false-valid-deref.i error 0 wit inspect 18    3200 200   error (invalid witness file) 0 wit inspect .60 44 error (2) 0 wit inspect .023 5.0 error (invalid witness file) 0 wit inspect .0016 .28 - wit inspect
sleep_false-valid-deref.i error (1) 0 wit inspect .22 12 2.8 error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .024 4.9 error (invalid witness file) 0 wit inspect .0017 .27 - wit inspect
chgrp-incomplete_true-no-overflow_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 2.5  410 30   error 0 wit inspect 6.2  260 true -32 wit inspect 12     360   error (1) 0 wit inspect .77   19    - wit inspect
basename_false-unreach-call_true-no-overflow_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    560 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
chroot-incomplete_true-no-overflow_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900 13000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
cut_false-unreach-call_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 42    6300 530   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
date_false-unreach-call_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 130    13000 1400   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
dirname_true-no-overflow_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    2300 10000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
du_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 45    6100 500   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
echo_true-no-overflow_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    1500 10000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.8
expand_false-unreach-call_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 180    11000 2300   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
fold_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 79    4900 840   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
hostid_true-no-overflow_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    2300 12000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
logname_true-no-overflow_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    500 13000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
ls-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    320 10000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 5.0
mkdir_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 30    4300 380   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .025 4.8
mkfifo-incomplete_true-no-overflow_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    1400 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .026 4.8
od_false-unreach-call_true-no-overflow_true-valid-memsafety.i out of memory 0 wit inspect 150    15000 1800   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
printf_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (1) 0 wit inspect .26 13 2.5 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .049 5.0
readlink_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 27    3900 360   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
realpath_true-no-overflow_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    1500 9400   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
rm_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 40    5600 510   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
seq_true-no-overflow_true-valid-memsafety.i error (1) 0 wit inspect .24 13 2.5 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.8
stty_false-unreach-call_true-no-overflow_true-valid-memsafety.i out of memory 0 wit inspect 51    15000 740   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
sync_true-no-overflow_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    360 12000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.8
tac_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 27    3800 320   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
tee_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 29    4000 410   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
test-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 12    2300 140   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
touch_false-unreach-call_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 68    9300 800   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.9
uname_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 23    3500 250   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
uniq_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 35    5000 510   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
usleep_true-no-overflow_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    930 13000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
uudecode_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 74    10000 880   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
wc_false-unreach-call_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 30    4400 340   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
who_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 27    3900 370   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.9
whoami-incomplete_true-no-overflow_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    2400 10000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .049 4.8
yes_true-no-overflow_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    670 14000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.8
sv-benchmarks/c/busybox-1.22.0/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
total 38 1 13000   150000 160000 4 1 13   610 4 -32 23 580 4 1 1.7  50 34 0 .77 170
    correct results 1 1 2.0 310 23 1 1 5.9 260 0 1 1 .95 30 0
        correct true 0 0 0 0 0
        correct false 1 1 2.0 310 23 1 1 5.9 260 0 1 1 .95 30 0
    correct-unconfimed results 1 0 2.5 410 30 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0
        correct-unconfirmed false 1 0 2.5 410 30 0 0 0 0
    incorrect results 0 0 1 -32 12 360 0 0
        incorrect true 0 0 1 -32 12 360 0 0
        incorrect false 0 0 0 0 0
score (38 tasks, max score: 72) 1 1 -32 1 0
Run set symbiotic.sv-comp18.Systems_BusyBox_MemSafety cpa-seq-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.Systems_BusyBox_MemSafety uautomizer-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.Systems_BusyBox_MemSafety fshell-witness2test-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.Systems_BusyBox_MemSafety uautomizer-validate-correctness-witnesses-symbiotic.sv-comp18-correctness-witness.Systems_BusyBox_MemSafety