Tool 2LS 0.6.0 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-01 08:19:20 CET 2017-12-01 08:41:15 CET 2017-12-01 08:58:15 CET 2017-12-01 08:59:36 CET 2017-12-01 08:42:37 CET
Run set 2ls.sv-comp18.Systems_BusyBox_MemSafety cpa-seq-validate-violation-witnesses-2ls.sv-comp18-violation-witness.Systems_BusyBox_MemSafety uautomizer-validate-violation-witnesses-2ls.sv-comp18-violation-witness.Systems_BusyBox_MemSafety fshell-witness2test-validate-violation-witnesses-2ls.sv-comp18-violation-witness.Systems_BusyBox_MemSafety uautomizer-validate-correctness-witnesses-2ls.sv-comp18-correctness-witness.Systems_BusyBox_MemSafety
Options --graphml-witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/2ls.2017-12-01_0819.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/2ls.2017-12-01_0819.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/2ls.2017-12-01_0819.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/2ls.2017-12-01_0819.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 error (134) 0 wit inspect .31 32 2.8 error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect
head_false-valid-deref.i error (6) 0 wit inspect .41 41 4.5 error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0036 .30 - wit inspect
sleep_false-valid-deref.i error (134) 0 wit inspect 2.3  39 24   error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .0012 .34 - wit inspect
chgrp-incomplete_true-no-overflow_false-valid-memtrack.i error (134) 0 wit inspect .47 37 4.6 error (invalid witness file) 0 wit inspect .58 45 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect
basename_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect .31 32 2.6 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .038 4.9
chroot-incomplete_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect 1.4  38 12   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
cut_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect 35    87 470   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
date_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (6) 0 wit inspect .50 46 3.9 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .049 5.0
dirname_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect .27 31 3.0 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
du_true-no-overflow_true-valid-memsafety.i error (5) 0 wit inspect 18    69 200   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
echo_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect 1.1  38 12   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
expand_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect 120    130 850   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
fold_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect 14    62 170   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.9
hostid_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect .26 34 2.4 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
logname_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect .45 37 3.9 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .025 4.8
ls-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900    340 5500   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
mkdir_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect 6.5  45 70   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .045 4.9
mkfifo-incomplete_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect .44 35 3.5 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.9
od_false-unreach-call_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900    630 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
printf_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (6) 0 wit inspect .56 45 5.2 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .035 4.9
readlink_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect 6.5  43 78   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .048 5.0
realpath_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect .48 37 5.1 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
rm_true-no-overflow_true-valid-memsafety.i error (5) 0 wit inspect 16    68 170   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .045 4.8
seq_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect 4.1  40 52   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
stty_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect 250    210 2300   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .026 4.8
sync_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect .37 35 3.8 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .046 4.8
tac_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect 13    58 140   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.8
tee_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect 8.4  49 95   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
test-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (5) 0 wit inspect 98    130 880   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .038 4.8
touch_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect 16    67 170   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 5.0
uname_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect 4.1  41 37   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .049 4.8
uniq_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect 13    57 150   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .017 5.0
usleep_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect .81 37 9.6 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
uudecode_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect 28    81 300   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.8
wc_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (6) 0 wit inspect .38 41 3.4 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
who_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect 4.7  41 43   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .035 5.0
whoami-incomplete_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect .47 37 3.9 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .036 4.8
yes_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect .44 37 4.3 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.9
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 0 2500 3000 23000 4 0 2.2 180 4 0 .079 19 4 0 .0074 1.2 34 0 .93 170
    correct results 0 0 0 0 0
        correct true 0 0 0 0 0
        correct false 0 0 0 0 0
    incorrect results 0 0 0 0 0
        incorrect true 0 0 0 0 0
        incorrect false 0 0 0 0 0
score (38 tasks, max score: 72) 0 0 0 0 0
Run set 2ls.sv-comp18.Systems_BusyBox_MemSafety cpa-seq-validate-violation-witnesses-2ls.sv-comp18-violation-witness.Systems_BusyBox_MemSafety uautomizer-validate-violation-witnesses-2ls.sv-comp18-violation-witness.Systems_BusyBox_MemSafety fshell-witness2test-validate-violation-witnesses-2ls.sv-comp18-violation-witness.Systems_BusyBox_MemSafety uautomizer-validate-correctness-witnesses-2ls.sv-comp18-correctness-witness.Systems_BusyBox_MemSafety