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* [apollon013; apollon077; apollon078; apollon114] [apollon077; apollon078; apollon089; apollon164] [apollon077; apollon078; apollon089; apollon134] [apollon022; apollon077; apollon078]
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] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [4; 8], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33554 MB; 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 10:20:37 CET 2017-12-01 11:18:40 CET 2017-12-01 11:36:11 CET 2017-12-01 11:38:17 CET 2017-12-01 11:21:10 CET
Run set 2ls.sv-comp18.Systems_BusyBox_NoOverflows cpa-seq-validate-violation-witnesses-2ls.sv-comp18-violation-witness.Systems_BusyBox_NoOverflows uautomizer-validate-violation-witnesses-2ls.sv-comp18-violation-witness.Systems_BusyBox_NoOverflows fshell-witness2test-validate-violation-witnesses-2ls.sv-comp18-violation-witness.Systems_BusyBox_NoOverflows uautomizer-validate-correctness-witnesses-2ls.sv-comp18-correctness-witness.Systems_BusyBox_NoOverflows
Options --graphml-witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/2ls.2017-12-01_1020.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_1020.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/2ls.2017-12-01_1020.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/2ls.2017-12-01_1020.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
chgrp-incomplete_false-no-overflow.i error (134) 0 wit inspect .32 37 3.0 error (invalid witness file) 0 wit inspect .41 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0015 .33 - wit inspect
chroot-incomplete_false-no-overflow.i error (134) 0 wit inspect .58 37 6.7 error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .020 5.0 error (invalid witness file) 0 wit inspect .0010 .27 - wit inspect
cut_false-no-overflow.i error (134) 0 wit inspect 13    51 120   error (invalid witness file) 0 wit inspect .40 43 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .0011 .33 - wit inspect
date_false-no-overflow.i error (6) 0 wit inspect .43 46 3.1 error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .038 4.8 error (invalid witness file) 0 wit inspect .0016 .29 - wit inspect
du_false-no-overflow.i error (5) 0 wit inspect 6.8  44 58   error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect
echo_false-no-overflow.i error (134) 0 wit inspect .50 38 5.0 error (invalid witness file) 0 wit inspect .44 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect
expand_false-no-overflow.i error (134) 0 wit inspect 31    72 300   error (invalid witness file) 0 wit inspect .39 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect
fold_false-no-overflow.i error (134) 0 wit inspect 5.6  42 48   error (invalid witness file) 0 wit inspect .40 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect
head_false-no-overflow.i error (6) 0 wit inspect .39 40 3.2 error (invalid witness file) 0 wit inspect .43 43 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .0030 .34 - wit inspect
logname_false-no-overflow.i error (134) 0 wit inspect .32 37 3.2 error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .025 5.0 error (invalid witness file) 0 wit inspect .0011 .29 - wit inspect
ls-incomplete_false-no-overflow.i error (5) 0 wit inspect 230    190 2100   error (invalid witness file) 0 wit inspect .55 45 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect
mkdir_false-no-overflow.i error (134) 0 wit inspect 2.6  43 23   error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect
mkfifo-incomplete_false-no-overflow.i error (134) 0 wit inspect .30 36 2.8 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .0012 .30 - wit inspect
od_false-no-overflow.i error (134) 0 wit inspect 750    320 7200   error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .022 4.8 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect
printf_false-no-overflow.i error (6) 0 wit inspect .54 42 4.4 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0015 .26 - wit inspect
readlink_false-no-overflow.i error (134) 0 wit inspect 2.8  40 23   error (invalid witness file) 0 wit inspect .40 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0015 .26 - wit inspect
realpath_false-no-overflow.i error (134) 0 wit inspect .36 37 3.1 error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .023 5.0 error (invalid witness file) 0 wit inspect .0015 .26 - wit inspect
rm_false-no-overflow.i error (5) 0 wit inspect 6.4  44 60   error (invalid witness file) 0 wit inspect .40 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect
seq_false-no-overflow.i error (134) 0 wit inspect 1.6  40 15   error (invalid witness file) 0 wit inspect .40 43 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .0014 .35 - wit inspect
sleep_false-no-overflow.i error (134) 0 wit inspect .91 39 12   error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .0012 .34 - wit inspect
stty_false-no-overflow.i error (134) 0 wit inspect 73    120 670   error (invalid witness file) 0 wit inspect .44 43 error (2) 0 wit inspect .024 5.0 error (invalid witness file) 0 wit inspect .0014 .31 - wit inspect
sync_false-no-overflow.i error (134) 0 wit inspect .27 35 3.3 error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect
tac_false-no-overflow.i error (134) 0 wit inspect 5.4  41 51   error (invalid witness file) 0 wit inspect .43 43 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .0014 .34 - wit inspect
tee_false-no-overflow.i error (6) 0 wit inspect .35 41 3.3 error (invalid witness file) 0 wit inspect .40 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .0014 .32 - wit inspect
test-incomplete_false-no-overflow.i error (5) 0 wit inspect 32    74 280   error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0015 .33 - wit inspect
touch_false-no-overflow.i error (134) 0 wit inspect 5.7  45 49   error (invalid witness file) 0 wit inspect .41 43 error (2) 0 wit inspect .048 4.9 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect
uname_false-no-overflow.i error (134) 0 wit inspect 1.6  41 14   error (invalid witness file) 0 wit inspect .60 45 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0032 .34 - wit inspect
uniq_false-no-overflow.i error (134) 0 wit inspect 5.5  41 43   error (invalid witness file) 0 wit inspect .41 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0011 .29 - wit inspect
usleep_false-no-overflow.i error (134) 0 wit inspect .47 37 4.1 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect
uudecode_false-no-overflow.i error (134) 0 wit inspect 11    48 94   error (invalid witness file) 0 wit inspect .43 41 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0015 .29 - wit inspect
wc_false-no-overflow.i error (6) 0 wit inspect .35 42 3.2 error (invalid witness file) 0 wit inspect .39 43 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect
who_false-no-overflow.i error (134) 0 wit inspect 1.7  42 14   error (invalid witness file) 0 wit inspect .40 45 error (2) 0 wit inspect .022 5.0 error (invalid witness file) 0 wit inspect .0010 .26 - wit inspect
whoami-incomplete_false-no-overflow.i - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect
yes_false-no-overflow.i error (134) 0 wit inspect .33 37 3.0 error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .025 4.8 error (invalid witness file) 0 wit inspect .0014 .34 - wit inspect
basename_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect .24 32 2.0 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
chgrp-incomplete_true-no-overflow_false-valid-memtrack.i error (134) 0 wit inspect .29 37 3.5 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
chroot-incomplete_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect .59 37 6.1 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
cut_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect 14    51 110   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
date_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (6) 0 wit inspect .45 46 3.4 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
dirname_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect .24 31 1.7 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
du_true-no-overflow_true-valid-memsafety.i error (5) 0 wit inspect 6.8  44 57   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
echo_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect .48 38 5.0 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
expand_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect 30    71 260   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .046 4.9
fold_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect 5.4  42 41   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
head_true-no-overflow_true-valid-deref.i error (6) 0 wit inspect .42 40 2.6 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
hostid_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect .26 34 1.9 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .017 4.8
logname_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect .34 36 2.6 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
ls-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (5) 0 wit inspect 230    190 2000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
mkdir_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect 2.6  43 20   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
mkfifo-incomplete_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect .30 36 2.4 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
od_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect 760    320 7400   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .017 4.8
printf_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (6) 0 wit inspect .55 43 4.1 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
readlink_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect 2.5  41 26   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
realpath_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect .33 37 3.5 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .048 4.9
rm_true-no-overflow_true-valid-memsafety.i error (5) 0 wit inspect 6.0  43 55   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
seq_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect 1.6  40 14   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
sleep_true-no-overflow_true-valid-deref.i error (134) 0 wit inspect .97 38 8.1 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .050 4.8
stty_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect 70    120 600   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
sync_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect .30 35 2.6 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
tac_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect 5.4  41 45   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
tee_true-no-overflow_true-valid-memsafety.i error (6) 0 wit inspect .36 41 2.8 - 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 29    73 330   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
touch_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect 5.7  45 54   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
uname_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect 1.6  41 13   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
uniq_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect 5.0  42 47   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
usleep_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect .46 37 4.1 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
uudecode_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect 11    49 93   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
wc_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (6) 0 wit inspect .34 42 3.1 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
who_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect 1.6  41 15   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
whoami-incomplete_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect .32 37 3.0 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
yes_true-no-overflow_true-valid-memsafety.i error (134) 0 wit inspect .34 36 3.0 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 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 70 0 2400 4000 23000 34 0 16 1500 34 0 .74 170 34 0 .050 9.8 37 0 .75 180
    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 (71 tasks, max score: 108) 0 0 0 0 0
Run set 2ls.sv-comp18.Systems_BusyBox_NoOverflows cpa-seq-validate-violation-witnesses-2ls.sv-comp18-violation-witness.Systems_BusyBox_NoOverflows uautomizer-validate-violation-witnesses-2ls.sv-comp18-violation-witness.Systems_BusyBox_NoOverflows fshell-witness2test-validate-violation-witnesses-2ls.sv-comp18-violation-witness.Systems_BusyBox_NoOverflows uautomizer-validate-correctness-witnesses-2ls.sv-comp18-correctness-witness.Systems_BusyBox_NoOverflows