Tool 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* [apollon004; apollon025; apollon077; apollon078; apollon080] [apollon077; apollon078; apollon157] [apollon038; apollon077; apollon078; apollon164] [apollon025; apollon052; 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:49:29 CET 2017-12-01 12:01:34 CET 2017-12-01 12:20:33 CET 2017-12-01 12:23:03 CET 2017-12-01 12:03:46 CET
Run set cpa-seq.sv-comp18.Systems_BusyBox_NoOverflows cpa-seq-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.Systems_BusyBox_NoOverflows uautomizer-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.Systems_BusyBox_NoOverflows fshell-witness2test-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.Systems_BusyBox_NoOverflows uautomizer-validate-correctness-witnesses-cpa-seq.sv-comp18-correctness-witness.Systems_BusyBox_NoOverflows
Options -svcomp18 -heap 10000M -benchmark -timelimit 900s -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-seq.2017-12-01_1049.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/cpa-seq.2017-12-01_1049.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/cpa-seq.2017-12-01_1049.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cpa-seq.2017-12-01_1049.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   1700 5700 0 .43 43 0 .047 4.8 0 .0019 .29 -
chroot-incomplete_false-no-overflow.i 0 38   520 430 0 .64 43 0 .044 5.0 0 .0012 .28 -
cut_false-no-overflow.i 0 900   6100 12000 0 .61 43 0 .021 4.8 0 .0036 .28 -
date_false-no-overflow.i 0 900   3300 10000 0 .43 42 0 .024 4.9 0 .0039 .26 -
du_false-no-overflow.i 0 900   3400 9900 0 .67 43 0 .018 4.8 0 .0012 .26 -
echo_false-no-overflow.i 0 900   1100 11000 0 .65 44 0 .018 4.8 0 .0021 .26 -
expand_false-no-overflow.i 0 900   5900 9200 0 .56 43 0 .048 4.9 0 .0011 .26 -
fold_false-no-overflow.i 0 900   1100 9800 0 .63 43 0 .023 4.9 0 .0011 .28 -
head_false-no-overflow.i 0 900   1300 6800 0 .64 44 0 .024 4.8 0 .0035 .26 -
logname_false-no-overflow.i 0 900   1300 5500 0 .56 44 0 .019 4.9 0 .0011 .28 -
ls-incomplete_false-no-overflow.i 0 900   3100 11000 0 .39 41 0 .019 4.9 0 .0016 .29 -
mkdir_false-no-overflow.i 0 900   6200 10000 0 .40 42 0 .019 4.8 0 .0019 .26 -
mkfifo-incomplete_false-no-overflow.i 0 110   780 1100 0 91    510 -32 5.4   300   -32 .92   20    -
od_false-no-overflow.i 0 900   6300 11000 0 .40 42 0 .046 4.9 0 .0011 .31 -
printf_false-no-overflow.i 0 490   910 3100 0 91    620 -32 10     480   0 .63   20    -
readlink_false-no-overflow.i 0 900   6300 11000 0 .56 43 0 .019 4.8 0 .0011 .29 -
realpath_false-no-overflow.i 0 900   1500 6000 0 .68 43 0 .019 4.8 0 .0014 .28 -
rm_false-no-overflow.i 0 900   6200 11000 0 .41 43 0 .018 4.8 0 .0014 .26 -
seq_false-no-overflow.i 0 900   6400 9900 0 .49 43 0 .020 4.9 0 .0041 .31 -
sleep_false-no-overflow.i 0 6.5 320 56 0 .57 43 0 .018 4.9 0 .0012 .26 -
stty_false-no-overflow.i 0 2.5 180 22 0 .55 42 0 .024 4.9 0 .0019 .28 -
sync_false-no-overflow.i 0 46   580 490 0 .50 41 0 .024 4.9 0 .0011 .26 -
tac_false-no-overflow.i 0 900   6200 8400 0 .66 44 0 .018 4.8 0 .0011 .26 -
tee_false-no-overflow.i 0 900   3300 11000 0 .61 43 0 .018 4.9 0 .0014 .29 -
test-incomplete_false-no-overflow.i 0 900   4300 11000 0 .66 44 0 .018 4.8 0 .0019 .29 -
touch_false-no-overflow.i 0 900   6200 9900 0 .56 44 0 .018 4.9 0 .0014 .26 -
uname_false-no-overflow.i 0 900   6000 11000 0 .56 43 0 .025 4.8 0 .0035 .26 -
uniq_false-no-overflow.i 0 900   6300 12000 0 .40 41 0 .025 5.0 0 .0011 .26 -
usleep_false-no-overflow.i 0 900   1200 5800 0 .45 43 0 .021 5.0 0 .0011 .26 -
uudecode_false-no-overflow.i 0 2.6 190 22 0 .65 43 0 .018 4.9 0 .0033 .30 -
wc_false-no-overflow.i 0 900   5800 9600 0 .53 41 0 .020 5.0 0 .0017 .29 -
who_false-no-overflow.i 0 900   6300 9400 0 .58 44 0 .018 4.9 0 .0015 .31 -
whoami-incomplete_false-no-overflow.i - 0 .56 45 0 .023 4.9 0 .0036 .31 -
yes_false-no-overflow.i 0 900   1300 7900 0 .52 41 0 .049 4.9 0 .0011 .28 -
basename_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 900   3400 11000 - - - 0 .039 4.9
chgrp-incomplete_true-no-overflow_false-valid-memtrack.i 0 250   15000 2000 - - - 0 .025 4.9
chroot-incomplete_true-no-overflow_true-valid-memsafety.i 0 33   520 340 - - - 0 .019 4.8
cut_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 900   6100 11000 - - - 0 .024 5.0
date_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 900   3300 10000 - - - 0 .018 4.8
dirname_true-no-overflow_true-valid-memsafety.i 0 900   5200 9500 - - - 0 .018 4.8
du_true-no-overflow_true-valid-memsafety.i 0 900   3300 11000 - - - 0 .018 4.8
echo_true-no-overflow_true-valid-memsafety.i 0 900   1000 9600 - - - 0 .018 4.8
expand_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 900   5900 11000 - - - 0 .019 4.9
fold_true-no-overflow_true-valid-memsafety.i 0 900   930 10000 - - - 0 .020 4.9
head_true-no-overflow_true-valid-deref.i 0 150   880 1200 - - - 0 .018 4.8
hostid_true-no-overflow_true-valid-memsafety.i 0 530   15000 5900 - - - 0 .022 4.8
logname_true-no-overflow_true-valid-memsafety.i 0 290   15000 2000 - - - 0 .018 4.9
ls-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 900   3100 9100 - - - 0 .018 4.9
mkdir_true-no-overflow_true-valid-memsafety.i 0 900   6400 11000 - - - 0 .018 4.8
mkfifo-incomplete_true-no-overflow_true-valid-memsafety.i 0 900   1300 5800 - - - 0 .022 4.8
od_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 900   6300 10000 - - - 0 .019 4.8
printf_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 260   850 2200 - - - 0 .017 4.9
readlink_true-no-overflow_true-valid-memsafety.i 0 900   6200 13000 - - - 0 .024 4.8
realpath_true-no-overflow_true-valid-memsafety.i 0 900   1500 6800 - - - 0 .018 4.8
rm_true-no-overflow_true-valid-memsafety.i 0 900   6400 11000 - - - 0 .018 4.8
seq_true-no-overflow_true-valid-memsafety.i 0 900   6300 12000 - - - 0 .018 4.8
sleep_true-no-overflow_true-valid-deref.i 0 6.5 340 65 - - - 0 .044 4.8
stty_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 2.8 200 27 - - - 0 .018 5.0
sync_true-no-overflow_true-valid-memsafety.i 0 40   700 530 - - - 0 .024 4.8
tac_true-no-overflow_true-valid-memsafety.i 0 900   6300 10000 - - - 0 .024 5.0
tee_true-no-overflow_true-valid-memsafety.i 0 900   3300 13000 - - - 0 .018 4.8
test-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 900   4600 10000 - - - 0 .018 4.8
touch_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 900   6200 12000 - - - 0 .024 4.8
uname_true-no-overflow_true-valid-memsafety.i 0 900   6000 12000 - - - 0 .020 5.0
uniq_true-no-overflow_true-valid-memsafety.i 0 900   6200 11000 - - - 0 .023 4.8
usleep_true-no-overflow_true-valid-memsafety.i 0 210   880 1500 - - - 0 .018 4.9
uudecode_true-no-overflow_true-valid-memsafety.i 0 2.4 170 21 - - - 0 .019 4.9
wc_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 900   5800 11000 - - - 0 .025 4.9
who_true-no-overflow_true-valid-memsafety.i 0 900   6200 12000 - - - 0 .018 4.8
whoami-incomplete_true-no-overflow_true-valid-memsafety.i 0 900   2200 12000 - - - 0 .018 4.9
yes_true-no-overflow_true-valid-memsafety.i 0 900   1200 6900 - - - 0 .020 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 49000 280000 540000 34 0 200 2500 34 -64 17 930 34 -32 1.6  49 37 0 .78 180
    correct results 0 0 0 0 0
        correct true 0 0 0 0 0
        correct false 0 0 0 0 0
    correct-unconfimed results 2 0 600 1700 4200 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0
        correct-unconfirmed false 2 0 600 1700 4200 0 0 0 0
    incorrect results 0 0 2 -64 16 780 1 -32 .92 20 0
        incorrect true 0 0 2 -64 16 780 1 -32 .92 20 0
        incorrect false 0 0 0 0 0
score (71 tasks, max score: 108) 0 0 -64 -32 0
Run set cpa-seq.sv-comp18.Systems_BusyBox_NoOverflows cpa-seq-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.Systems_BusyBox_NoOverflows uautomizer-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.Systems_BusyBox_NoOverflows fshell-witness2test-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.Systems_BusyBox_NoOverflows uautomizer-validate-correctness-witnesses-cpa-seq.sv-comp18-correctness-witness.Systems_BusyBox_NoOverflows