Tool CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a CPA-witness2test 1.7-svn 29852 CProver witness2test 0.1 ULTIMATE Automizer 0.1.23-635dfa2a
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.15.0-42-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB
Date of execution 2018-12-05 05:46:16 CET 2018-12-06 09:44:44 CET 2018-12-06 10:50:29 CET 2018-12-06 10:57:45 CET 2018-12-12 19:32:16 CET 2018-12-06 09:52:34 CET
Run set cpa-seq.sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows cpa-seq-validate-violation-witnesses-cpa-seq.sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows uautomizer-validate-violation-witnesses-cpa-seq.sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows cpa-witness2test-validate-violation-witnesses-cpa-seq.sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows fshell-witness2test-validate-violation-witnesses-cpa-seq.sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows uautomizer-validate-correctness-witnesses-cpa-seq.sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows
Options -svcomp19 -heap 10000M -benchmark -timelimit 900s -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -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 -witness ../../results-verified/cpa-seq.2018-12-05_0546.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cpa-seq.2018-12-05_0546.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true -witness ../../results-verified/cpa-seq.2018-12-05_0546.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/cpa-seq.2018-12-05_0546.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cpa-seq.2018-12-05_0546.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/busybox-1.22.0/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
chgrp-incomplete_false-no-overflow.i 0 900   890   1700 7600 0   0   0 .96 .56 45 0   0   0 8.1   4.8   300   .66 0   0 1.1  .72 51 0     0   0 .073  .073  12    0     0    -
chroot-incomplete_false-no-overflow.i 0 900   890   1300 5900 0   0   0 1.0  .61 47 0   0   0 8.3   4.6   290   .66 0   0 1.2  .73 51 0     0   0 .094  .096  11    0     0    -
cut_false-no-overflow.i 0 900   870   6700 11000 0   0   0 1.1  .63 50 0   0   0 10     5.5   300   .62 0   0 1.2  .74 54 0     0   0 .13   .13   13    0     0    -
date_false-no-overflow.i 0 900   880   3400 11000 0   0   0 .95 .57 51 0   0   0 9.5   5.3   300   .66 0   0 1.2  .78 55 0     0   0 .12   .12   14    0     0    -
du_false-no-overflow.i 0 900   880   3300 11000 0   0   0 1.1  .62 55 0   0   0 11     6.7   350   .62 0   0 1.4  .85 61 0     0   0 .11   .11   14    0     0    -
echo_false-no-overflow.i 0 910   890   850 13000 0   0   0 .92 .54 46 0   0   0 8.5   4.9   300   .66 0   0 1.1  .71 51 0     0   0 .082  .086  11    0     0    -
expand_false-no-overflow.i 0 910   870   6400 12000 0   0   0 1.1  .65 60 0   0   0 13     8.9   470   .62 0   0 1.4  .86 66 0     0   0 .11   .12   16    0     0    -
fold_false-no-overflow.i 0 900   890   810 10000 0   0   0 1.1  .63 51 0   0   0 6.3   3.7   270   .66 0   0 1.3  .81 57 0     0   0 .10   .10   13    0     .12 -
head_false-no-overflow.i 0 900   890   1200 5800 0   0   0 1.1  .67 49 0   0   0 8.5   4.9   300   .66 0   0 1.2  .73 52 0     0   0 .084  .085  12    0     0    -
logname_false-no-overflow.i 0 900   890   1400 6000 0   0   0 .84 .51 46 0   0   0 7.8   4.6   290   .62 0   0 1.1  .69 50 0     0   0 .11   .11   11    0     0    -
ls-incomplete_false-no-overflow.i 0 910   880   3100 13000 0   0   0 1.3  .73 61 0   0   0 13     8.5   400   .62 0   0 1.5  .94 65 0     0   0 .15   .15   19    0     0    -
mkdir_false-no-overflow.i 0 910   870   6700 12000 0   0   0 1.1  .62 59 0   0   0 13     8.7   460   .62 0   0 1.4  .86 64 0     0   0 .13   .13   15    0     0    -
mkfifo-incomplete_false-no-overflow.i 0 68   58   720 660 0   0   0 92    87    540 0   0   0 7.4   4.4   300   .66 0   0 7.0  130    290 .029 0   0 .88   .89   22    .094 0    -
od_false-no-overflow.i 0 900   870   6600 13000 0   0   0 .99 .58 53 0   0   0 9.5   5.6   300   .62 0   0 1.3  .81 56 0     0   0 .13   .13   18    0     0    -
printf_false-no-overflow.i 0 900   890   1200 6700 0   0   0 1.1  .63 51 0   0   0 11     5.8   300   .66 0   0 1.2  .77 56 0     0   0 .13   .13   13    0     0    -
readlink_false-no-overflow.i 0 910   870   7000 12000 0   0   0 1.4  .79 59 0   0   0 12     8.6   470   .66 0   0 1.4  .85 64 0     0   0 .11   .11   14    0     0    -
realpath_false-no-overflow.i 0 900   890   1300 6800 0   0   0 .85 .51 45 0   0   0 8.1   4.7   290   .66 0   0 1.1  .72 52 0     0   0 .086  .086  11    0     0    -
rm_false-no-overflow.i 0 910   870   6600 12000 0   0   0 1.2  .66 59 0   0   0 13     9.0   480   .62 0   0 1.4  .86 64 0     0   0 .11   .11   15    0     0    -
seq_false-no-overflow.i 0 900   870   7100 11000 0   0   0 1.1  .64 58 0   0   0 13     9.0   470   .62 0   0 1.4  .86 62 0     0   0 .10   .099  14    0     0    -
sleep_false-no-overflow.i 0 7.9 2.7 340 72 0   0   0 .96 .57 46 0   0   0 7.9   4.7   300   .62 0   0 1.1  .72 51 0     0   0 .076  .075  11    0     0    -
stty_false-no-overflow.i 0 900   880   2200 11000 0   0   0 1.3  .75 55 0   0   0 11     5.8   320   .66 0   0 1.3  .82 61 0     0   0 .12   .12   16    0     0    -
sync_false-no-overflow.i 0 57   48   490 590 0   0   0 .79 .47 47 0   0   0 9.3   5.1   300   .66 0   0 1.1  .69 50 0     0   0 .075  .075  11    0     0    -
tac_false-no-overflow.i 0 910   870   6800 13000 0   0   0 1.1  .62 59 0   0   0 13     8.8   460   .66 0   0 1.5  .90 63 0     0   0 .099  .099  14    0     0    -
tee_false-no-overflow.i 0 900   880   3500 9400 0   0   0 1.0  .59 56 0   0   0 11     7.4   390   .66 0   0 1.2  .76 58 0     0   0 .097  .098  14    0     0    -
test-incomplete_false-no-overflow.i 0 33   24   590 360 0   0   0 .76 .47 42 0   0   0 .022 .024 5.6 0    0   0 .96 .63 47 0     0   0 .0051 .0063 .40 0     0    -
touch_false-no-overflow.i 0 910   870   6600 11000 0   0   0 1.2  .70 59 0   0   0 13     8.9   470   .62 0   0 1.5  .89 64 0     0   0 .13   .17   15    0     0    -
uname_false-no-overflow.i 0 910   870   6500 12000 0   0   0 1.1  .66 60 0   0   0 16     10     460   .66 0   0 1.4  .83 65 0     0   0 .096  .098  14    0     0    -
uniq_false-no-overflow.i 0 900   870   6900 11000 0   0   0 1.1  .61 58 0   0   0 13     8.6   440   .66 0   0 1.4  .84 63 0     0   0 .13   .13   14    0     0    -
usleep_false-no-overflow.i 0 900   890   1400 6000 0   0   0 .96 .58 46 0   0   0 8.5   5.0   290   .62 0   0 1.1  .71 50 0     0   0 .074  .074  11    0     0    -
uudecode_false-no-overflow.i 0 3.2 1.1 220 26 0   0   0 .61 .38 40 0   0   0 .022 .022 5.5 0    0   0 1.0  .68 49 0     0   0 .0046 .0060 .40 0     0    -
wc_false-no-overflow.i 0 910   870   6300 11000 0   0   0 1.1  .63 58 0   0   0 13     8.8   460   .62 0   0 1.4  .86 63 0     0   0 .096  .097  15    0     0    -
who_false-no-overflow.i 0 910   870   6900 11000 0   0   0 1.1  .63 60 0   0   0 13     8.8   460   .66 0   0 1.4  .87 63 0     0   0 .10   .10   14    0     0    -
whoami-incomplete_false-no-overflow.i 0 900   890   950 6100 0   0   0 .73 .44 45 0   0   0 8.0   4.8   300   .62 0   0 1.1  .67 50 0     0   0 .082  .083  11    0     .10 -
yes_false-no-overflow.i 0 900   890   1200 6700 0   0   0 .75 .46 46 0   0   0 9.6   5.5   290   .62 0   0 1.0  .69 50 0     0   0 .083  .086  11    0     0    -
basename_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 900   890   1000 5500 0   0   - - - - 0 230     200     2900   .62 0  
chgrp-incomplete_true-no-overflow_false-valid-memtrack.i 0 100   92   750 920 0   0   - - - - 0 8.6   4.7   290   .66 0  
chroot-incomplete_true-no-overflow_true-valid-memsafety.i 0 900   890   1400 6200 0   0   - - - - 0 8.5   4.8   300   .62 0  
cut_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 910   870   6500 12000 0   0   - - - - 0 13     8.8   460   .66 0  
date_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 900   880   3500 10000 0   0   - - - - 0 13     8.1   390   .62 0  
dirname_true-no-overflow_true-valid-memsafety.i 0 900   880   5300 9900 0   0   - - - - 0 200     160     3200   .62 0  
du_true-no-overflow_true-valid-memsafety.i 0 900   880   3300 11000 0   0   - - - - 0 13     8.1   380   .62 0  
echo_true-no-overflow_true-valid-memsafety.i 0 910   890   860 8200 0   0   - - - - 0 8.4   4.7   300   .66 0  
expand_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 910   870   6600 12000 0   0   - - - - 0 13     8.9   470   .62 0  
fold_true-no-overflow_true-valid-memsafety.i 0 900   890   830 10000 0   0   - - - - 0 7.0   3.8   270   .65 0  
head_true-no-overflow_true-valid-memsafety.i 0 600   580   1000 4000 0   0   - - - - 0 8.5   4.9   300   .62 0  
hostid_true-no-overflow_true-valid-memsafety.i 0 540   510   15000 6600 0   0   - - - - 0 .021 .022 5.6 0    0  
logname_true-no-overflow_true-valid-memsafety.i 0 230   220   830 1900 0   0   - - - - 0 8.1   4.4   290   .66 0  
ls-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 900   880   3100 11000 0   0   - - - - 0 13     8.2   400   .66 0  
mkdir_true-no-overflow_true-valid-memsafety.i 0 910   870   6700 12000 0   0   - - - - 0 13     8.8   480   .66 0  
mkfifo-incomplete_true-no-overflow_true-valid-memsafety.i 0 170   160   800 1600 0   0   - - - - 0 10     5.5   290   .66 0  
od_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 910   870   6800 12000 0   0   - - - - 0 10     5.6   310   .62 0  
printf_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 210   200   15000 2000 0   0   - - - - 0 .022 .023 5.6 0    0  
readlink_true-no-overflow_true-valid-memsafety.i 0 900   870   6900 12000 0   0   - - - - 0 8.6   4.7   290   .62 0  
realpath_true-no-overflow_true-valid-memsafety.i 0 900   890   1400 7100 0   0   - - - - 0 8.0   4.5   300   .66 0  
rm_true-no-overflow_true-valid-memsafety.i 0 910   870   6400 11000 0   0   - - - - 0 15     9.7   460   .66 0  
seq_true-no-overflow_true-valid-memsafety.i 0 910   870   6700 11000 0   0   - - - - 0 13     8.5   460   .62 0  
sleep_true-no-overflow_true-valid-memsafety.i 0 7.9 2.6 320 66 0   0   - - - - 0 9.1   4.8   300   .62 0  
stty_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 900   880   2200 10000 0   0   - - - - 0 13     6.7   320   .66 0  
sync_true-no-overflow_true-valid-memsafety.i 0 40   31   620 460 0   0   - - - - 0 8.5   4.9   290   .62 0  
tac_true-no-overflow_true-valid-memsafety.i 0 900   870   6800 12000 0   0   - - - - 0 9.4   5.4   290   .62 0  
tee_true-no-overflow_true-valid-memsafety.i 0 900   880   3600 11000 0   0   - - - - 0 11     7.1   390   .66 0  
test-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 30   21   570 310 0   0   - - - - 0 .026 .028 5.7 0    0  
touch_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 910   880   7500 11000 0   0   - - - - 0 13     8.6   470   .66 0  
uname_true-no-overflow_true-valid-memsafety.i 0 900   870   6600 11000 0   0   - - - - 0 9.1   5.3   290   .62 0  
uniq_true-no-overflow_true-valid-memsafety.i 0 900   870   6800 11000 0   0   - - - - 0 8.5   4.9   300   .62 0  
usleep_true-no-overflow_true-valid-memsafety.i 0 140   130   800 1700 0   0   - - - - 0 8.1   4.5   290   .66 0  
uudecode_true-no-overflow_true-valid-memsafety.i 0 910   870   6500 12000 0   0   - - - - 0 14     9.5   470   .66 0  
wc_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 910   870   6200 11000 0   0   - - - - 0 14     9.0   460   .66 0  
who_true-no-overflow_true-valid-memsafety.i 0 910   870   7000 11000 0   0   - - - - 0 13     9.0   470   .66 0  
whoami-incomplete_true-no-overflow_true-valid-memsafety.i 0 300   290   15000 2300 0   0   - - - - 0 .021 .022 5.6 0    0  
yes_true-no-overflow_true-valid-memsafety.i 0 900   890   1100 5700 0   0   - - - - 0 8.0   4.5   290   .66 0  
sv-benchmarks/c/busybox-1.22.0/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
total 71 0 52000 51000 290000 580000 0   0   34 0 130 110 2300 0   0   34 0 340 210 12000 20 0   34 0 48 150 2200 .029 0   34 0 4.1 4.2 440 .094 .23 37 0 760 560 17000 21 0  
    correct results 0 0 0 0 0 0
        correct true 0 0 0 0 0 0
        correct false 0 0 0 0 0 0
    correct-unconfimed results 1 0 68 58 720 660 0   0   0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0
        correct-unconfirmed false 1 0 68 58 720 660 0   0   0 0 0 0 0
    incorrect results 0 0 0 0 0 0
        incorrect true 0 0 0 0 0 0
        incorrect false 0 0 0 0 0 0
score (71 tasks, max score: 108) 0 0 0 0 0 0
Run set cpa-seq.sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows cpa-seq-validate-violation-witnesses-cpa-seq.sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows uautomizer-validate-violation-witnesses-cpa-seq.sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows cpa-witness2test-validate-violation-witnesses-cpa-seq.sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows fshell-witness2test-validate-violation-witnesses-cpa-seq.sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows uautomizer-validate-correctness-witnesses-cpa-seq.sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows