Tool PeSCo 1.7-svn b8d6131600+ 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* [apollon004; apollon069; apollon137; apollon154] [apollon004; apollon006; apollon021; apollon061; apollon109; apollon155] 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-06 12:44:04 CET 2018-12-08 07:39:30 CET 2018-12-08 12:16:42 CET 2018-12-08 13:32:07 CET 2018-12-12 20:37:42 CET 2018-12-08 09:11:31 CET
Run set pesco.sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows cpa-seq-validate-violation-witnesses-pesco.sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows uautomizer-validate-violation-witnesses-pesco.sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows cpa-witness2test-validate-violation-witnesses-pesco.sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows fshell-witness2test-validate-violation-witnesses-pesco.sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows uautomizer-validate-correctness-witnesses-pesco.sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows
Options -svcomp19-pesco -heap 10000M -stack 2048k -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/pesco.2018-12-06_1244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/pesco.2018-12-06_1244.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/pesco.2018-12-06_1244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/pesco.2018-12-06_1244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/pesco.2018-12-06_1244.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 6200 0   0   0 .95 .56 45 0   0   0 8.5   4.9   300   .66 0   0 1.1  .66 51 0    0   0 .080  .080  11    0     0    -
chroot-incomplete_false-no-overflow.i 0 900   890   1300 6800 0   0   0 1.1  .62 47 0   0   0 8.8   5.1   290   .66 0   0 1.2  .73 51 0    0   0 .076  .098  12    0     0    -
cut_false-no-overflow.i 0 910   870   6800 13000 0   0   0 1.1  .63 61 0   0   0 13     8.8   470   .62 0   0 1.3  .79 64 0    0   0 .13   .14   15    0     0    -
date_false-no-overflow.i 0 900   880   3600 12000 0   0   0 1.0  .60 56 0   0   0 14     8.8   400   .66 0   0 1.3  .82 61 0    0   0 .12   .12   16    0     .15 -
du_false-no-overflow.i 0 900   880   3500 11000 0   0   0 1.0  .60 59 0   0   0 12     7.5   390   .62 0   0 1.4  .85 61 0    0   0 .14   .13   15    0     0    -
echo_false-no-overflow.i 0 910   890   870 7900 0   0   0 .81 .47 48 0   0   0 8.2   4.8   300   .62 0   0 1.1  .72 53 0    0   0 .081  .094  11    0     0    -
expand_false-no-overflow.i 0 910   870   6600 12000 0   0   0 1.1  .63 59 0   0   0 13     8.8   470   .62 0   0 1.4  .83 64 0    0   0 .14   .14   16    0     0    -
fold_false-no-overflow.i 0 900   890   830 11000 0   0   0 .92 .53 52 0   0   0 6.5   3.8   260   .62 0   0 1.2  .76 52 0    0   0 .094  .094  13    0     0    -
head_false-no-overflow.i 0 900   890   1200 5700 0   0   0 .90 .53 50 0   0   0 8.5   4.8   290   .66 0   0 1.2  .73 53 0    0   0 .11   .11   12    0     0    -
logname_false-no-overflow.i 0 900   890   1400 7500 0   0   0 .77 .47 47 0   0   0 8.1   4.6   290   .62 0   0 1.1  .72 50 0    0   0 .11   .11   11    0     0    -
ls-incomplete_false-no-overflow.i 0 900   880   3200 12000 0   0   0 1.3  .72 58 0   0   0 13     8.2   400   .62 0   0 1.4  .84 64 0    0   0 .14   .14   19    0     0    -
mkdir_false-no-overflow.i 0 900   870   6900 11000 0   0   0 1.1  .65 50 0   0   0 10     5.4   300   .62 0   0 1.3  .78 53 0    0   0 .095  .095  13    0     0    -
mkfifo-incomplete_false-no-overflow.i 0 68   58   730 660 0   0   0 92    88    540 0   0   0 8.1   4.6   300   .66 0   0 6.8  130    280 .87 0   0 .87   .89   22    .094 0    -
od_false-no-overflow.i 0 910   870   6900 11000 0   0   0 1.2  .68 62 0   0   0 15     10     490   .66 0   0 1.4  .82 67 0    0   0 .14   .14   19    0     0    -
printf_false-no-overflow.i 0 900   890   1200 5800 0   0   0 .92 .53 53 0   0   0 9.0   5.2   300   .66 0   0 1.2  .76 55 0    0   0 .11   .11   13    0     .13 -
readlink_false-no-overflow.i 0 910   870   6900 12000 0   0   0 1.1  .61 59 0   0   0 13     8.7   460   .62 0   0 1.4  .81 61 0    0   0 .13   .13   14    0     0    -
realpath_false-no-overflow.i 0 900   890   1400 8500 0   0   0 .77 .46 46 0   0   0 8.2   4.7   290   .66 0   0 1.1  .70 52 0    0   0 .073  .073  12    0     0    -
rm_false-no-overflow.i 0 900   870   6600 13000 0   0   0 .99 .58 52 0   0   0 8.8   5.1   290   .62 0   0 1.4  .83 55 0    0   0 .097  .097  14    0     0    -
seq_false-no-overflow.i 0 900   860   6900 12000 0   0   0 .88 .53 51 0   0   0 9.4   5.2   300   .62 0   0 1.2  .77 53 0    0   0 .093  .091  12    0     0    -
sleep_false-no-overflow.i 0 8.1 2.7 340 77 0   0   0 .83 .50 46 0   0   0 8.6   4.9   300   .66 0   0 1.1  .72 52 0    0   0 .083  .084  12    0     0    -
stty_false-no-overflow.i 0 900   880   2200 11000 0   0   0 1.1  .61 56 0   0   0 9.4   5.3   320   .66 0   0 1.3  .80 62 0    0   0 .13   .14   16    0     0    -
sync_false-no-overflow.i 0 55   47   610 580 0   0   0 .78 .46 46 0   0   0 9.2   5.3   300   .62 0   0 1.1  .66 50 0    0   0 .073  .073  12    0     0    -
tac_false-no-overflow.i 0 900   870   6900 10000 0   0   0 .90 .54 51 0   0   0 8.1   4.6   300   .62 0   0 1.2  .74 52 0    0   0 .10   .10   13    0     0    -
tee_false-no-overflow.i 0 900   880   3700 12000 0   0   0 1.1  .65 55 0   0   0 14     8.9   400   .66 0   0 1.3  .78 59 0    0   0 .10   .10   14    0     0    -
test-incomplete_false-no-overflow.i 0 32   23   570 430 0   0   0 .60 .37 42 0   0   0 .025 .026 5.6 0    0   0 .94 .60 48 0    0   0 .0044 .0053 .53 0     0    -
touch_false-no-overflow.i 0 910   870   6700 13000 0   0   0 .89 .53 51 0   0   0 11     5.7   290   .66 0   0 1.2  .75 58 0    0   0 .13   .13   13    0     0    -
uname_false-no-overflow.i 0 910   870   6800 13000 0   0   0 1.0  .60 57 0   0   0 13     8.9   460   .62 0   0 1.3  .80 64 0    0   0 .11   .11   14    0     0    -
uniq_false-no-overflow.i 0 910   870   6900 14000 0   0   0 1.2  .66 60 0   0   0 13     8.7   460   .62 0   0 1.4  .87 64 0    0   0 .11   .11   15    0     0    -
usleep_false-no-overflow.i 0 900   890   1400 5200 0   0   0 .91 .54 48 0   0   0 8.6   5.1   290   .62 0   0 1.1  .72 53 0    0   0 .079  .079  11    0     0    -
uudecode_false-no-overflow.i 0 3.3 1.2 230 29 0   0   0 .60 .37 42 0   0   0 .023 .023 5.6 0    0   0 .95 .60 47 0    0   0 .0038 .0049 .53 0     0    -
wc_false-no-overflow.i 0 910   870   6200 12000 0   0   0 1.1  .61 60 0   0   0 13     8.8   460   .62 0   0 1.4  .83 65 0    0   0 .097  .097  15    0     0    -
who_false-no-overflow.i 0 910   870   7000 13000 0   0   0 1.3  .73 59 0   0   0 13     9.1   460   .66 0   0 1.4  .84 65 0    0   0 .11   .11   14    0     0    -
whoami-incomplete_false-no-overflow.i 0 900   890   1100 6700 0   0   0 .81 .51 47 0   0   0 7.7   4.5   290   .62 0   0 1.1  .72 50 0    0   0 .080  .080  11    0     0    -
yes_false-no-overflow.i 0 900   890   1200 6500 0   0   0 .75 .47 45 0   0   0 7.9   4.5   290   .66 0   0 1.1  .68 50 0    0   0 .078  .078  12    0     0    -
basename_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 900   890   1100 4600 0   0   - - - - 0 240     200     3000   .62 0  
chgrp-incomplete_true-no-overflow_false-valid-memtrack.i 0 110   95   740 1000 0   0   - - - - 0 7.6   4.3   300   .66 0  
chroot-incomplete_true-no-overflow_true-valid-memsafety.i 0 900   890   1200 6300 0   0   - - - - 0 8.5   4.9   290   .62 0  
cut_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 910   870   6700 13000 0   0   - - - - 0 14     9.1   470   .62 0  
date_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 900   880   3500 10000 0   0   - - - - 0 12     7.7   390   .66 0  
dirname_true-no-overflow_true-valid-memsafety.i 0 910   880   5000 10000 0   0   - - - - 0 190     150     3200   .62 0  
du_true-no-overflow_true-valid-memsafety.i 0 900   880   3400 10000 0   0   - - - - 0 12     7.4   390   .66 0  
echo_true-no-overflow_true-valid-memsafety.i 0 910   890   860 8500 0   0   - - - - 0 8.3   4.8   290   .62 0  
expand_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 900   870   6500 13000 0   0   - - - - 0 9.0   5.1   290   .66 0  
fold_true-no-overflow_true-valid-memsafety.i 0 900   890   670 10000 0   0   - - - - 0 6.8   4.0   270   .66 0  
head_true-no-overflow_true-valid-memsafety.i 0 620   610   1100 4000 0   0   - - - - 0 8.3   4.8   300   .66 0  
hostid_true-no-overflow_true-valid-memsafety.i 0 550   520   15000 7600 0   0   - - - - 0 .027 .028 5.7 0    0  
logname_true-no-overflow_true-valid-memsafety.i 0 230   220   840 2300 0   0   - - - - 0 9.1   4.9   290   .66 0  
ls-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 910   880   3100 12000 0   0   - - - - 0 15     9.6   400   .66 0  
mkdir_true-no-overflow_true-valid-memsafety.i 0 900   870   6600 11000 0   0   - - - - 0 11     6.3   320   .66 0  
mkfifo-incomplete_true-no-overflow_true-valid-memsafety.i 0 170   160   810 1700 0   0   - - - - 0 8.1   4.7   290   .66 0  
od_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 910   870   6700 12000 0   0   - - - - 0 17     11     470   .66 0  
printf_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 210   200   15000 1900 0   0   - - - - 0 .021 .021 5.6 0    0  
readlink_true-no-overflow_true-valid-memsafety.i 0 910   870   7100 11000 0   0   - - - - 0 13     8.7   460   .66 0  
realpath_true-no-overflow_true-valid-memsafety.i 0 900   890   1400 8000 0   0   - - - - 0 10     5.4   290   .66 0  
rm_true-no-overflow_true-valid-memsafety.i 0 910   870   6400 11000 0   0   - - - - 0 14     9.2   470   .62 0  
seq_true-no-overflow_true-valid-memsafety.i 0 900   870   7000 12000 0   0   - - - - 0 9.4   5.1   300   .66 0  
sleep_true-no-overflow_true-valid-memsafety.i 0 7.8 2.7 330 76 0   0   - - - - 0 8.0   4.6   290   .66 0  
stty_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 900   880   2200 11000 0   0   - - - - 0 9.8   5.4   320   .66 0  
sync_true-no-overflow_true-valid-memsafety.i 0 40   31   640 430 0   0   - - - - 0 8.4   4.8   290   .62 0  
tac_true-no-overflow_true-valid-memsafety.i 0 900   870   7000 11000 0   0   - - - - 0 14     8.9   460   .62 0  
tee_true-no-overflow_true-valid-memsafety.i 0 900   880   3500 11000 0   0   - - - - 0 14     8.6   390   .66 0  
test-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 30   21   560 330 0   0   - - - - 0 .021 .021 5.6 0    0  
touch_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 910   870   6900 9000 0   0   - - - - 0 14     9.1   470   .66 0  
uname_true-no-overflow_true-valid-memsafety.i 0 900   870   6600 9900 0   0   - - - - 0 9.0   5.1   300   .66 0  
uniq_true-no-overflow_true-valid-memsafety.i 0 900   870   6900 11000 0   0   - - - - 0 13     8.7   470   .62 0  
usleep_true-no-overflow_true-valid-memsafety.i 0 140   130   790 1200 0   0   - - - - 0 8.7   5.0   300   .66 0  
uudecode_true-no-overflow_true-valid-memsafety.i 0 910   870   6600 13000 0   0   - - - - 0 13     8.7   480   .66 0  
wc_false-unreach-call_true-no-overflow_true-valid-memsafety.i 0 910   870   6300 13000 0   0   - - - - 0 15     10     470   .62 0  
who_true-no-overflow_true-valid-memsafety.i 0 910   880   7500 12000 0   0   - - - - 0 13     8.6   460   .66 0  
whoami-incomplete_true-no-overflow_true-valid-memsafety.i 0 310   300   15000 2700 0   0   - - - - 0 .021 .022 5.7 0    0  
yes_true-no-overflow_true-valid-memsafety.i 0 900   890   970 7000 0   0   - - - - 0 8.1   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 590000 0   0   34 0 120 110 2300 0   0   34 0 330 200 11000 20 0   34 0 47 150 2100 .87 0   34 0 4.1 4.2 440 .094 .28 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 730 660 0   0   0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0
        correct-unconfirmed false 1 0 68 58 730 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 pesco.sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows cpa-seq-validate-violation-witnesses-pesco.sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows uautomizer-validate-violation-witnesses-pesco.sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows cpa-witness2test-validate-violation-witnesses-pesco.sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows fshell-witness2test-validate-violation-witnesses-pesco.sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows uautomizer-validate-correctness-witnesses-pesco.sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows