Tool ULTIMATE Automizer 0.1.23-3204b741 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] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-12-03 11:17:40 CET 2017-12-03 11:52:01 CET 2017-12-03 12:09:33 CET 2017-12-03 12:09:49 CET 2017-12-03 11:53:41 CET
Run set uautomizer.sv-comp18.Systems_BusyBox_NoOverflows cpa-seq-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.Systems_BusyBox_NoOverflows uautomizer-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.Systems_BusyBox_NoOverflows fshell-witness2test-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.Systems_BusyBox_NoOverflows uautomizer-validate-correctness-witnesses-uautomizer.sv-comp18-correctness-witness.Systems_BusyBox_NoOverflows
Options --full-output -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/uautomizer.2017-12-03_1117.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/uautomizer.2017-12-03_1117.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/uautomizer.2017-12-03_1117.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/uautomizer.2017-12-03_1117.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 0 wit inspect 270   1600 2800 error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .050 4.9 error (invalid witness file) 0 wit inspect .0038 .30 - wit inspect
chroot-incomplete_false-no-overflow.i error 0 wit inspect 380   1700 3800 error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .045 4.9 error (invalid witness file) 0 wit inspect .0041 .32 - wit inspect
cut_false-no-overflow.i timeout 0 wit inspect 900   2200 7100 error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .047 4.9 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect
date_false-no-overflow.i error (7) 0 wit inspect 4.3 230 34 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .046 4.9 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect
du_false-no-overflow.i timeout 0 wit inspect 900   12000 7400 error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .049 4.9 error (invalid witness file) 0 wit inspect .0039 .32 - wit inspect
echo_false-no-overflow.i timeout 0 wit inspect 900   3000 7600 error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .046 4.8 error (invalid witness file) 0 wit inspect .0021 .28 - wit inspect
expand_false-no-overflow.i timeout 0 wit inspect 900   2700 6000 error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .047 4.9 error (invalid witness file) 0 wit inspect .0051 .26 - wit inspect
fold_false-no-overflow.i timeout 0 wit inspect 900   1900 8000 error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .026 4.9 error (invalid witness file) 0 wit inspect .0040 .29 - wit inspect
head_false-no-overflow.i timeout 0 wit inspect 900   5500 8700 error (invalid witness file) 0 wit inspect .49 41 error (2) 0 wit inspect .047 4.9 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect
logname_false-no-overflow.i error 0 wit inspect 76   1100 800 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .048 5.0 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect
ls-incomplete_false-no-overflow.i error (7) 0 wit inspect 4.5 230 32 error (invalid witness file) 0 wit inspect .51 42 error (2) 0 wit inspect .048 4.8 error (invalid witness file) 0 wit inspect .0045 .28 - wit inspect
mkdir_false-no-overflow.i timeout 0 wit inspect 900   1900 6700 error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .046 4.9 error (invalid witness file) 0 wit inspect .0018 .26 - wit inspect
mkfifo-incomplete_false-no-overflow.i error 0 wit inspect 130   1200 1600 error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .047 4.9 error (invalid witness file) 0 wit inspect .0033 .28 - wit inspect
od_false-no-overflow.i error (7) 0 wit inspect 6.9 320 52 error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect
printf_false-no-overflow.i error 0 wit inspect 230   2000 1800 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .047 4.9 error (invalid witness file) 0 wit inspect .0038 .33 - wit inspect
readlink_false-no-overflow.i timeout 0 wit inspect 900   1800 8400 error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0049 .33 - wit inspect
realpath_false-no-overflow.i error 0 wit inspect 160   1500 1600 error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .048 4.8 error (invalid witness file) 0 wit inspect .0039 .26 - wit inspect
rm_false-no-overflow.i timeout 0 wit inspect 900   1300 8900 error (invalid witness file) 0 wit inspect .50 41 error (2) 0 wit inspect .042 4.8 error (invalid witness file) 0 wit inspect .0021 .34 - wit inspect
seq_false-no-overflow.i error (7) 0 wit inspect 4.4 240 39 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .027 4.8 error (invalid witness file) 0 wit inspect .0040 .28 - wit inspect
sleep_false-no-overflow.i error 0 wit inspect 570   2200 5800 error (invalid witness file) 0 wit inspect .53 45 error (2) 0 wit inspect .041 4.9 error (invalid witness file) 0 wit inspect .0010 .34 - wit inspect
stty_false-no-overflow.i error (7) 0 wit inspect 4.6 290 37 error (invalid witness file) 0 wit inspect .51 45 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .0031 .26 - wit inspect
sync_false-no-overflow.i error 0 wit inspect 200   1400 2400 error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect .0012 .33 - wit inspect
tac_false-no-overflow.i timeout 0 wit inspect 900   3600 7700 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .050 4.9 error (invalid witness file) 0 wit inspect .0044 .26 - wit inspect
tee_false-no-overflow.i timeout 0 wit inspect 900   12000 7000 error (invalid witness file) 0 wit inspect .52 45 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect .0048 .26 - wit inspect
test-incomplete_false-no-overflow.i error (7) 0 wit inspect 4.5 230 33 error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .047 4.9 error (invalid witness file) 0 wit inspect .0039 .26 - wit inspect
touch_false-no-overflow.i timeout 0 wit inspect 900   2400 5900 error (invalid witness file) 0 wit inspect .48 42 error (2) 0 wit inspect .045 4.9 error (invalid witness file) 0 wit inspect .0047 .32 - wit inspect
uname_false-no-overflow.i timeout 0 wit inspect 900   3100 7100 error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect .0048 .26 - wit inspect
uniq_false-no-overflow.i timeout 0 wit inspect 900   1300 8600 error (invalid witness file) 0 wit inspect .50 41 error (2) 0 wit inspect .053 4.9 error (invalid witness file) 0 wit inspect .0047 .26 - wit inspect
usleep_false-no-overflow.i error 0 wit inspect 200   3000 2300 error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect .0047 .28 - wit inspect
uudecode_false-no-overflow.i error (7) 0 wit inspect 4.5 230 34 error (invalid witness file) 0 wit inspect .51 42 error (2) 0 wit inspect .042 4.9 error (invalid witness file) 0 wit inspect .0040 .36 - wit inspect
wc_false-no-overflow.i timeout 0 wit inspect 900   1800 8200 error (invalid witness file) 0 wit inspect .51 42 error (2) 0 wit inspect .046 4.9 error (invalid witness file) 0 wit inspect .0040 .26 - wit inspect
who_false-no-overflow.i error (7) 0 wit inspect 4.5 230 37 error (invalid witness file) 0 wit inspect .50 42 error (2) 0 wit inspect .047 5.0 error (invalid witness file) 0 wit inspect .0051 .26 - wit inspect
whoami-incomplete_false-no-overflow.i - wit inspect error (1) 0 wit inspect .76 46 true -32 wit inspect 15     510   error (1) 0 wit inspect .10   9.8  - wit inspect
yes_false-no-overflow.i error 0 wit inspect 190   1500 1900 error (invalid witness file) 0 wit inspect .49 43 error (2) 0 wit inspect .034 4.8 error (invalid witness file) 0 wit inspect .0019 .26 - wit inspect
basename_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (7) 0 wit inspect 3.9 220 33 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
chgrp-incomplete_true-no-overflow_false-valid-memtrack.i error 0 wit inspect 380   1500 4000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
chroot-incomplete_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 340   1800 2900 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
cut_false-unreach-call_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   2000 6800 - 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 (7) 0 wit inspect 4.5 230 35 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.9
dirname_true-no-overflow_true-valid-memsafety.i error (7) 0 wit inspect 4.1 230 32 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
du_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   10000 5600 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
echo_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   2900 8400 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 5.0
expand_false-unreach-call_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   2700 7700 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
fold_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   2200 6800 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
head_true-no-overflow_true-valid-deref.i error 0 wit inspect 230   4100 2200 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
hostid_true-no-overflow_true-valid-memsafety.i true 2 wit inspect 9.6 480 74 - wit inspect - wit inspect - wit inspect true 2 wit inspect 11     420  
logname_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 130   1000 1500 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .017 4.8
ls-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (7) 0 wit inspect 4.8 230 38 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.8
mkdir_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   2100 6700 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
mkfifo-incomplete_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 160   1100 1600 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
od_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (7) 0 wit inspect 6.2 320 52 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
printf_false-unreach-call_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 330   1900 2400 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
readlink_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   2400 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .017 4.9
realpath_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 190   1300 2100 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
rm_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   2000 10000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
seq_true-no-overflow_true-valid-memsafety.i error (7) 0 wit inspect 4.5 240 34 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
sleep_true-no-overflow_true-valid-deref.i error 0 wit inspect 630   3900 6400 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.8
stty_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (7) 0 wit inspect 4.7 290 44 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
sync_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 170   1400 1700 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
tac_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   3100 7600 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
tee_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   9900 6100 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .017 4.9
test-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i error (7) 0 wit inspect 4.1 230 36 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
touch_false-unreach-call_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   2200 6800 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
uname_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   3100 6700 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
uniq_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   1400 9000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
usleep_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 210   2700 2200 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
uudecode_true-no-overflow_true-valid-memsafety.i error (7) 0 wit inspect 4.4 230 38 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
wc_false-unreach-call_true-no-overflow_true-valid-memsafety.i timeout 0 wit inspect 900   2100 8900 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .017 4.9
who_true-no-overflow_true-valid-memsafety.i error (7) 0 wit inspect 4.4 230 33 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
whoami-incomplete_true-no-overflow_true-valid-memsafety.i true 2 wit inspect 13   610 100 - wit inspect - wit inspect - wit inspect true 2 wit inspect 15     520  
yes_true-no-overflow_true-valid-memsafety.i error 0 wit inspect 170   1600 2000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 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 70 4 32000 150000 280000 34 0 18 1500 34 -32 17 670 34 0 .21 19 37 4 27 1100
    correct results 2 4 23 1100 180 0 0 0 2 4 26 930
        correct true 2 4 23 1100 180 0 0 0 2 4 26 930
        correct false 0 0 0 0 0
    incorrect results 0 0 1 -32 15 510 0 0
        incorrect true 0 0 1 -32 15 510 0 0
        incorrect false 0 0 0 0 0
score (71 tasks, max score: 108) 4 0 -32 0 4
Run set uautomizer.sv-comp18.Systems_BusyBox_NoOverflows cpa-seq-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.Systems_BusyBox_NoOverflows uautomizer-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.Systems_BusyBox_NoOverflows fshell-witness2test-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.Systems_BusyBox_NoOverflows uautomizer-validate-correctness-witnesses-uautomizer.sv-comp18-correctness-witness.Systems_BusyBox_NoOverflows