Tool ULTIMATE Taipan 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]
Date of execution 2017-12-03 08:43:49 CET 2017-12-03 08:58:51 CET 2017-12-03 09:15:45 CET 2017-12-03 09:17:25 CET 2017-12-03 09:00:18 CET
Run set utaipan.sv-comp18.Systems_BusyBox_NoOverflows cpa-seq-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.Systems_BusyBox_NoOverflows uautomizer-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.Systems_BusyBox_NoOverflows fshell-witness2test-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.Systems_BusyBox_NoOverflows uautomizer-validate-correctness-witnesses-utaipan.sv-comp18-correctness-witness.Systems_BusyBox_NoOverflows
Options --full-output -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/utaipan.2017-12-03_0843.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/utaipan.2017-12-03_0843.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/utaipan.2017-12-03_0843.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/utaipan.2017-12-03_0843.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 0 900   6400 12000 0 .57 43 0 .019 4.8 0 .0018 .29 -
chroot-incomplete_false-no-overflow.i 0 900   6000 13000 0 .54 41 0 .044 4.8 0 .0041 .26 -
cut_false-no-overflow.i 0 900   5900 12000 0 .55 44 0 .025 4.8 0 .0046 .29 -
date_false-no-overflow.i 0 4.5 240 35 0 .56 41 0 .027 4.8 0 .0013 .26 -
du_false-no-overflow.i 0 900   5600 8600 0 .59 44 0 .019 4.8 0 .0012 .26 -
echo_false-no-overflow.i 0 900   6400 12000 0 .55 43 0 .051 4.8 0 .0018 .28 -
expand_false-no-overflow.i 0 900   5700 12000 0 .55 44 0 .020 4.8 0 .0014 .32 -
fold_false-no-overflow.i 0 900   4700 12000 0 .57 41 0 .048 5.0 0 .0045 .26 -
head_false-no-overflow.i 0 900   6300 14000 0 .53 41 0 .038 4.9 0 .0046 .30 -
logname_false-no-overflow.i 0 900   6500 11000 0 .56 43 0 .020 4.9 0 .0047 .26 -
ls-incomplete_false-no-overflow.i 0 4.6 230 34 0 .59 44 0 .023 4.8 0 .0013 .28 -
mkdir_false-no-overflow.i 0 900   5800 13000 0 .57 41 0 .024 4.9 0 .0012 .26 -
mkfifo-incomplete_false-no-overflow.i 0 900   6500 12000 0 .59 44 0 .019 4.9 0 .0042 .26 -
od_false-no-overflow.i 0 5.6 290 47 0 .56 41 0 .047 4.8 0 .0045 .26 -
printf_false-no-overflow.i 0 900   6100 12000 0 .54 43 0 .048 4.9 0 .0038 .33 -
readlink_false-no-overflow.i 0 900   6000 14000 0 .54 44 0 .024 4.8 0 .0036 .36 -
realpath_false-no-overflow.i 0 900   6500 12000 0 .42 43 0 .050 4.9 0 .0041 .26 -
rm_false-no-overflow.i 0 900   6100 11000 0 .59 44 0 .020 4.9 0 .0046 .26 -
seq_false-no-overflow.i 0 4.3 230 34 0 .59 47 0 .020 4.8 0 .0046 .29 -
sleep_false-no-overflow.i 0 900   5100 12000 0 .54 43 0 .018 4.8 0 .0042 .26 -
stty_false-no-overflow.i 0 5.0 300 42 0 .57 41 0 .019 4.8 0 .0043 .28 -
sync_false-no-overflow.i 0 910   6300 10000 0 .52 41 0 .020 5.0 0 .0010 .31 -
tac_false-no-overflow.i 0 900   5800 12000 0 .57 43 0 .048 4.8 0 .0035 .29 -
tee_false-no-overflow.i 0 900   5300 7900 0 .54 42 0 .038 4.9 0 .0017 .27 -
test-incomplete_false-no-overflow.i 0 4.5 240 33 0 .55 43 0 .048 4.9 0 .0038 .28 -
touch_false-no-overflow.i 0 900   6200 13000 0 .57 43 0 .019 4.8 0 .0041 .30 -
uname_false-no-overflow.i 0 900   5900 11000 0 .55 44 0 .045 4.8 0 .0012 .28 -
uniq_false-no-overflow.i 0 900   6100 12000 0 .54 42 0 .019 4.8 0 .0037 .29 -
usleep_false-no-overflow.i 0 900   4800 10000 0 .56 43 0 .018 5.0 0 .0011 .30 -
uudecode_false-no-overflow.i 0 4.5 240 35 0 .58 44 0 .019 4.9 0 .0012 .26 -
wc_false-no-overflow.i 0 900   5500 11000 0 .56 42 0 .020 4.8 0 .0015 .26 -
who_false-no-overflow.i 0 4.3 230 34 0 .57 42 0 .044 4.9 0 .0011 .30 -
whoami-incomplete_false-no-overflow.i - 0 .80 48 -32 16     520   0 .12   9.7  -
yes_false-no-overflow.i 0 900   6700 11000 0 .59 45 0 .021 4.9 0 .0042 .35 -
basename_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 4.0 230 33 - - - 0 .035 4.8
chgrp-incomplete_true-no-overflow_false-valid-memtrack.i 0 900   6400 11000 - - - 0 .030 4.9
chroot-incomplete_true-no-overflow_true-valid-memsafety.i 0 900   6000 14000 - - - 0 .054 4.8
cut_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 900   5900 11000 - - - 0 .019 4.8
date_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 4.2 240 37 - - - 0 .038 4.9
dirname_true-no-overflow_true-valid-memsafety.i 0 3.9 230 34 - - - 0 .019 4.8
du_true-no-overflow_true-valid-memsafety.i 0 900   5500 9900 - - - 0 .047 4.8
echo_true-no-overflow_true-valid-memsafety.i 0 900   6500 11000 - - - 0 .019 5.0
expand_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 900   5600 12000 - - - 0 .046 4.8
fold_true-no-overflow_true-valid-memsafety.i 0 910   4700 12000 - - - 0 .019 5.0
head_true-no-overflow_true-valid-deref.i 0 900   6600 11000 - - - 0 .048 4.9
hostid_true-no-overflow_true-valid-memsafety.i 2 9.7 450 81 - - - 2 12     430  
logname_true-no-overflow_true-valid-memsafety.i 0 900   6500 12000 - - - 0 .023 4.9
ls-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 4.4 230 34 - - - 0 .048 4.9
mkdir_true-no-overflow_true-valid-memsafety.i 0 900   5900 12000 - - - 0 .018 4.8
mkfifo-incomplete_true-no-overflow_true-valid-memsafety.i 0 910   6600 12000 - - - 0 .042 4.8
od_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 5.9 300 46 - - - 0 .031 4.8
printf_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 900   6200 12000 - - - 0 .019 4.9
readlink_true-no-overflow_true-valid-memsafety.i 0 900   6000 13000 - - - 0 .042 4.9
realpath_true-no-overflow_true-valid-memsafety.i 0 900   6500 14000 - - - 0 .017 4.9
rm_true-no-overflow_true-valid-memsafety.i 0 900   6100 13000 - - - 0 .023 4.8
seq_true-no-overflow_true-valid-memsafety.i 0 4.4 240 32 - - - 0 .038 4.8
sleep_true-no-overflow_true-valid-deref.i 0 900   5100 12000 - - - 0 .029 4.8
stty_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 4.9 280 37 - - - 0 .020 4.9
sync_true-no-overflow_true-valid-memsafety.i 0 900   6400 11000 - - - 0 .018 4.8
tac_true-no-overflow_true-valid-memsafety.i 0 900   6000 13000 - - - 0 .044 5.0
tee_true-no-overflow_true-valid-memsafety.i 0 900   5600 9200 - - - 0 .049 4.8
test-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 4.3 230 34 - - - 0 .038 4.8
touch_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 900   6000 12000 - - - 0 .026 4.9
uname_true-no-overflow_true-valid-memsafety.i 0 900   5900 13000 - - - 0 .044 4.8
uniq_true-no-overflow_true-valid-memsafety.i 0 900   6100 11000 - - - 0 .037 5.0
usleep_true-no-overflow_true-valid-memsafety.i 0 900   4800 11000 - - - 0 .047 4.8
uudecode_true-no-overflow_true-valid-memsafety.i 0 4.5 240 36 - - - 0 .019 4.8
wc_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 900   5400 12000 - - - 0 .024 4.9
who_true-no-overflow_true-valid-memsafety.i 0 4.1 230 31 - - - 0 .048 4.8
whoami-incomplete_true-no-overflow_true-valid-memsafety.i 2 13   570 110 - - - 2 16     520  
yes_true-no-overflow_true-valid-memsafety.i 0 900   6600 12000 - - - 0 .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 4 45000 300000 580000 34 0 19 1500 34 -32 17 680 34 0 .22 19 37 4 29 1100
    correct results 2 4 23 1000 190 0 0 0 2 4 28 940
        correct true 2 4 23 1000 190 0 0 0 2 4 28 940
        correct false 0 0 0 0 0
    incorrect results 0 0 1 -32 16 520 0 0
        incorrect true 0 0 1 -32 16 520 0 0
        incorrect false 0 0 0 0 0
score (71 tasks, max score: 108) 4 0 -32 0 4
Run set utaipan.sv-comp18.Systems_BusyBox_NoOverflows cpa-seq-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.Systems_BusyBox_NoOverflows uautomizer-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.Systems_BusyBox_NoOverflows fshell-witness2test-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.Systems_BusyBox_NoOverflows uautomizer-validate-correctness-witnesses-utaipan.sv-comp18-correctness-witness.Systems_BusyBox_NoOverflows