Tool 2LS 0.7.2-sv-comp19 CBMC CBMC Path 5.10 () CPAchecker 1.7-svn 29794 CPAchecker 1.7-svn 29852 DepthK 3.1 DIVINE ESBMC version 6.0.0 64-bit x86_64 linux PeSCo 1.7-svn b8d6131600+ SMACK 1.9.3 symbiotic 6.0.3-77d4af47 ULTIMATE Automizer 0.1.23-635dfa2a ULTIMATE Kojak 0.1.23-635dfa2a ULTIMATE Taipan 0.1.23-635dfa2a VeriAbs 1.3.10
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
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-04 22:44:17 CET 2018-12-04 22:48:40 CET 2018-12-04 22:45:10 CET 2018-12-04 22:41:10 CET 2018-12-05 05:46:16 CET 2018-12-05 09:36:33 CET 2018-12-10 10:00:20 CET 2018-12-06 11:06:04 CET 2018-12-06 11:03:31 CET 2018-12-06 12:44:04 CET 2018-12-07 19:13:55 CET 2018-12-07 21:42:05 CET 2018-12-08 07:42:40 CET 2018-12-08 11:04:44 CET 2018-12-08 14:19:36 CET 2018-12-10 16:50:17 CET
Run set 2ls.[sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety] cbmc.[sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety] cbmc-path.[sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety] cpa-bam-bnb.[sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety] cpa-seq.[sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety] depthk.[sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety] divine-explicit.[sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety] divine-smt.[sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety] esbmc-kind.[sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety] pesco.[sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety] smack.[sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety] symbiotic.[sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety] uautomizer.[sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety] ukojak.[sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety] utaipan.[sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety] veriabs.[sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety]
Options --graphml-witness witness.graphml --graphml-witness witness.graphml --graphml-witness witness.graphml -svcomp19-bam-bnb -disable-java-assertions -heap 10000m -svcomp19 -heap 10000M -benchmark -timelimit 900s --no-symbolic -s kinduction -svcomp19-pesco -heap 10000M -stack 2048k -benchmark -timelimit 900s -w error-witness.graphml --witness witness.graphml --full-output --full-output --full-output
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J)
busybox-1.22.0/basename_false-valid-deref.i valid-deref valid-free valid-memtrack error (134) .25  32 2.9  false(valid-deref) 12    770   130   error (134) 28    340 340   error (1) .49 42 5.5 error 5.2 280 47 false(valid-deref) 350    650 5300   error - divine failed with exitcode 1 1.3   170   19    error - divine failed with exitcode 1 1.3   170   16    false(valid-deref) 540     1000 7900    error 4.9 270 44 disqualified 750   270   9900 false(valid-deref) .65 23 8.6 unknown 820   2600 9300 timeout 900   950 9200 timeout 900   2900 9900 unknown .024 7.5 .12 
busybox-1.22.0/head_false-valid-deref.i valid-deref valid-free valid-memtrack error (6) .40  39 3.8  error (134) 3.5  53   50   error (134) .76 29 10   error (1) .53 42 5.1 error 6.5 300 52 out of memory (false(valid-deref)) 22    15000 250   error - divine failed with exitcode 1 1.2   160   17    error - divine failed with exitcode 1 1.2   160   15    out of memory 22     15000 260    error 6.2 290 58 disqualified 900   9.5 12000 error(unknown, slicing-finished) 1.8  96 19   unknown 8.8 340 61 unknown 8.0 320 58 unknown 9.5 360 72 unknown .020 7.7 .11 
busybox-1.22.0/sleep_false-valid-deref.i valid-deref valid-free valid-memtrack error (134) 1.2   39 11    error (134) .88 27   11   error (134) .63 27 8.5 error (1) .53 44 5.8 error 6.1 310 51 unknown 900    800 10000   error - divine failed with exitcode 1 1.2   160   16    error - divine failed with exitcode 1 1.2   160   16    unknown .22  32 3.2  error 6.0 290 47 disqualified 750   480   7400 error(returned 1, instr-finished) .38 21 3.7 unknown 8.6 360 69 unknown 8.8 340 74 unknown 8.6 360 73 unknown .016 7.4 .11 
busybox-1.22.0/chgrp-incomplete_true-no-overflow_false-valid-memtrack.i valid-deref valid-free valid-memtrack error (134) .35  37 3.3  error (134) .29 13   3.5 error (134) .39 20 5.7 error (1) .51 43 4.9 error 5.9 290 48 false(valid-memtrack) 580    980 7000   error - divine failed with exitcode 1 1.2   160   14    error - divine failed with exitcode 1 1.2   160   15    unknown .20  30 2.5  error 6.2 290 51 disqualified 840   500   8400 false(valid-memtrack) 1.2  22 14   unknown 9.1 360 75 unknown 8.0 340 65 unknown 8.6 350 65 unknown .021 7.5 .12 
busybox-1.22.0/basename_false-unreach-call_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (134) .27  32 2.4  error (42) 880    6400   9800   error (134) 21    290 320   error (1) .50 44 4.5 error 5.1 290 50 unknown 900    810 12000   error - divine failed with exitcode 1 1.3   170   14    error - divine failed with exitcode 1 1.3   170   17    timeout 900     1100 11000    error 4.9 270 44 disqualified 750   200   8600 timeout (verification) 900    470 9300   error (7) 170   2900 2000 timeout 900   1000 11000 error (7) 200   2800 2500 unknown .026 7.3 .14 
busybox-1.22.0/chroot-incomplete_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (134) .66  38 7.7  error (134) .39 16   4.9 error (134) .43 23 6.5 error (1) .52 43 5.1 error 5.8 290 45 unknown 900    2200 7100   error - divine failed with exitcode 1 1.2   160   16    error - divine failed with exitcode 1 1.2   160   15    timeout 900     4400 7900    error 6.0 300 45 disqualified 750   370   6800 timeout (verification) 900    68 14000   unknown 8.9 340 72 unknown 9.1 370 78 unknown 7.6 350 61 unknown .031 7.8 .11 
busybox-1.22.0/cut_false-unreach-call_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (134) 15     89 190    error (134) 7.1  84   87   error (134) 1.3  47 16   error (1) .50 42 4.6 error 7.1 310 55 out of memory (false(no-overflow)) 22    15000 280   error - divine failed with exitcode 1 1.2   170   20    error - divine failed with exitcode 1 1.2   170   19    out of memory 22     15000 230    error 6.3 290 52 disqualified 900   9.6 12000 error(unknown, slicing-finished) 14    180 120   unknown 8.4 350 64 unknown 8.5 340 65 unknown 8.5 330 65 unknown .022 7.1 .20 
busybox-1.22.0/date_false-unreach-call_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (6) .47  47 4.5  error (134) 3.0  130   40   error (134) 2.8  79 39   error (1) .50 44 5.2 error 6.9 310 57 out of memory (false(no-overflow)) 22    15000 280   error - divine failed with exitcode 1 1.2   170   16    error - divine failed with exitcode 1 1.3   170   19    out of memory 22     15000 270    error 7.2 300 54 disqualified 900   9.8 13000 error(unknown, slicing-finished) 16    330 170   unknown 9.4 350 68 unknown 8.4 340 69 unknown 9.0 330 77 unknown .021 7.4 .13 
busybox-1.22.0/dirname_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (134) .24  31 2.6  out of memory 590    13000   6700   error (134) 1.1  32 15   error (1) .52 44 5.0 error 5.1 290 42 unknown 900    920 11000   error - divine failed with exitcode 1 1.3   170   17    error - divine failed with exitcode 1 1.3   170   16    timeout 900     4400 11000    error 5.1 290 41 disqualified 880   400   9500 error(unknown, cex-confirmation) .65 27 8.1 timeout 900   3200 11000 timeout 900   940 8700 timeout 900   2300 12000 unknown .046 7.4 .11 
busybox-1.22.0/du_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (134) 7.9   72 96    error (134) 62    220   710   error (134) .70 40 8.4 error (1) .55 43 4.7 error 6.7 300 56 out of memory (false(no-overflow)) 22    15000 240   error - divine failed with exitcode 1 1.3   160   15    error - divine failed with exitcode 1 1.3   160   17    out of memory 22     15000 320    error 6.8 310 59 disqualified 750   3300   8900 error(unknown, slicing-finished) 41    210 440   unknown 9.4 370 82 unknown 8.9 360 77 unknown 8.6 320 63 unknown .023 7.8 .18 
busybox-1.22.0/echo_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (134) .55  38 6.6  error (42) 880    7200   7200   error (134) .50 22 7.1 error (1) .50 42 4.5 error 6.0 290 53 unknown 900    1700 10000   error - divine failed with exitcode 1 1.2   160   15    error - divine failed with exitcode 1 1.2   160   18    unknown .23  32 2.8  error 6.0 300 43 disqualified 750   170   11000 timeout (verification) 900    680 7900   unknown 7.7 330 71 unknown 9.0 340 71 unknown 8.5 360 72 unknown .025 7.7 .088
busybox-1.22.0/expand_false-unreach-call_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (134) 35     130 470    error (134) 34    210   460   error (134) .51 29 6.9 error (1) .53 43 4.9 error 7.0 300 63 out of memory (false(no-overflow)) 24    15000 290   error - divine failed with exitcode 1 1.2   170   16    error - divine failed with exitcode 1 1.2   170   17    out of memory 22     15000 280    error 6.9 310 58 disqualified 900   9.5 13000 error(unknown, slicing-finished) 25    270 220   unknown 8.6 360 70 unknown 8.9 370 72 unknown 9.2 360 70 unknown .025 7.8 .15 
busybox-1.22.0/fold_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (134) 6.2   57 88    error (134) 3.7  50   49   error (134) .45 26 5.6 error (1) .52 43 5.2 error 6.5 300 57 out of memory (false(no-overflow)) 22    15000 270   error - divine failed with exitcode 1 1.3   160   15    error - divine failed with exitcode 1 1.2   160   14    out of memory 22     15000 280    error 6.5 300 58 disqualified 900   9.7 11000 error(unknown, slicing-finished) 8.9  170 77   unknown 9.1 360 80 unknown 8.9 350 75 unknown 8.7 340 68 unknown .021 7.6 .13 
busybox-1.22.0/head_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (6) .38  40 4.4  error (134) 3.5  54   44   error (134) .74 27 9.3 error (1) .52 42 5.1 error 6.6 300 60 out of memory (false(no-overflow)) 22    15000 310   error - divine failed with exitcode 1 1.2   160   17    error - divine failed with exitcode 1 1.7   160   30    out of memory 22     15000 260    error 6.4 300 56 disqualified 900   9.6 12000 error(unknown, slicing-finished) 1.8  97 19   unknown 8.3 340 72 unknown 8.5 330 67 unknown 8.4 340 64 unknown .050 6.9 .12 
busybox-1.22.0/hostid_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (134) .26  34 2.2  out of memory 570    13000   6600   error (134) .26 16 3.1 error (1) .52 42 6.2 error 5.1 280 45 unknown 900    670 10000   error - divine failed with exitcode 1 1.3   170   17    error - divine failed with exitcode 1 1.3   170   21    timeout 900     1600 9200    error 5.1 280 47 disqualified 880   400   8100 timeout (verification) 900    2000 13000   timeout 900   2200 11000 timeout 900   840 11000 timeout 900   1800 10000 unknown .026 6.9 .10 
busybox-1.22.0/logname_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (134) .34  37 4.0  error (134) .25 14   3.7 error (134) .30 19 2.9 error (1) .48 43 5.1 error 5.8 300 55 false(valid-deref) 830    1500 7200   error - divine failed with exitcode 1 1.2   160   15    error - divine failed with exitcode 1 1.2   160   18    unknown .19  30 2.7  error 5.5 280 46 disqualified 890   440   9200 error(unknown, cex-confirmation) .67 24 8.2 unknown 8.6 370 69 unknown 8.6 330 69 unknown 8.8 370 76 unknown .022 7.3 .11 
busybox-1.22.0/ls-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (134) 300     340 3000    error (134) 3.6  55   45   error (134) 1.1  58 13   error (1) .53 42 4.9 error 8.2 330 70 out of memory (false(no-overflow)) 23    15000 300   error - divine failed with exitcode 1 1.3   170   20    error - divine failed with exitcode 1 1.3   170   16    out of memory 22     15000 260    error 8.6 370 74 disqualified 750   3500   9400 error(unknown, slicing-finished) 210    1000 1900   error (7) 18   350 140 error (7) 19   360 160 error (7) 18   360 150 unknown .026 7.7 .091
busybox-1.22.0/mkdir_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (134) 3.1   45 31    error 880    1100   3300   error (134) 2.4  64 31   error (1) .51 43 5.3 error 6.5 300 52 out of memory (false(no-overflow)) 22    15000 260   error - divine failed with exitcode 1 1.2   160   16    error - divine failed with exitcode 1 1.3   160   17    out of memory 22     15000 300    error 7.0 310 60 disqualified 900   9.9 14000 error(unknown, slicing-finished) 14    180 120   unknown 8.8 360 69 unknown 9.2 340 75 unknown 8.7 350 66 unknown .021 7.7 .15 
busybox-1.22.0/mkfifo-incomplete_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (134) .31  36 3.3  error (134) .28 14   3.9 error (134) .22 17 2.6 error (1) .51 42 4.8 error 5.4 290 40 unknown 900    1700 8500   error - divine failed with exitcode 1 1.3   170   17    error - divine failed with exitcode 1 1.3   170   18    unknown .19  30 2.7  error 5.8 280 49 disqualified 750   450   7500 timeout (verification) 900    64 11000   unknown 8.8 350 68 unknown 8.7 330 73 unknown 8.6 350 69 unknown .023 7.6 .10 
busybox-1.22.0/od_false-unreach-call_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack timeout 900     670 11000    error 880    670   4700   error (134) 3.1  90 42   error (1) .51 43 4.6 error 9.1 390 79 out of memory (false(no-overflow)) 22    15000 250   error - divine failed with exitcode 1 1.3   170   15    error - divine failed with exitcode 1 1.3   170   16    out of memory 22     15000 280    error 8.4 380 75 disqualified 900   10   13000 error(unknown, slicing-finished) 90    860 670   unknown 9.4 350 80 unknown 9.8 360 79 unknown 11   370 81 unknown .045 6.7 .080
busybox-1.22.0/printf_false-unreach-call_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (6) .57  43 4.8  error (134) 23    110   290   error (134) .46 25 4.9 error (1) .51 43 5.1 error 6.5 300 60 unknown 900    2000 7600   error - divine failed with exitcode 1 1.3   160   17    error - divine failed with exitcode 1 1.2   160   15    unknown .24  36 3.0  error 6.4 280 56 disqualified 750   320   9800 error(returned 1, instr-finished) 2.5  110 29   unknown 8.8 370 79 unknown 8.1 320 66 unknown 9.0 370 71 unknown .028 7.3 .13 
busybox-1.22.0/readlink_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (134) 3.2   41 35    error (134) .82 27   13   error (134) 1.9  53 25   error (1) .53 42 4.9 error 6.7 300 52 out of memory (false(no-overflow)) 22    15000 260   error - divine failed with exitcode 1 1.2   160   15    error - divine failed with exitcode 1 1.2   160   15    out of memory 22     15000 290    error 6.5 300 54 disqualified 890   760   6400 error(unknown, slicing-finished) 5.6  95 66   unknown 8.6 350 79 unknown 9.0 360 71 unknown 8.6 360 65 unknown .030 7.1 .10 
busybox-1.22.0/realpath_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (134) .35  37 3.9  error (134) .30 14   5.4 error (134) .38 20 4.7 error (1) .53 42 4.8 error 5.5 280 43 unknown 900    1600 8700   error - divine failed with exitcode 1 1.2   160   20    error - divine failed with exitcode 1 1.2   160   20    unknown .22  31 2.2  error 6.1 290 58 disqualified 750   430   7100 timeout (verification) 900    76 11000   unknown 8.7 350 63 unknown 8.4 350 75 unknown 9.0 360 78 unknown .024 7.6 .11 
busybox-1.22.0/rm_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (134) 7.2   68 93    error 880    270   12000   error (134) 1.2  45 17   error (1) .52 42 4.8 error 6.8 300 57 out of memory (false(no-overflow)) 22    15000 260   error - divine failed with exitcode 1 1.2   160   19    error - divine failed with exitcode 1 1.2   160   17    out of memory 22     15000 260    error 6.9 300 57 disqualified 140   580   1300 error(unknown, slicing-finished) 44    210 450   unknown 9.2 360 79 unknown 8.9 360 81 unknown 8.4 320 71 unknown .026 7.6 .13 
busybox-1.22.0/seq_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (134) 1.8   40 22    error (134) .71 21   10   error (134) 1.1  41 12   error (1) .50 42 4.8 error 6.4 310 56 out of memory (false(no-overflow)) 22    15000 270   error - divine failed with exitcode 1 1.2   160   15    error - divine failed with exitcode 1 1.2   160   20    out of memory 22     15000 260    error 6.3 310 60 disqualified 900   9.2 13000 error(returned 1, instr-finished) 4.5  83 53   unknown 8.5 360 78 unknown 8.7 360 82 unknown 8.3 330 64 unknown .021 7.7 .094
busybox-1.22.0/sleep_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (134) 1.2   39 11    error (134) .90 27   12   error (134) .67 26 9.8 error (1) .51 42 4.8 error 6.2 300 50 unknown 900    870 12000   error - divine failed with exitcode 1 1.2   160   16    error - divine failed with exitcode 1 1.3   160   13    unknown .23  32 2.6  error 5.9 280 55 disqualified 750   480   8500 error(returned 1, instr-finished) .35 21 3.5 unknown 8.9 360 77 unknown 8.8 370 72 unknown 8.3 360 79 unknown .023 7.6 .11 
busybox-1.22.0/stty_false-unreach-call_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (134) 78     210 790    error (134) 66    180   800   error (134) 1.3  63 18   error (1) .51 43 4.8 error 10   510 100 out of memory (false(no-overflow)) 23    15000 270   error - divine failed with exitcode 1 1.3   160   19    error - divine failed with exitcode 1 1.3   160   18    out of memory 22     15000 310    error 10   510 84 disqualified 760   660   5500 timeout (instrumentation) 900    520 12000   unknown 9.5 350 77 unknown 10   380 85 unknown 9.8 370 83 unknown .025 7.8 .092
busybox-1.22.0/sync_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (134) .30  35 3.2  error (134) .21 11   2.6 error (134) .37 21 4.6 error (1) .52 42 5.0 error 5.4 290 45 unknown 900    610 13000   error - divine failed with exitcode 1 1.3   170   18    error - divine failed with exitcode 1 1.3   170   18    unknown .19  30 2.7  error 5.3 290 49 disqualified 890   460   7800 timeout (verification) 900    160 8300   unknown 8.1 350 65 unknown 7.8 340 68 unknown 8.1 340 72 unknown .025 7.6 .12 
busybox-1.22.0/tac_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (134) 6.2   57 68    error (134) 2.6  44   35   error (134) 1.0  40 15   error (1) .49 42 5.2 error 6.3 300 51 out of memory (false(no-overflow)) 22    15000 290   error - divine failed with exitcode 1 1.2   160   15    error - divine failed with exitcode 1 1.2   160   16    out of memory 22     15000 300    error 6.7 300 55 disqualified 750   710   7100 error(unknown, slicing-finished) 7.1  110 86   unknown 9.1 370 73 unknown 8.6 360 71 unknown 8.0 340 65 unknown .023 7.6 .13 
busybox-1.22.0/tee_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (134) 4.0   49 47    error (134) 1.2  32   15   error (134) 1.1  46 14   error (1) .52 42 5.6 error 6.5 290 56 out of memory (false(no-overflow)) 22    15000 280   error - divine failed with exitcode 1 1.2   160   18    error - divine failed with exitcode 1 1.2   160   15    out of memory 22     15000 320    error 6.4 300 61 disqualified 750   3300   9200 error(unknown, slicing-finished) 6.2  110 66   unknown 8.0 320 66 unknown 8.7 360 71 unknown 8.0 330 71 unknown .025 7.2 .15 
busybox-1.22.0/test-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (134) 37     130 380    error 880    690   5900   error (134) .99 35 15   error (1) .52 43 4.5 error 6.8 300 66 unknown 900    15000 5900   error - divine failed with exitcode 1 1.2   160   15    error - divine failed with exitcode 1 1.2   160   16    unknown .24  37 2.8  error 6.6 290 61 disqualified 750   490   7500 error(unknown, slicing-finished) 2.7  87 21   unknown 9.3 360 80 unknown 9.1 350 83 unknown 8.7 340 71 unknown .026 7.3 .11 
busybox-1.22.0/touch_false-unreach-call_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (134) 6.5   67 69    error (134) 2.8  110   36   error (134) 2.5  69 31   error (1) .53 44 5.8 error 7.2 310 56 out of memory (false(no-overflow)) 22    15000 250   error - divine failed with exitcode 1 1.3   160   17    error - divine failed with exitcode 1 1.2   160   17    out of memory 22     15000 290    error 6.8 290 63 disqualified 900   9.8 11000 error(unknown, slicing-finished) 11    270 100   unknown 9.0 320 75 unknown 8.6 330 69 unknown 9.1 370 71 unknown .022 7.3 .11 
busybox-1.22.0/uname_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (134) 1.9   41 21    error (134) 1.1  120   16   error (134) 2.3  62 29   error (1) .53 44 5.1 error 6.7 310 56 out of memory (false(no-overflow)) 22    15000 250   error - divine failed with exitcode 1 1.2   160   16    error - divine failed with exitcode 1 1.3   160   16    out of memory 22     15000 300    error 6.9 300 58 disqualified 890   760   8800 error(unknown, slicing-finished) 5.7  110 54   unknown 8.6 370 67 unknown 8.5 360 70 unknown 8.6 360 69 unknown .022 7.6 .091
busybox-1.22.0/uniq_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (134) 5.8   58 67    error (134) 2.0  39   25   error (134) 1.2  43 15   error (1) .50 42 5.3 error 6.6 310 59 out of memory (false(no-overflow)) 22    15000 270   error - divine failed with exitcode 1 1.2   170   15    error - divine failed with exitcode 1 1.2   170   20    out of memory 22     15000 290    error 6.8 300 52 disqualified 900   9.7 11000 error(unknown, slicing-finished) 9.7  140 110   unknown 9.0 360 76 unknown 8.1 340 67 unknown 8.3 330 70 unknown .030 7.5 .095
busybox-1.22.0/usleep_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (134) .48  37 6.1  error (134) .25 13   3.5 error (134) .73 26 9.2 error (1) .53 43 5.3 error 5.8 300 48 false(valid-deref) 85    350 990   error - divine failed with exitcode 1 1.2   160   17    error - divine failed with exitcode 1 1.2   160   15    unknown .23  31 2.3  error 5.7 290 47 disqualified 750   410   9700 timeout (verification) 900    180 8000   unknown 8.6 360 78 unknown 7.9 320 62 unknown 7.9 340 65 unknown .024 7.5 .11 
busybox-1.22.0/uudecode_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (134) 12     81 170    error (134) 6.1  85   69   error (134) 2.0  58 29   error (1) .49 42 5.2 error 7.0 310 63 out of memory (false(no-overflow)) 22    15000 270   error - divine failed with exitcode 1 1.2   160   16    error - divine failed with exitcode 1 1.3   160   16    out of memory 22     15000 290    error 7.0 310 55 disqualified 900   9.8 13000 error(unknown, slicing-finished) 22    250 180   unknown 8.8 350 72 unknown 8.5 350 81 unknown 9.0 330 83 unknown .021 7.6 .089
busybox-1.22.0/wc_false-unreach-call_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (6) .37  42 4.5  error 880    580   6000   error (134) .45 25 6.2 error (1) .50 43 5.2 error 6.5 300 50 out of memory (false(no-overflow)) 22    15000 250   error - divine failed with exitcode 1 1.2   160   14    error - divine failed with exitcode 1 1.2   160   17    out of memory 22     15000 240    error 6.2 300 57 disqualified 890   840   9800 error(unknown, slicing-finished) 7.9  130 68   unknown 8.6 340 72 unknown 8.4 330 75 unknown 8.9 370 66 unknown .039 7.2 .13 
busybox-1.22.0/who_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (134) 2.1   42 21    error (134) .78 27   12   error (134) 1.7  50 21   error (1) .50 42 4.8 error 6.5 300 51 out of memory (false(no-overflow)) 22    15000 270   error - divine failed with exitcode 1 1.3   170   16    error - divine failed with exitcode 1 1.2   170   16    out of memory 23     15000 350    error 6.3 300 55 disqualified 750   720   9500 error(unknown, slicing-finished) 5.9  100 58   unknown 8.6 350 64 unknown 8.4 320 70 unknown 9.1 360 75 unknown .022 7.2 .12 
busybox-1.22.0/whoami-incomplete_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (134) .35  37 3.2  error (134) .22 12   3.3 error (134) .33 19 3.2 error (1) .54 43 5.1 error 5.5 280 53 unknown 900    700 9600   error - divine failed with exitcode 1 1.2   160   16    error - divine failed with exitcode 1 1.2   160   15    unknown .20  31 2.3  error 5.9 290 46 disqualified 890   470   10000 timeout (verification) 900    150 8700   unknown 8.4 360 64 unknown 8.7 360 73 unknown 8.5 330 66 unknown .023 7.8 .084
busybox-1.22.0/yes_true-no-overflow_true-valid-memsafety.i valid-deref valid-free valid-memtrack error (134) .34  37 3.5  error (134) .24 12   3.1 error (134) .30 19 3.9 error (1) .51 43 4.4 error 5.8 300 50 unknown 360    1200 3800   error - divine failed with exitcode 1 1.2   160   17    error - divine failed with exitcode 1 1.2   160   19    unknown .21  30 2.5  error 6.0 290 53 disqualified 760   520   8900 timeout (verification) 900    110 11000   unknown 8.1 320 63 unknown 7.5 330 65 unknown 7.9 350 65 unknown .025 7.6 .099
busybox-1.22.0/chgrp-incomplete_false-no-overflow.i no-overflow error (134) .30  37 3.2  error (134) .23 12   2.9 error (134) .20 18 2.2 error (1) .52 44 5.2 timeout 900   1700 7600 unknown 900    800 11000   unknown .033 4.6 .22 unknown .029 4.7 .19 unknown 3.0   140 45    timeout 900   1700 6200 disqualified 880   670   8000 timeout (verification) 900    140 8200   unknown 8.4 350 70 unknown 7.6 320 58 unknown 8.3 360 67 unknown .023 7.5 .16 
busybox-1.22.0/chroot-incomplete_false-no-overflow.i no-overflow error (134) .46  38 4.8  error (134) .28 14   3.6 error (134) .97 68 12   error (1) .50 42 5.0 timeout 900   1300 5900 unknown 900    1700 9200   unknown .037 4.8 .15 unknown .031 4.6 .20 unknown 3.0   150 46    timeout 900   1300 6800 disqualified 880   690   7100 timeout (verification) 900    59 11000   unknown 8.5 350 62 unknown 9.2 350 74 unknown 8.6 330 69 unknown .023 7.4 .14 
busybox-1.22.0/cut_false-no-overflow.i no-overflow error (134) 10     50 91    error (134) 5.8  76   69   error (134) .79 75 9.4 error (1) .49 43 5.1 timeout 900   6700 11000 out of memory 22    15000 270   unknown .046 4.6 .19 unknown .055 4.6 .20 out of memory 22     15000 270    timeout 910   6800 13000 disqualified 880   730   6600 error(unknown, slicing-finished) 1.7  81 17   unknown 8.6 350 66 unknown 9.1 330 65 unknown 9.2 350 77 unknown .022 7.5 .097
busybox-1.22.0/date_false-no-overflow.i no-overflow error (6) .43  48 3.7  error (134) 2.4  120   28   error (134) .71 55 8.4 error (1) .53 42 7.8 timeout 900   3400 11000 out of memory 22    15000 340   unknown .031 4.6 .19 unknown .030 4.6 .18 out of memory 22     15000 250    timeout 900   3600 12000 disqualified 880   4000   11000 error(unknown, slicing-finished) 2.9  170 25   unknown 9.2 370 71 unknown 9.3 360 75 unknown 9.3 350 74 unknown .024 7.6 .087
busybox-1.22.0/du_false-no-overflow.i no-overflow error (134) 5.8   46 54    error (134) 52    200   480   error (134) .48 39 5.7 error (1) .53 44 5.4 timeout 900   3300 11000 out of memory 23    15000 310   unknown .028 4.7 .18 unknown .029 4.6 .21 out of memory 22     15000 290    timeout 900   3500 11000 disqualified 880   3700   11000 error(unknown, slicing-finished) 3.1  120 20   unknown 8.8 320 67 unknown 9.4 360 76 unknown 8.8 350 72 unknown .022 7.9 .090
busybox-1.22.0/echo_false-no-overflow.i no-overflow error (134) .41  38 5.3  error (42) 880    3100   5700   error (134) .66 86 7.9 error (1) .52 42 4.7 timeout 910   850 13000 unknown 900    1600 9700   unknown .028 4.7 .19 unknown .031 4.6 .21 unknown 4.2   240 66    timeout 910   870 7900 disqualified 880   570   6900 timeout (verification) 900    460 6600   unknown 8.1 340 64 unknown 8.4 330 67 unknown 8.5 360 73 unknown .021 7.5 .11 
busybox-1.22.0/expand_false-no-overflow.i no-overflow error (134) 24     71 190    error (134) 29    200   420   error (134) .38 33 4.4 error (1) .52 42 4.6 timeout 910   6400 12000 out of memory 22    15000 290   unknown .055 4.7 .16 unknown .028 4.5 .25 out of memory 22     15000 270    timeout 910   6600 12000 disqualified 880   840   6700 error(unknown, slicing-finished) 2.9  100 21   unknown 8.8 360 73 unknown 9.0 360 75 unknown 8.9 330 67 unknown .031 7.7 .13 
busybox-1.22.0/fold_false-no-overflow.i no-overflow error (134) 4.7   42 32    error (134) 2.9  45   37   error (134) .35 29 3.8 error (1) .51 44 4.9 timeout 900   810 10000 out of memory 22    15000 270   unknown .037 4.6 .26 unknown .032 4.6 .17 out of memory 22     15000 280    timeout 900   830 11000 disqualified 880   690   8900 error(unknown, slicing-finished) 1.1  60 13   unknown 9.1 350 75 unknown 8.9 350 68 unknown 9.1 370 71 unknown .021 7.1 .11 
busybox-1.22.0/head_false-no-overflow.i no-overflow error (6) .37  40 4.1  error (134) 2.9  48   37   error (134) .59 51 7.0 error (1) .51 42 5.2 timeout 900   1200 5800 out of memory 22    15000 270   unknown .036 4.6 .21 unknown .052 4.6 .17 out of memory 22     15000 290    timeout 900   1200 5700 disqualified 880   490   8700 error(unknown, slicing-finished) .63 54 7.1 unknown 9.2 350 67 unknown 8.7 330 73 unknown 8.1 320 61 unknown .024 7.7 .083
busybox-1.22.0/logname_false-no-overflow.i no-overflow error (134) .28  37 2.8  error (134) .20 13   2.5 error (134) .21 18 2.3 error (1) .51 42 5.4 timeout 900   1400 6000 witness invalid (false(no-overflow)) 190    640 2500   unknown .028 4.6 .22 unknown .028 4.6 .19 unknown 3.0   150 39    timeout 900   1400 7500 disqualified 880   660   7200 timeout (verification) 900    51 13000   unknown 9.0 350 63 unknown 8.5 350 77 unknown 8.6 350 74 unknown .021 7.6 .16 
busybox-1.22.0/ls-incomplete_false-no-overflow.i no-overflow error (134) 190     180 1500    error (134) 2.6  45   38   error (134) 1.1  120 13   error (1) .49 43 5.2 timeout 910   3100 13000 out of memory 22    15000 260   unknown .042 4.7 .22 unknown .026 4.6 .20 out of memory 22     15000 310    timeout 900   3200 12000 disqualified 880   3900   10000 error(unknown, slicing-finished) 19    310 100   error (7) 9.9 340 88 error (7) 10   350 79 error (7) 10   370 92 unknown .018 7.5 .15 
busybox-1.22.0/mkdir_false-no-overflow.i no-overflow error (134) 2.2   44 19    error 880    1600   4800   error (134) .54 33 7.5 error (1) .53 43 5.3 timeout 910   6700 12000 out of memory 22    15000 270   unknown .032 4.6 .20 unknown .026 4.6 .25 out of memory 22     15000 250    timeout 900   6900 11000 disqualified 880   670   6400 error(unknown, slicing-finished) 1.2  81 16   unknown 8.9 350 82 unknown 9.0 340 74 unknown 9.4 360 78 unknown .024 7.7 .11 
busybox-1.22.0/mkfifo-incomplete_false-no-overflow.i no-overflow error (134) .31  36 2.0  error (134) .23 12   2.4 error (134) .20 16 2.0 error (1) .50 43 5.0 false(no-overflow) 68   720 660 unknown 900    2000 11000   unknown .046 4.6 .18 unknown .027 4.6 .27 unknown 3.0   140 39    false(no-overflow) 68   730 660 disqualified 880   680   7500 timeout (verification) 900    52 11000   unknown 7.9 350 64 unknown 8.6 360 74 unknown 8.5 360 63 unknown .025 7.6 .098
busybox-1.22.0/od_false-no-overflow.i no-overflow error (134) 540     340 5500    error 880    740   4800   error (134) .79 61 8.2 error (1) .47 41 4.8 timeout 900   6600 13000 out of memory 22    15000 280   unknown .028 4.6 .25 unknown .031 4.6 .16 out of memory 22     15000 250    timeout 910   6900 11000 disqualified 880   1100   6100 error(unknown, slicing-finished) 13    350 68   unknown 8.9 330 77 unknown 10   360 89 unknown 10   350 76 unknown .027 7.6 .099
busybox-1.22.0/printf_false-no-overflow.i no-overflow error (6) .48  43 5.1  error (134) 18    98   230   error (134) .25 24 2.8 error (1) .54 43 5.4 timeout 900   1200 6700 unknown 900    4000 7100   unknown .027 4.6 .27 unknown .054 4.6 .14 unknown 3.0   150 35    timeout 900   1200 5800 disqualified 880   490   8500 error(returned 1, before-instr) .27 17 3.4 unknown 8.2 330 65 unknown 9.2 360 71 unknown 8.8 360 76 unknown .023 7.5 .12 
busybox-1.22.0/readlink_false-no-overflow.i no-overflow error (134) 2.1   41 26    error (134) .64 24   7.5 error (134) .84 69 11   error (1) .49 42 5.0 timeout 910   7000 12000 out of memory 23    15000 270   unknown .030 4.6 .20 unknown .030 4.6 .20 out of memory 22     15000 280    timeout 910   6900 12000 disqualified 880   690   6800 error(unknown, slicing-finished) .95 54 9.1 unknown 8.1 320 73 unknown 8.5 330 76 unknown 8.6 360 70 unknown .022 7.6 .092
busybox-1.22.0/realpath_false-no-overflow.i no-overflow error (134) .30  37 2.4  error (134) .23 13   2.9 error (134) .95 61 11   error (1) .50 42 5.2 timeout 900   1300 6800 unknown 900    2100 7800   unknown .035 4.6 .14 unknown .033 4.8 .27 unknown 3.0   140 38    timeout 900   1400 8500 disqualified 880   680   8100 timeout (verification) 900    72 13000   unknown 8.0 350 69 unknown 8.5 360 69 unknown 8.5 330 70 unknown .021 7.3 .12 
busybox-1.22.0/rm_false-no-overflow.i no-overflow error (134) 5.2   45 41    error (134) 880    310   10000   error (134) .71 70 9.1 error (1) .51 42 6.0 timeout 910   6600 12000 out of memory 22    15000 260   unknown .030 4.5 .17 unknown .026 4.7 .24 out of memory 22     15000 260    timeout 900   6600 13000 disqualified 880   690   7700 error(unknown, slicing-finished) 1.9  110 16   unknown 8.9 360 70 unknown 8.5 330 68 unknown 9.1 360 78 unknown .022 7.8 .17 
busybox-1.22.0/seq_false-no-overflow.i no-overflow error (134) 1.1   41 12    error (134) .52 16   7.3 error (134) .47 30 5.8 error (1) .51 43 5.2 timeout 900   7100 11000 out of memory 22    15000 280   unknown .029 4.6 .27 unknown .055 4.6 .18 out of memory 22     15000 280    timeout 900   6900 12000 disqualified 880   680   9900 error(returned 1, before-instr) .27 18 2.8 unknown 8.5 340 67 unknown 8.6 360 72 unknown 9.1 360 80 unknown .021 7.6 .099
busybox-1.22.0/sleep_false-no-overflow.i no-overflow error (134) .73  38 8.2  error (134) .69 24   9.6 error (134) .71 85 9.8 error (1) .51 43 5.1 unknown 7.9 340 72 unknown 890    670 9900   unknown .029 4.6 .21 unknown .027 4.6 .17 unknown 3.5   170 52    unknown 8.1 340 77 disqualified 880   490   8000 error(returned 1, before-instr) .25 17 3.1 unknown 8.0 340 69 unknown 8.9 360 74 unknown 8.7 360 67 unknown .035 7.7 .12 
busybox-1.22.0/stty_false-no-overflow.i no-overflow error (134) 47     110 500    error (134) 57    160   640   error (134) 3.4  180 46   error (1) .54 44 5.0 timeout 900   2200 11000 out of memory 23    15000 260   unknown .031 4.6 .16 unknown .046 4.6 .15 out of memory 22     15000 260    timeout 900   2200 11000 disqualified 880   1400   5800 timeout (verification) 900    170 11000   unknown 9.4 360 79 unknown 9.3 340 78 unknown 10   380 83 unknown .024 7.8 .070
busybox-1.22.0/sync_false-no-overflow.i no-overflow error (134) .27  35 2.5  error (134) .16 10   1.7 error (134) .27 16 2.8 error (1) .48 42 4.6 unknown 57   490 590 unknown 900    840 13000   unknown .031 4.6 .23 unknown .030 4.6 .28 unknown 3.0   140 41    unknown 55   610 580 disqualified 880   690   7000 timeout (verification) 900    130 7600   unknown 9.5 360 64 unknown 8.5 360 70 unknown 8.7 350 72 unknown .019 7.5 .14 
busybox-1.22.0/tac_false-no-overflow.i no-overflow error (134) 4.9   41 33    error (134) 2.1  39   24   error (134) .69 55 10   error (1) .49 43 4.8 timeout 910   6800 13000 out of memory 22    15000 260   unknown .031 4.6 .21 unknown .026 4.6 .26 out of memory 22     15000 330    timeout 900   6900 10000 disqualified 880   800   9300 error(unknown, slicing-finished) .80 46 9.5 unknown 8.4 330 68 unknown 8.9 340 73 unknown 9.3 350 76 unknown .016 7.2 .089
busybox-1.22.0/tee_false-no-overflow.i no-overflow error (6) .33  41 3.1  error (134) .87 27   12   error (134) 1.3  110 17   error (1) .50 41 4.5 timeout 900   3500 9400 out of memory 22    15000 300   unknown .029 4.6 .21 unknown .034 4.6 .20 out of memory 22     15000 290    timeout 900   3700 12000 disqualified 880   3700   11000 error(unknown, slicing-finished) .78 48 9.4 unknown 7.7 330 67 unknown 8.7 360 69 unknown 8.6 340 70 unknown .023 7.8 .072
busybox-1.22.0/test-incomplete_false-no-overflow.i no-overflow error (134) 23     68 220    error 880    670   6100   error (134) 2.8  170 37   error (1) .51 43 5.6 exception 33   590 360 unknown 900    15000 7800   unknown .038 4.6 .15 unknown .030 4.6 .21 unknown 3.3   170 41    exception 32   570 430 disqualified 880   580   8700 error(unknown, slicing-finished) .83 60 8.6 unknown 9.3 360 78 unknown 9.0 360 65 unknown 8.4 350 71 unknown .025 7.6 .11 
busybox-1.22.0/touch_false-no-overflow.i no-overflow error (134) 4.5   46 40    error (134) 2.2  110   28   error (134) .60 35 7.3 error (1) .53 44 5.5 timeout 910   6600 11000 out of memory 22    15000 320   unknown .029 4.6 .19 unknown .026 4.6 .37 out of memory 22     15000 240    timeout 910   6700 13000 disqualified 880   700   7400 error(unknown, slicing-finished) 1.6  120 19   unknown 9.2 370 79 unknown 8.3 340 67 unknown 9.2 350 82 unknown .022 7.6 .17 
busybox-1.22.0/uname_false-no-overflow.i no-overflow error (134) 1.1   42 14    error (134) .81 120   9.8 error (134) .52 32 7.7 error (1) .51 42 4.7 timeout 910   6500 12000 out of memory 22    15000 300   unknown .025 4.6 .23 unknown .048 4.6 .30 out of memory 22     15000 270    timeout 910   6800 13000 disqualified 880   630   8400 error(unknown, slicing-finished) .77 49 9.1 unknown 8.5 350 68 unknown 8.6 350 76 unknown 8.7 360 73 unknown .024 7.6 .092
busybox-1.22.0/uniq_false-no-overflow.i no-overflow error (134) 4.4   42 37    error (134) 1.6  34   25   error (134) .71 77 9.3 error (1) .53 43 5.0 timeout 900   6900 11000 out of memory 22    15000 250   unknown .030 4.7 .17 unknown .033 4.7 .26 out of memory 22     15000 260    timeout 910   6900 14000 disqualified 880   710   7200 error(unknown, slicing-finished) 1.3  73 14   unknown 8.7 340 64 unknown 8.6 360 77 unknown 8.7 340 70 unknown .022 7.8 .13 
busybox-1.22.0/usleep_false-no-overflow.i no-overflow error (134) .41  37 4.1  error (134) .18 12   2.2 error (134) .58 39 7.9 error (1) .51 41 4.9 timeout 900   1400 6000 unknown 900    760 11000   unknown .029 4.6 .18 unknown .027 4.6 .26 unknown 3.4   180 50    timeout 900   1400 5200 disqualified 880   480   6400 timeout (verification) 900    140 8500   unknown 8.5 360 69 unknown 8.4 330 64 unknown 8.5 340 65 unknown .023 8.0 .092
busybox-1.22.0/uudecode_false-no-overflow.i no-overflow error (134) 9.1   46 55    error (134) 5.0  77   80   error (134) 2.0  210 25   error (1) .51 42 5.3 error (parsing failed) 3.2 220 26 out of memory 22    15000 270   unknown .034 4.6 .21 unknown .033 4.6 .26 out of memory 22     15000 250    error (parsing failed) 3.3 230 29 disqualified 880   810   6400 error(unknown, slicing-finished) 1.9  100 20   unknown 9.4 360 72 unknown 9.2 370 79 unknown 8.8 370 67 unknown .046 7.4 .075
busybox-1.22.0/wc_false-no-overflow.i no-overflow error (6) .34  42 3.4  error 880    620   7800   error (134) .28 23 4.3 error (1) .54 44 5.0 timeout 910   6300 11000 out of memory 22    15000 260   unknown .030 4.6 .25 unknown .027 4.6 .20 out of memory 22     15000 290    timeout 910   6200 12000 disqualified 880   1100   9400 error(unknown, slicing-finished) .89 58 9.9 unknown 9.1 350 63 unknown 8.6 320 65 unknown 8.3 350 78 unknown .021 7.2 .12 
busybox-1.22.0/who_false-no-overflow.i no-overflow error (134) 1.3   42 12    error (134) .57 22   7.1 error (134) .76 67 9.5 error (1) .52 43 5.5 timeout 910   6900 11000 out of memory 22    15000 300   unknown .059 4.5 .26 unknown .029 4.6 .19 out of memory 22     15000 280    timeout 910   7000 13000 disqualified 880   670   7900 error(unknown, slicing-finished) 1.0  58 12   unknown 8.2 350 72 unknown 8.6 320 66 unknown 9.2 340 76 unknown .020 7.8 .11 
busybox-1.22.0/whoami-incomplete_false-no-overflow.i no-overflow error (134) .30  37 3.2  error (134) .18 11   2.3 error (134) .28 27 3.1 error (1) .54 43 5.1 timeout 900   950 6100 unknown 900    1000 11000   unknown .040 4.6 .15 unknown .025 4.6 .21 unknown 3.0   140 39    timeout 900   1100 6700 disqualified 880   480   9800 timeout (verification) 900    130 7500   unknown 7.2 330 65 unknown 8.6 340 73 unknown 8.4 360 72 unknown .021 7.9 .10 
busybox-1.22.0/yes_false-no-overflow.i no-overflow error (134) .29  37 3.2  error (134) .18 12   2.3 error (134) .57 80 7.2 error (1) .53 42 4.3 timeout 900   1200 6700 witness invalid (false(no-overflow)) 190    860 2000   unknown .031 4.6 .26 unknown .032 4.8 .14 unknown 3.4   160 49    timeout 900   1200 6500 disqualified 880   560   8200 timeout (verification) 900    90 11000   unknown 8.0 330 63 unknown 8.9 360 70 unknown 8.3 360 65 unknown .022 7.3 .12 
busybox-1.22.0/basename_false-unreach-call_true-no-overflow_true-valid-memsafety.i no-overflow error (134) .22  32 2.2  error (42) 880    6000   7300   error (134) 7.5  500 110   error (1) .48 41 4.5 timeout 900   1000 5500 unknown 900    660 10000   unknown .045 4.6 .18 unknown .054 4.6 .14 timeout 900     990 9300    timeout 900   1100 4600 disqualified 880   620   9800 timeout (verification) 900    380 8100   error (7) 180   2600 2000 timeout 900   890 11000 error (7) 180   920 1900 unknown .044 7.6 .097
busybox-1.22.0/chgrp-incomplete_true-no-overflow_false-valid-memtrack.i no-overflow error (134) .31  37 2.7  error (134) .21 12   3.2 error (134) .19 18 2.6 error (1) .51 43 5.0 unknown 100   750 920 unknown 900    800 10000   unknown .035 4.7 .24 unknown .030 4.6 .21 unknown 3.0   140 37    unknown 110   740 1000 disqualified 880   680   7500 timeout (verification) 900    130 8300   unknown 8.2 350 75 unknown 8.2 340 65 unknown 8.2 340 62 unknown .024 7.4 .17 
busybox-1.22.0/chroot-incomplete_true-no-overflow_true-valid-memsafety.i no-overflow error (134) .46  38 4.7  error (134) .28 14   3.3 error (134) .96 68 14   error (1) .52 43 5.3 timeout 900   1400 6200 unknown 900    1600 10000   unknown .026 4.6 .19 unknown .032 4.6 .34 unknown 3.0   150 39    timeout 900   1200 6300 disqualified 880   690   6900 timeout (verification) 900    58 14000   unknown 8.3 360 62 unknown 8.3 320 67 unknown 8.4 330 70 unknown .020 7.2 .088
busybox-1.22.0/cut_false-unreach-call_true-no-overflow_true-valid-memsafety.i no-overflow error (134) 11     50 89    error (134) 5.8  76   68   error (134) .79 76 8.6 error (1) .50 43 6.0 timeout 910   6500 12000 out of memory 22    15000 280   unknown .031 4.6 .22 unknown .033 4.6 .18 out of memory 22     15000 290    timeout 910   6700 13000 disqualified 880   760   7000 error(unknown, slicing-finished) 1.7  80 16   unknown 8.1 350 75 unknown 9.1 350 69 unknown 9.1 360 72 unknown .023 7.7 .16 
busybox-1.22.0/date_false-unreach-call_true-no-overflow_true-valid-memsafety.i no-overflow error (6) .41  47 4.2  error (134) 2.3  120   34   error (134) .72 55 7.9 error (1) .51 42 5.1 timeout 900   3500 10000 out of memory 22    15000 250   unknown .033 4.6 .25 unknown .033 4.6 .17 out of memory 22     15000 230    timeout 900   3500 10000 disqualified 880   3900   12000 error(unknown, slicing-finished) 2.9  150 24   unknown 9.4 360 68 unknown 9.5 350 72 unknown 8.7 370 76 unknown .022 7.8 .088
busybox-1.22.0/dirname_true-no-overflow_true-valid-memsafety.i no-overflow error (134) .23  31 1.9  out of memory 620    13000   8100   error (134) .17 13 2.0 error (1) .50 42 5.4 timeout 900   5300 9900 unknown 900    1800 10000   unknown .045 4.6 .18 unknown .032 4.7 .12 timeout 900     11000 10000    timeout 910   5000 10000 disqualified 880   700   7100 timeout (verification) 900    980 12000   error (7) 140   2700 1400 timeout 900   1000 7500 error (7) 160   1100 1600 unknown .023 7.5 .12 
busybox-1.22.0/du_true-no-overflow_true-valid-memsafety.i no-overflow error (134) 5.8   45 53    error (134) 54    200   490   error (134) .46 38 5.9 error (1) .51 42 4.7 timeout 900   3300 11000 out of memory 22    15000 250   unknown .054 4.6 .12 unknown .028 4.6 .34 out of memory 22     15000 270    timeout 900   3400 10000 disqualified 880   3800   12000 error(unknown, slicing-finished) 3.1  120 21   unknown 9.8 360 81 unknown 9.4 360 79 unknown 8.4 330 68 unknown .023 7.5 .11 
busybox-1.22.0/echo_true-no-overflow_true-valid-memsafety.i no-overflow error (134) .41  38 4.8  error (42) 880    3100   7300   error (134) .65 86 8.6 error (1) .50 42 4.8 timeout 910   860 8200 unknown 900    1600 11000   unknown .029 4.6 .17 unknown .031 4.6 .18 unknown 4.2   240 46    timeout 910   860 8500 disqualified 880   560   7300 timeout (verification) 900    430 6800   unknown 8.4 340 64 unknown 8.7 340 69 unknown 8.4 360 77 unknown .023 7.7 .10 
busybox-1.22.0/expand_false-unreach-call_true-no-overflow_true-valid-memsafety.i no-overflow error (134) 24     71 220    error (134) 29    190   400   error (134) .36 33 5.5 error (1) .51 43 4.9 timeout 910   6600 12000 out of memory 22    15000 270   unknown .031 4.8 .20 unknown .024 4.6 .20 out of memory 22     15000 280    timeout 900   6500 13000 disqualified 880   840   7600 error(unknown, slicing-finished) 3.1  100 23   unknown 9.2 350 82 unknown 9.2 330 71 unknown 8.2 350 62 unknown .021 7.9 .15 
busybox-1.22.0/fold_true-no-overflow_true-valid-memsafety.i no-overflow error (134) 4.8   42 33    error (134) 2.9  44   36   error (134) .36 30 4.2 error (1) .52 43 4.9 timeout 900   830 10000 out of memory 22    15000 260   unknown .055 4.5 .15 unknown .028 4.6 .19 out of memory 22     15000 320    timeout 900   670 10000 disqualified 880   730   6500 error(unknown, slicing-finished) 1.0  60 11   unknown 8.3 330 65 unknown 8.6 340 68 unknown 9.2 360 73 unknown .022 7.6 .13 
busybox-1.22.0/head_true-no-overflow_true-valid-memsafety.i no-overflow error (6) .37  40 3.3  error (134) 2.9  48   33   error (134) .59 50 7.8 error (1) .49 42 5.3 unknown 600   1000 4000 out of memory 23    15000 270   unknown .032 4.6 .31 unknown .029 4.7 .19 out of memory 22     15000 280    unknown 620   1100 4000 disqualified 880   490   7800 error(unknown, slicing-finished) .61 54 7.0 unknown 8.5 360 70 unknown 8.8 370 65 unknown 8.3 360 74 unknown .023 7.1 .096
busybox-1.22.0/hostid_true-no-overflow_true-valid-memsafety.i no-overflow error (134) .22  34 2.0  out of memory 550    13000   6500   error (134) .16 15 1.6 error (1) .51 43 4.8 out of memory 540   15000 6600 unknown 900    1800 10000   unknown .028 4.6 .20 unknown .031 4.6 .13 timeout 900     14000 11000    out of memory 550   15000 7600 disqualified 880   910   7400 timeout (verification) 900    500 10000   true 18   550 150 true 33   750 290 true 19   520 160 unknown .020 7.9 .14 
busybox-1.22.0/logname_true-no-overflow_true-valid-memsafety.i no-overflow error (134) .31  37 2.4  error (134) .19 13   2.2 error (134) .20 18 2.5 error (1) .50 42 4.7 unknown 230   830 1900 false(no-overflow) 220    860 2200   unknown .030 4.6 .19 unknown .052 4.6 .14 unknown 3.0   150 35    unknown 230   840 2300 disqualified 880   720   7600 timeout (verification) 900    52 13000   unknown 7.8 350 66 unknown 8.9 350 69 unknown 8.8 340 70 unknown .022 7.3 .14 
busybox-1.22.0/ls-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i no-overflow error (134) 180     180 2300    error (134) 2.6  45   40   error (134) 1.1  120 13   error (1) .51 43 4.7 timeout 900   3100 11000 out of memory 22    15000 310   unknown .031 4.8 .20 unknown .027 4.6 .28 out of memory 22     15000 240    timeout 910   3100 12000 disqualified 880   3900   11000 error(unknown, slicing-finished) 20    300 94   error (7) 9.4 330 83 error (7) 10   340 80 error (7) 10   360 91 unknown .022 7.4 .099
busybox-1.22.0/mkdir_true-no-overflow_true-valid-memsafety.i no-overflow error (134) 2.0   43 19    error 880    1600   4800   error (134) .53 33 6.3 error (1) .50 42 4.5 timeout 910   6700 12000 out of memory 23    15000 260   unknown .032 4.5 .18 unknown .037 4.6 .23 out of memory 22     15000 300    timeout 900   6600 11000 disqualified 880   660   7300 error(unknown, slicing-finished) 1.1  81 16   unknown 8.5 340 68 unknown 8.8 360 82 unknown 8.8 360 65 unknown .023 7.6 .15 
busybox-1.22.0/mkfifo-incomplete_true-no-overflow_true-valid-memsafety.i no-overflow error (134) .26  36 2.6  error (134) .21 12   2.4 error (134) .17 17 2.2 error (1) .52 42 5.0 unknown 170   800 1600 unknown 900    2000 9400   unknown .031 4.6 .21 unknown .029 4.6 .19 unknown 3.0   140 38    unknown 170   810 1700 disqualified 880   670   7100 timeout (verification) 900    54 11000   unknown 8.5 360 62 unknown 7.7 330 61 unknown 8.4 340 67 unknown .027 7.6 .078
busybox-1.22.0/od_false-unreach-call_true-no-overflow_true-valid-memsafety.i no-overflow error (134) 540     340 6200    error 880    670   4300   error (134) .78 61 9.4 error (1) .51 43 5.2 timeout 910   6800 12000 out of memory 23    15000 300   unknown .030 4.6 .15 unknown .028 4.6 .30 out of memory 22     15000 260    timeout 910   6700 12000 disqualified 880   1000   8200 error(unknown, slicing-finished) 13    340 65   unknown 8.9 340 74 unknown 9.6 370 80 unknown 9.6 350 79 unknown .025 7.6 .11 
busybox-1.22.0/printf_false-unreach-call_true-no-overflow_true-valid-memsafety.i no-overflow error (6) .50  43 4.1  error (134) 18    98   220   error (134) .25 24 3.1 error (1) .55 42 5.7 out of memory 210   15000 2000 unknown 900    3500 7800   unknown .033 4.6 .19 unknown .027 4.6 .21 unknown 3.0   150 45    out of memory 210   15000 1900 disqualified 880   460   9800 error(returned 1, before-instr) .27 18 3.4 unknown 9.5 360 84 unknown 8.5 360 72 unknown 9.0 360 74 unknown .027 7.4 .15 
busybox-1.22.0/readlink_true-no-overflow_true-valid-memsafety.i no-overflow error (134) 2.1   41 25    error (134) .64 24   8.1 error (134) .87 69 10   error (1) .51 43 4.6 timeout 900   6900 12000 out of memory 22    15000 330   unknown .032 4.6 .18 unknown .052 4.6 .20 out of memory 22     15000 290    timeout 910   7100 11000 disqualified 880   670   7300 error(unknown, slicing-finished) .95 54 13   unknown 9.0 360 73 unknown 9.0 350 75 unknown 8.5 360 68 unknown .031 7.5 .12 
busybox-1.22.0/realpath_true-no-overflow_true-valid-memsafety.i no-overflow error (134) .31  37 3.8  error (134) .23 12   3.6 error (134) .95 61 14   error (1) .53 43 4.9 timeout 900   1400 7100 unknown 900    2100 7600   unknown .028 4.6 .17 unknown .029 4.7 .25 unknown 3.0   140 44    timeout 900   1400 8000 disqualified 880   670   6500 timeout (verification) 900    71 12000   unknown 8.6 360 71 unknown 8.2 360 63 unknown 7.8 340 68 unknown .021 7.8 .17 
busybox-1.22.0/rm_true-no-overflow_true-valid-memsafety.i no-overflow error (134) 5.0   45 41    error 880    300   11000   error (134) .71 71 9.8 error (1) .53 44 5.4 timeout 910   6400 11000 out of memory 23    15000 260   unknown .034 4.6 .23 unknown .030 4.8 .22 out of memory 22     15000 330    timeout 910   6400 11000 disqualified 880   750   8800 error(unknown, slicing-finished) 1.8  110 16   unknown 8.2 350 69 unknown 8.9 360 72 unknown 8.2 330 67 unknown .021 7.6 .11 
busybox-1.22.0/seq_true-no-overflow_true-valid-memsafety.i no-overflow error (134) 1.1   40 14    error (134) .50 16   6.2 error (134) .48 30 6.7 error (1) .54 43 5.0 timeout 910   6700 11000 out of memory 22    15000 290   unknown .046 4.6 .16 unknown .031 4.7 .29 out of memory 22     15000 270    timeout 900   7000 12000 disqualified 880   670   6500 error(returned 1, before-instr) .26 17 3.8 unknown 7.9 340 66 unknown 8.3 340 65 unknown 8.3 360 66 unknown .033 7.7 .15 
busybox-1.22.0/sleep_true-no-overflow_true-valid-memsafety.i no-overflow error (134) .72  39 9.0  error (134) .69 24   8.6 error (134) .72 85 9.8 error (1) .51 42 5.1 unknown 7.9 320 66 unknown 890    680 10000   unknown .037 4.6 .12 unknown .030 4.7 .24 unknown 3.5   170 55    unknown 7.8 330 76 disqualified 880   730   7300 error(returned 1, before-instr) .27 17 2.7 unknown 8.9 360 74 unknown 8.7 350 73 unknown 8.9 360 74 unknown .027 7.7 .12 
busybox-1.22.0/stty_false-unreach-call_true-no-overflow_true-valid-memsafety.i no-overflow error (134) 48     110 450    error (134) 56    160   550   error (134) 3.4  180 47   error (1) .49 42 4.7 timeout 900   2200 10000 out of memory 23    15000 250   unknown .030 4.7 .18 unknown .028 4.7 .18 out of memory 22     15000 280    timeout 900   2200 11000 disqualified 880   1400   6700 timeout (verification) 900    170 13000   unknown 9.9 370 77 unknown 10   360 82 unknown 10   370 79 unknown .022 7.6 .12 
busybox-1.22.0/sync_true-no-overflow_true-valid-memsafety.i no-overflow error (134) .27  35 2.7  error (134) .17 10   1.8 error (134) .24 16 2.7 error (1) .54 43 4.7 unknown 40   620 460 unknown 900    870 11000   unknown .027 4.7 .19 unknown .046 4.6 .18 unknown 3.0   140 50    unknown 40   640 430 disqualified 880   680   6800 timeout (verification) 900    130 8200   unknown 8.2 360 65 unknown 7.9 340 61 unknown 8.3 340 69 unknown .025 7.2 .13 
busybox-1.22.0/tac_true-no-overflow_true-valid-memsafety.i no-overflow error (134) 4.5   41 38    error (134) 2.1  39   28   error (134) .68 55 8.0 error (1) .58 42 4.4 timeout 900   6800 12000 out of memory 23    15000 300   unknown .035 4.6 .29 unknown .032 4.8 .11 out of memory 22     15000 260    timeout 900   7000 11000 disqualified 880   680   7600 error(unknown, slicing-finished) .78 45 9.2 unknown 8.8 330 71 unknown 9.5 340 72 unknown 8.4 340 72 unknown .022 7.3 .092
busybox-1.22.0/tee_true-no-overflow_true-valid-memsafety.i no-overflow error (6) .33  41 3.7  error (134) .87 28   12   error (134) 1.3  110 19   error (1) .52 42 5.6 timeout 900   3600 11000 out of memory 22    15000 280   unknown .031 4.6 .19 unknown .028 4.6 .14 out of memory 22     15000 250    timeout 900   3500 11000 disqualified 880   3700   13000 error(unknown, slicing-finished) .78 48 6.9 unknown 8.9 360 69 unknown 9.2 360 74 unknown 9.6 370 76 unknown .032 7.1 .10 
busybox-1.22.0/test-incomplete_false-unreach-call_true-no-overflow_true-valid-memsafety.i no-overflow error (134) 23     68 250    error 880    670   5500   error (134) 2.7  170 40   error (1) .53 42 4.8 exception 30   570 310 unknown 900    15000 8000   unknown .031 4.6 .13 unknown .029 4.6 .21 unknown 3.3   170 50    exception 30   560 330 disqualified 880   420   6600 error(unknown, slicing-finished) .82 61 10   unknown 9.4 360 64 unknown 9.2 350 68 unknown 8.8 360 74 unknown .027 7.2 .082
busybox-1.22.0/touch_false-unreach-call_true-no-overflow_true-valid-memsafety.i no-overflow error (134) 4.1   47 46    error (134) 2.2  110   32   error (134) .59 35 8.8 error (1) .52 42 5.4 timeout 910   7500 11000 out of memory 23    15000 300   unknown .031 4.6 .23 unknown .034 4.6 .21 out of memory 22     15000 300    timeout 910   6900 9000 disqualified 880   720   7100 error(unknown, slicing-finished) 1.6  120 16   unknown 8.8 360 75 unknown 9.1 340 75 unknown 9.5 360 78 unknown .025 7.4 .13 
busybox-1.22.0/uname_true-no-overflow_true-valid-memsafety.i no-overflow error (134) 1.1   41 11    error (134) .85 120   11   error (134) .50 32 6.5 error (1) .50 43 4.5 timeout 900   6600 11000 out of memory 22    15000 270   unknown .029 4.6 .20 unknown .045 4.7 .16 out of memory 22     15000 270    timeout 900   6600 9900 disqualified 880   640   8100 error(unknown, slicing-finished) .77 54 8.6 unknown 7.8 340 69 unknown 8.5 360 68 unknown 8.5 360 66 unknown .021 7.5 .12 
busybox-1.22.0/uniq_true-no-overflow_true-valid-memsafety.i no-overflow error (134) 4.2   42 38    error (134) 1.6  34   23   error (134) .70 77 11   error (1) .52 43 5.4 timeout 900   6800 11000 out of memory 23    15000 330   unknown .031 4.8 .20 unknown .060 4.6 .21 out of memory 22     15000 280    timeout 900   6900 11000 disqualified 880   730   6400 error(unknown, slicing-finished) 1.2  72 13   unknown 9.1 360 79 unknown 8.6 360 70 unknown 8.4 350 69 unknown .023 7.3 .11 
busybox-1.22.0/usleep_true-no-overflow_true-valid-memsafety.i no-overflow error (134) .38  37 4.8  error (134) .18 12   2.3 error (134) .57 39 6.8 error (1) .51 43 5.4 unknown 140   800 1700 unknown 900    810 11000   unknown .038 4.6 .14 unknown .029 4.6 .26 unknown 3.4   180 44    unknown 140   790 1200 disqualified 880   510   8900 timeout (verification) 900    150 9300   unknown 8.6 350 69 unknown 8.0 320 59 unknown 7.9 340 60 unknown .018 7.5 .11 
busybox-1.22.0/uudecode_true-no-overflow_true-valid-memsafety.i no-overflow error (134) 8.7   46 100    error (134) 4.9  76   55   error (134) 2.0  210 23   error (1) .55 42 5.2 timeout 910   6500 12000 out of memory 22    15000 260   unknown .028 4.6 .22 unknown .042 4.7 .16 out of memory 22     15000 250    timeout 910   6600 13000 disqualified 880   780   7100 error(unknown, slicing-finished) 2.0  99 22   unknown 9.0 370 72 unknown 8.5 340 70 unknown 8.9 350 77 unknown .022 7.5 .18 
busybox-1.22.0/wc_false-unreach-call_true-no-overflow_true-valid-memsafety.i no-overflow error (6) .38  42 3.4  error 880    610   7200   error (134) .29 23 3.7 error (1) .51 42 5.6 timeout 910   6200 11000 out of memory 22    15000 240   unknown .030 4.6 .15 unknown .045 4.6 .17 out of memory 22     15000 260    timeout 910   6300 13000 disqualified 880   1100   5100 error(unknown, slicing-finished) .90 58 12   unknown 8.9 350 73 unknown 8.5 350 72 unknown 8.6 350 74 unknown .022 7.7 .091
busybox-1.22.0/who_true-no-overflow_true-valid-memsafety.i no-overflow error (134) 1.3   42 13    error (134) .56 22   7.3 error (134) .77 67 13   error (1) .53 44 5.1 timeout 910   7000 11000 out of memory 22    15000 260   unknown .035 4.8 .22 unknown .031 4.7 .17 out of memory 22     15000 310    timeout 910   7500 12000 disqualified 880   660   8400 error(unknown, slicing-finished) 1.0  58 11   unknown 8.7 350 76 unknown 9.0 350 79 unknown 8.7 360 77 unknown .021 7.2 .12 
busybox-1.22.0/whoami-incomplete_true-no-overflow_true-valid-memsafety.i no-overflow error (134) .29  37 3.0  error (134) .18 12   2.1 error (134) .27 27 4.3 error (1) .56 44 5.1 out of memory 300   15000 2300 unknown 900    920 12000   unknown .031 4.6 .14 unknown .029 4.6 .16 unknown 3.0   140 39    out of memory 310   15000 2700 disqualified 880   460   7900 timeout (verification) 900    130 7500   unknown 8.7 350 67 unknown 8.5 360 73 unknown 8.6 340 69 unknown .027 7.2 .10 
busybox-1.22.0/yes_true-no-overflow_true-valid-memsafety.i no-overflow error (134) .30  37 3.4  error (134) .18 12   2.0 error (134) .61 80 6.7 error (1) .50 42 4.5 timeout 900   1100 5700 false(no-overflow) 170    850 1800   unknown .033 4.6 .16 unknown .062 4.7 .22 unknown 3.4   160 44    timeout 900   970 7000 disqualified 880   560   6600 timeout (verification) 900    93 11000   unknown 8.1 330 60 unknown 8.3 360 71 unknown 8.5 330 71 unknown .021 7.6 .14 
ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_false-unreach-call.cil.out.i unreach-call error (6) 3.0   290 25    false(unreach-call) 3.1  220   26   out of memory 260    15000 2100   false(unreach-call) 53    1700 470   false(unreach-call) 21   910 180 unknown 16    40 210   error - divine failed with signal 6 (program::insert: unresolved symbol (global variable): cpu_possible_mask) 2.5   240   31    error - divine failed with signal 6 (.../lart/abstract/vpa.cpp: 82: encountered unknown parent instruction:) 2.3   230   29    false(unreach-call) 15     4700 170    false(unreach-call) 380   1700 2800 disqualified 860   940   12000 error(unknown, verification-finished) 4.1  62 62   error (7) 61   1000 520 error (7) 65   1000 550 error (7) 570   4700 7400 false(unreach-call) 53     870   580    
ldv-linux-3.0/module_get_put-drivers-block-loop.ko_false-unreach-call.cil.out.i unreach-call error (6) 2.6   260 28    error 880    1900   5300   false(valid-deref) .50 42 6.7 false(unreach-call) 26    720 220   timeout 960   9300 7600 unknown 48    140 570   error - divine failed with exitcode 1 1.6   210   22    error - divine failed with signal 6 (.../lart/abstract/util.cpp: 190: encountered unknown parent instruction:) 1.7   210   21    unknown .43  130 5.0  unknown 68   2300 690 disqualified 71   520   690 error(unknown, verification-finished) .96 50 14   timeout 900   4100 8400 error (7) 450   2500 5900 timeout 900   3700 8200 timeout 900     1900   7700    
ldv-linux-3.0/module_get_put-drivers-block-pktcdvd.ko_false-unreach-call.cil.out.i unreach-call error (6) 2.6   330 21    false(valid-deref) 600    4000   5400   false(valid-free) .73 60 9.3 error 32    1100 270   timeout 960   7500 8300 unknown 140    300 1800   error - divine failed with exitcode 1 1.7   210   19    error - divine failed with signal 6 (.../lart/abstract/util.cpp: 190: encountered unknown parent instruction:) 1.7   210   22    unknown .87  210 13    unknown 81   1600 600 disqualified 16   300   210 error(unknown, verification-finished) 2.4  140 17   timeout 900   5100 7400 error (7) 240   2900 2500 timeout 900   5200 9200 timeout 900     1200   8100    
ldv-linux-3.0/module_get_put-drivers-isdn-gigaset-gigaset.ko_false-unreach-call.cil.out.i unreach-call error (6) 1.3   110 10    false(unreach-call) 120    2100   820   error (134) 2.9  130 29   timeout 900    8500 9000   timeout 960   6100 10000 unknown 900    3100 8000   error - divine failed with exitcode 1 1.8   210   26    error - divine failed with signal 6 (.../lart/abstract/util.cpp: 190: encountered unknown parent instruction:) 1.8   210   27    false(unreach-call) 24     2000 260    unknown 250   2500 2100 disqualified 890   730   8000 timeout (verification) 900    2900 9400   timeout 900   2400 11000 timeout 900   2400 12000 timeout 900   6600 10000 unknown 86     1100   920    
ldv-linux-3.0/module_get_put-drivers-isdn-mISDN-mISDN_core.ko_false-unreach-call.cil.out.i unreach-call out of memory 98     15000 1000    error 880    3900   6900   error (134) 5.6  470 63   false(unreach-call) 100    3600 910   false(unreach-call) 19   680 170 unknown 7.4  30 100   error - divine failed with exitcode 1 1.8   210   28    error - divine failed with signal 6 (.../lart/abstract/util.cpp: 190: encountered unknown parent instruction:) 1.8   210   24    false(unreach-call) 40     3000 440    false(unreach-call) 490   2800 5000 disqualified 49   300   560 error(unknown, verification-finished) 1.3  31 16   unknown 11   390 87 unknown 11   380 76 unknown 12   380 90 false(unreach-call) 140     1200   1600    
ldv-linux-3.0/module_get_put-drivers-net-ppp_generic.ko_false-unreach-call.cil.out.i unreach-call error (6) 3.0   120 25    error 880    2100   6700   out of memory 340    15000 2900   timeout 900    8200 11000   false(unreach-call) 89   2600 800 false(unreach-call) 380    8000 3600   error - divine failed with exitcode 1 1.7   210   20    error - divine failed with signal 6 (.../lart/abstract/util.cpp: 190: encountered unknown parent instruction:) 1.7   210   23    out of memory 160     15000 1900    false(unreach-call) 250   2700 2600 disqualified 13   280   170 timeout (verification) 900    2800 8200   timeout 900   5600 11000 error (7) 270   2500 2800 timeout 900   5500 7400 false(unreach-call) 730     890   7300    
ldv-linux-3.0/module_get_put-drivers-net-wan-farsync.ko_false-unreach-call.cil.out.i unreach-call error (6) .72  61 5.0  error (42) 880    2100   4200   error (134) 9.0  810 100   timeout 900    4500 11000   timeout 960   9200 7400 unknown 2.7  170 29   error - divine failed with exitcode 1 1.7   210   22    error - divine failed with signal 6 (.../lart/abstract/util.cpp: 190: encountered unknown parent instruction:) 1.6   210   25    true 47     1000 590    timeout 910   6400 8900 disqualified 14   300   180 error(unknown, verification-finished) 1.3  75 14   timeout 900   4000 9500 timeout 900   3400 9900 timeout 900   3300 10000 false(unreach-call) 270     3000   2600    
ldv-linux-3.0/module_get_put-drivers-tty-synclink_gt.ko_false-unreach-call.cil.out.i unreach-call error (6) 22     1400 140    error 880    2900   4600   false(unreach-call) 6.6  400 78   timeout 900    11000 5300   false(unreach-call) 170   4100 1800 unknown 900    6800 7500   error - divine failed with exitcode 1 1.8   210   23    error - divine failed with signal 6 (.../lart/abstract/util.cpp: 190: encountered unknown parent instruction:) 1.7   210   26    timeout 900     6500 9300    false(unreach-call) 170   2200 2300 disqualified 70   2000   940 error(unknown, verification-finished) 10    250 83   timeout 900   8700 5600 timeout 900   4400 9300 timeout 900   8400 5500 timeout 900     990   10000    
ldv-linux-3.0/module_get_put-drivers-usb-core-usbcore.ko_false-unreach-call.cil.out.i unreach-call out of memory 130     15000 970    error 880    1900   11000   error (134) 350    2400 5300   false(unreach-call) 39    1100 340   false(unreach-call) 140   4200 1400 false(unreach-call) 18    1300 220   error - divine failed with exitcode 1 2.0   220   29    error - divine failed with signal 6 (.../lart/abstract/util.cpp: 190: encountered unknown parent instruction:) 2.0   220   24    false(unreach-call) 6.2   1300 97    false(unreach-call) 370   2500 3300 disqualified 900   2800   10000 error(unknown, verification-finished) 3.1  49 43   timeout 900   7000 10000 timeout 900   5800 9300 timeout 900   6700 11000 unknown 58     640   480    
ldv-linux-3.0/usb_urb-drivers-media-dvb-ttusb-dec-ttusb_dec.ko_false-unreach-call.cil.out.i unreach-call error (134) 1.3   68 12    error 880    2000   4500   out of memory 330    15000 3400   timeout 900    7600 11000   false(unreach-call) 29   990 250 false(unreach-call) 1.0  330 11   unknown 8.7   440   120    error - divine failed with signal 6 (.../lart/abstract/util.cpp: 190: encountered unknown parent instruction:) 1.7   210   21    false(unreach-call) 1.0   320 11    false(unreach-call) 81   1600 970 disqualified 13   220   160 error(unknown, verification-finished) .84 56 10   timeout 900   3500 9600 error (7) 260   2300 3000 timeout 900   4800 11000 false(unreach-call) 73     750   780    
ldv-linux-3.0/usb_urb-drivers-net-can-usb-ems_usb.ko_false-unreach-call.cil.out.i unreach-call error (134) .47  52 5.1  error (6) 22    97   320   error (6) 12    140 200   timeout 900    11000 7200   false(unreach-call) 23   810 180 false(unreach-call) 5.5  180 67   unknown 8.5   430   120    error - divine failed with signal 11 1.6   200   21    false(unreach-call) 4.9   250 59    false(unreach-call) 49   1600 560 disqualified 7.4 150   94 error(unknown, verification-finished) .60 29 7.1 unknown 510   4800 4700 error (7) 240   2900 2600 unknown 500   5100 4500 false(unreach-call) 710     2200   8300    
ldv-linux-3.0/usb_urb-drivers-net-usb-catc.ko_false-unreach-call.cil.out.i unreach-call error (134) .53  54 4.0  error (134) 110    3000   1600   error (134) 5.4  180 81   timeout 900    7500 9900   false(unreach-call) 620   6200 6500 false(unreach-call) .93 140 12   unknown 8.8   430   110    error - divine failed with signal 6 (.../lart/abstract/util.cpp: 190: encountered unknown parent instruction:) 1.6   200   20    false(unreach-call) 1.1   140 13    false(unreach-call) 55   1600 550 disqualified 18   190   250 error(unknown, verification-finished) .63 34 8.8 error (7) 94   1500 820 timeout 900   1800 9700 error (7) 420   3100 5900 false(unreach-call) 170     1200   2100    
ldv-linux-3.0/usb_urb-drivers-staging-lirc-lirc_imon.ko_false-unreach-call.cil.out.i unreach-call error (134) .40  47 3.3  false(valid-deref) 1.2  83   14   out of memory 380    15000 4000   timeout 910    11000 7800   false(unreach-call) 150   2800 1500 unknown 900    780 11000   unknown 8.5   430   110    error - divine failed with signal 11 1.6   200   20    false(unreach-call) 1.4   130 21    false(unreach-call) 75   1900 700 disqualified 10   190   120 error(unknown, verification-finished) 3.7  32 49   timeout 900   2200 11000 error (7) 150   2400 1600 timeout 900   4300 11000 false(unreach-call) 690     4500   7300    
ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko_false-unreach-call.cil.out.i unreach-call error (134) .42  47 3.7  false(valid-deref) 2.6  210   33   false(valid-free) 1.0  75 13   timeout 910    11000 7400   timeout 930   5900 9100 false(unreach-call) .64 120 7.3 error - divine failed with exitcode 1 1.6   200   21    error - divine failed with signal 6 (.../lart/abstract/util.cpp: 190: encountered unknown parent instruction:) 1.6   200   20    false(unreach-call) .63  120 8.9  false(unreach-call) 83   1700 860 disqualified 18   220   240 timeout (verification) 900    2200 13000   error (7) 150   2000 1400 error (7) 210   2400 2500 error (7) 430   3500 5700 false(unreach-call) 300     1000   3500    
ldv-linux-3.0/module_get_put-drivers-atm-eni.ko_true-unreach-call.cil.out.i unreach-call error (6) 36     420 260    error 880    4100   6900   out of memory 210    15000 2200   true 18    510 140   true 100   1600 1300 unknown 900    12000 7900   error - divine failed with exitcode 1 1.7   210   24    error - divine failed with signal 6 (.../lart/abstract/util.cpp: 190: encountered unknown parent instruction:) 1.7   210   22    out of memory 880     15000 5900    true 77   1200 620 disqualified 42   690   500 error(unknown, verification-finished) 1.6  100 16   true 36   1200 280 true 240   2900 2500 true 36   1000 290 true 43     1000   340    
ldv-linux-3.0/module_get_put-drivers-block-drbd-drbd.ko_true-unreach-call.cil.out.i unreach-call error (6) 3.2   290 18    false(valid-deref) 9.7  470   110   out of memory 250    15000 2900   true 27    880 240   true 110   3600 1300 unknown 16    40 230   error - divine failed with signal 6 (program::insert: unresolved symbol (global variable): cpu_possible_mask) 2.5   240   36    error - divine failed with signal 6 (.../lart/abstract/vpa.cpp: 82: encountered unknown parent instruction:) 2.3   230   27    out of memory 62     15000 700    true 460   3400 3500 disqualified 150   400   1400 error(unknown, verification-finished) 4.2  63 60   error (7) 64   1000 540 error (7) 63   1000 520 true 520   4200 6500 true 180     3000   1900    
ldv-linux-3.0/module_get_put-drivers-block-paride-pt.ko_true-unreach-call.cil.out.i unreach-call error (6) 1.6   130 19    error (42) 880    5300   5000   out of memory 180    15000 2400   true 12    470 95   true 120   3800 1200 unknown 900    3100 8300   error - divine failed with exitcode 1 1.7   200   21    error - divine failed with signal 11 1.6   200   23    timeout 900     2200 6300    true 47   2400 470 disqualified 6.3 170   81 timeout (verification) 900    2900 7100   true 28   840 230 true 120   1800 1300 true 31   760 260 true 58     2000   510    
ldv-linux-3.0/module_get_put-drivers-bluetooth-btmrvl_false-termination.ko_true-unreach-call.cil.out.i unreach-call error (6) 26     5400 240    error 880    3300   7300   out of memory 320    15000 2400   true 12    460 100   true 98   1500 1000 unknown 900    10000 6600   error - divine failed with exitcode 1 1.6   210   22    error - divine failed with signal 6 (.../lart/abstract/util.cpp: 190: encountered unknown parent instruction:) 1.6   210   24    timeout 900     10000 7500    true 36   1200 330 disqualified 5.6 180   82 true .59 25 7.6 true 30   1100 230 timeout 900   2600 7000 true 30   1100 240 true 29     670   240    
ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i unreach-call error (6) .61  59 5.4  error (42) 880    1700   5700   error (134) 100    2700 840   true 19    640 150   true 150   2300 1900 unknown 900    9500 12000   error - divine failed with exitcode 1 1.6   200   19    error - divine failed with signal 6 (.../lart/abstract/util.cpp: 190: encountered unknown parent instruction:) 1.6   200   20    timeout 900     1800 11000    timeout 900   9700 9100 disqualified 7.4 220   110 timeout (verification) 900    3200 13000   true 67   2500 780 timeout 900   3500 8600 true 33   930 280 true 150     6000   1500    
ldv-linux-3.0/module_get_put-drivers-gpu-drm-i915-i915.ko_true-unreach-call.cil.out.i unreach-call error (6) 4.9   460 32    false(valid-free) 5.9  360   50   false(valid-free) 8.9  540 80   true 37    1500 320   true 120   2300 1200 unknown 24    49 320   error - divine failed with exitcode 1 2.5   250   32    error - divine failed with signal 11 2.6   250   35    unknown 19     6100 220    timeout (exception) 910   1700 4400 disqualified 900   12000   8500 error(unknown, verification-finished) 6.1  88 68   timeout 900   5300 13000 timeout 900   5400 12000 timeout 900   5300 13000 true 760     6200   9200    
ldv-linux-3.0/module_get_put-drivers-hid-hid-magicmouse.ko_true-unreach-call.cil.out.i unreach-call error (6) .33  39 3.0  false(valid-free) 2.3  180   27   out of memory 180    15000 2500   true 8.3  330 73   true 8.7 450 69 unknown 900    2100 6500   unknown 8.3   430   95    error - divine failed with signal 11 1.6   200   22    timeout 900     1800 8100    true 97   2500 910 disqualified 4.1 100   57 true .40 21 5.9 true 16   540 130 true 25   720 200 true 17   540 120 true 22     620   180    
ldv-linux-3.0/module_get_put-drivers-hwmon-it87.ko_true-unreach-call.cil.out.i unreach-call error (6) .63  64 4.3  false(valid-free) .99 51   12   out of memory 180    15000 1300   true 15    510 130   true 99   1300 1300 unknown 900    2500 6100   unknown 8.9   440   120    error - divine failed with signal 11 1.7   210   24    true 3.5   230 43    true 75   1500 980 disqualified 6.9 170   81 true .69 38 8.2 true 39   2200 350 true 220   4400 2300 true 40   2000 370 true 60     2900   530    
ldv-linux-3.0/module_get_put-drivers-net-pppox_false-termination.ko_true-unreach-call.cil.out.i unreach-call error (6) .27  42 2.4  error (42) 880    1100   9900   out of memory 240    15000 2300   true 11    460 83   timeout 960   6600 7000 unknown 1.2  67 14   unknown 8.4   430   120    error - divine failed with signal 6 (.../lart/abstract/util.cpp: 190: encountered unknown parent instruction:) 1.6   200   20    true .33  39 3.7  true 18   1200 150 disqualified 880   370   9400 timeout (verification) 900    74 9700   true 21   590 180 true 17   630 140 true 21   660 170 unknown 17     260   150    
ldv-linux-3.0/module_get_put-drivers-net-sis900.ko_true-unreach-call.cil.out.i unreach-call error (6) 2.0   210 15    out of memory 330    13000   4100   false(unreach-call) 66    890 880   true 15    500 130   true 100   1700 1200 unknown 900    5000 8100   unknown 9.0   440   110    error - divine failed with signal 6 (.../lart/abstract/util.cpp: 190: encountered unknown parent instruction:) 1.7   210   23    timeout 900     3800 6300    true 120   1500 1800 disqualified 15   350   190 error(unknown, verification-finished) 1.6  110 16   true 34   920 290 true 130   4200 1600 true 34   920 290 true 40     970   350    
ldv-linux-3.0/module_get_put-drivers-scsi-megaraid.ko_true-unreach-call.cil.out.i unreach-call error (6) 53     880 280    error 880    4100   4900   false(unreach-call) 3.6  250 38   true 25    820 200   true 100   2500 1200 unknown 900    7800 7300   error - divine failed with exitcode 1 1.7   210   21    error - divine failed with signal 6 (.../lart/abstract/util.cpp: 190: encountered unknown parent instruction:) 1.8   210   23    timeout 900     2300 6600    true 95   1300 730 disqualified 43   420   520 error(unknown, verification-finished) 2.3  180 22   true 43   1300 380 true 160   4000 1500 true 45   1600 430 true 51     1100   410    
ldv-linux-3.0/module_get_put-drivers-video-aty-aty128fb.ko_true-unreach-call.cil.out.i unreach-call error (6) 1.6   110 13    error 880    3800   3900   out of memory 250    15000 2200   true 13    360 110   true 100   2400 1300 unknown 900    8400 9300   unknown 8.6   440   120    error - divine failed with signal 11 1.7   200   21    true 89     1400 940    true 52   1500 600 disqualified 8.5 170   120 true .83 56 9.0 true 120   3600 1400 error (7) 550   4700 6700 true 120   2700 1600 true 40     960   320    
ldv-linux-3.0/usb_urb-drivers-input-tablet-kbtab.ko_true-unreach-call.cil.out.i unreach-call error (134) .29  40 3.1  false(valid-deref) .64 60   8.6 error (134) 12    920 140   true 12    480 110   true 180   4500 1600 false(unreach-call) .37 62 4.5 unknown 8.4   430   120    error - divine failed with signal 11 1.6   200   20    false(unreach-call) .35  57 4.0  true 180   3100 1500 disqualified 880   610   8600 timeout (verification) 900    66 9600   true 53   1100 410 true 95   1300 1000 true 180   3500 1900 unknown 30     440   320    
ldv-linux-3.0/usb_urb-drivers-media-video-c-qcam.ko_true-unreach-call.cil.out.i unreach-call error (6) 2.8   110 18    error 880    2400   4700   out of memory 150    15000 1300   true 12    470 95   true 100   1600 1300 out of memory 560    15000 6200   unknown 8.5   430   120    error - divine failed with signal 6 (.../lart/abstract/util.cpp: 190: encountered unknown parent instruction:) 1.6   200   20    timeout 900     9400 7000    true 79   1500 1000 disqualified 6.1 170   77 true .72 46 8.4 unknown 10   380 81 unknown 9.3 380 83 unknown 10   380 77 unknown 75     1100   820    
ldv-linux-3.0/usb_urb-drivers-media-video-msp3400.ko_true-unreach-call.cil.out.i unreach-call error (134) 1.3   86 12    false(valid-free) 140    2900   900   out of memory 280    15000 2200   true 18    520 140   true 100   1400 1400 unknown 900    3400 6000   unknown 9.0   440   120    error - divine failed with signal 6 (.../lart/abstract/util.cpp: 190: encountered unknown parent instruction:) 1.6   210   21    true 640     3700 4400    true 130   1600 1500 disqualified 8.2 170   110 true 1.5  74 18   true 42   1500 410 true 130   2500 1400 true 41   1500 370 true 42     950   340    
ldv-linux-3.0/usb_urb-drivers-misc-c2port-core.ko_true-unreach-call.cil.out.i unreach-call error (134) .60  45 5.6  error (42) 880    1200   4400   out of memory 140    15000 1600   true 8.9  390 82   true 100   4400 780 timeout 900    8400 11000   unknown 8.6   430   110    error - divine failed with signal 6 (.../lart/abstract/util.cpp: 190: encountered unknown parent instruction:) 1.6   200   22    true 12     240 160    true 38   1400 410 disqualified 4.5 110   55 error(unknown, verification-finished) .51 23 7.2 true 20   590 160 true 230   4700 2700 true 20   580 170 true 31     760   280    
ldv-linux-3.0/usb_urb-drivers-mtd-sm_ftl.ko_true-unreach-call.cil.out.i unreach-call error (134) .99  51 10    error 880    1200   5000   false(valid-free) 1.1  100 14   true 13    490 110   true 23   700 210 out of memory 440    15000 5800   unknown 8.5   430   110    error - divine failed with signal 6 (.../lart/abstract/util.cpp: 190: encountered unknown parent instruction:) 1.6   200   21    timeout 900     14000 12000    timeout 910   7100 11000 disqualified 6.8 180   88 timeout (verification) 900    260 12000   true 25   760 210 true 78   1900 680 true 25   770 220 true 33     860   260    
ldv-linux-3.0/usb_urb-drivers-scsi-dc395x.ko_true-unreach-call.cil.out.i unreach-call error (134) 7.2   96 56    error 880    2500   4300   false(valid-deref) 8.9  660 79   true 19    650 170   true 100   2200 1300 unknown 900    13000 6300   unknown 9.2   440   110    error - divine failed with signal 6 (.../lart/abstract/util.cpp: 190: encountered unknown parent instruction:) 1.7   210   20    out of memory 360     15000 2900    true 170   1900 1700 disqualified 39   440   550 error(unknown, verification-finished) 4.4  160 48   error (7) 14   340 120 error (7) 15   340 110 error (7) 15   330 120 true 23     450   200    
ldv-linux-3.0/usb_urb-drivers-usb-serial-ir-usb.ko_true-unreach-call.cil.out.i unreach-call error (134) .35  43 3.7  false(valid-free) .69 60   9.6 error (134) 11    810 130   true 52    2600 500   timeout 940   5900 10000 unknown 900    600 14000   unknown 8.7   550   96    error - divine failed with signal 11 1.6   200   24    timeout 900     5800 11000    true 27   1200 230 disqualified 880   750   6800 error(unknown, verification-finished) 24    44 290   true 56   1200 450 true 130   1700 1500 true 56   1100 500 unknown 27     450   250    
ldv-linux-3.0/usb_urb-drivers-usb-serial-whiteheat.ko_true-unreach-call.cil.out.i unreach-call error (6) .98  59 8.9  false(valid-free) 16    710   180   error (134) 110    8400 1300   true 22    680 180   true 100   2800 1000 unknown 900    13000 8400   unknown 8.7   430   120    error - divine failed with signal 6 (.../lart/abstract/util.cpp: 190: encountered unknown parent instruction:) 1.6   200   19    out of memory 480     15000 4400    true 49   1400 550 disqualified 890   1400   9400 timeout (verification) 900    2800 8800   true 100   2000 850 true 160   2900 1500 timeout 900   4900 11000 true 82     2800   760    
ldv-linux-3.0/usb_urb-drivers-uwb-i1480-dfu-i1480-dfu-usb.ko_true-unreach-call.cil.out.i unreach-call error (134) .56  47 4.7  error 880    970   7000   out of memory 230    15000 2100   true 18    580 160   timeout 960   7600 11000 false(unreach-call) 1.2  110 14   unknown 8.5   430   110    error - divine failed with signal 11 1.6   200   25    false(unreach-call) 1.9   130 23    timeout 960   7100 8600 disqualified 890   520   7700 timeout (verification) 900    65 9500   timeout 900   5500 6200 error (7) 130   1100 1400 timeout 900   5400 6400 unknown 820     960   10000    
ldv-linux-3.0/usb_urb-drivers-vhost-vhost_net.ko_true-unreach-call.cil.out.i unreach-call error (134) 1.6   83 12    out of memory 100    14000   1000   error (134) 99    7800 980   true 17    540 150   true 110   4200 920 unknown 900    3800 8400   error - divine failed with exitcode 1 1.7   210   24    error - divine failed with signal 6 (.../lart/abstract/util.cpp: 190: encountered unknown parent instruction:) 1.7   200   23    true 150     3600 1600    true 84   1600 580 disqualified 11   180   150 error(unknown, verification-finished) 1.4  69 13   true 40   1200 320 true 75   1700 670 true 39   1200 390 unknown 160     1900   1900    
ldv-linux-3.0/usb_urb-drivers-video-arkfb.ko_true-unreach-call.cil.out.i unreach-call error (134) 1.4   76 10    error 880    2800   5800   false(valid-free) 1.2  100 13   true 13    470 100   true 100   1800 1300 unknown 700    11000 8400   unknown 8.5   430   120    error - divine failed with signal 11 1.6   210   23    true 21     570 200    true 39   1300 450 disqualified 7.2 170   100 true .88 79 10   true 44   1500 370 true 150   2700 1700 true 43   1400 380 true 49     1600   420    
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--gpu--drm--vmwgfx--vmwgfx.ko-ldv_main3_sequence_infinite_withcheck_stateful.cil.out.i unreach-call out of memory 110     15000 830    error 880    4800   6000   error (134) 5.9  450 55   false(unreach-call) 37    1500 330   timeout 960   6900 11000 false(unreach-call) 31    1700 350   error - divine failed with exitcode 1 2.3   250   28    error - divine failed with signal 6 (.../lart/abstract/util.cpp: 190: encountered unknown parent instruction:) 2.3   250   29    false(unreach-call) 62     2300 660    false(unreach-call) 890   2500 4800 disqualified 310   980   3200 error(unknown, verification-finished) 12    310 130   out of memory 600   15000 7900 timeout 900   4800 9800 out of memory 550   15000 6400 unknown 260     2800   2900    
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--input--mouse--synaptics_usb_false-termination.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i unreach-call error (134) .55  52 6.2  out of memory 510    13000   6200   out of memory 470    15000 4600   error 31    1100 280   false(unreach-call) 51   1100 500 false(unreach-call) 19    150 250   unknown 8.5   440   130    error - divine failed with signal 11 1.6   200   19    false(unreach-call) 7.0   150 95    false(unreach-call) 62   1600 630 disqualified 880   330   6000 error(unknown, verification-finished) .47 25 5.8 error (7) 72   2300 660 error (7) 220   2700 2900 error (7) 86   2800 770 false(unreach-call) 98     1100   1000    
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--input--mousedev_true-termination.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i unreach-call error (134) 1.5   75 13    out of memory 48    13000   590   out of memory 320    15000 2500   error 58    1900 440   timeout 900   4400 7300 false(unreach-call) 8.8  250 110   unknown 9.6   440   140    error - divine failed with signal 6 (.../lart/abstract/util.cpp: 190: encountered unknown parent instruction:) 1.6   210   19    timeout 900     6600 14000    false(unreach-call) 110   1900 1200 disqualified 31   300   480 error(unknown, verification-finished) 1.0  59 12   timeout 900   2500 11000 timeout 900   2100 11000 timeout 900   3000 10000 false(unreach-call) 71     880   710    
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--isdn--capi--kernelcapi.ko-ldv_main3_sequence_infinite_withcheck_stateful.cil.out.i unreach-call error (134) 1.1   110 8.0  error 880    1700   5300   false(unreach-call) 1.2  110 11   false(unreach-call) 18    660 140   exception 11   440 84 false(unreach-call) 1.1  180 10   error - divine failed with exitcode 1 1.7   210   24    error - divine failed with signal 6 (.../lart/abstract/util.cpp: 190: encountered unknown parent instruction:) 1.7   210   24    false(unreach-call) .99  170 9.0  exception 240   2700 2500 disqualified 890   1300   10000 error(unknown, verification-finished) 1.2  30 15   unknown 13   390 100 unknown 14   390 110 unknown 12   370 96 false(unreach-call) 94     760   1200    
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--media--dvb--dvb-usb--dvb-usb-dib0700.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i unreach-call error (134) 2.7   250 21    out of memory 85    13000   1100   false(unreach-call) 3.6  270 37   false(unreach-call) 23    840 180   false(unreach-call) 79   2900 1100 false(unreach-call) 2.4  430 28   unknown 9.4   460   130    error - divine failed with signal 11 1.9   220   24    false(unreach-call) 2.3   420 26    false(unreach-call) 380   4000 4100 disqualified 900   5900   9900 timeout (verification) 900    1100 4100   unknown 10   490 83 unknown 9.6 490 74 unknown 10   500 78 false(unreach-call) 280     2600   3000    
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--media--video--cpia2--cpia2.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i unreach-call error (134) 340     6100 3900    error 880    2100   4400   false(unreach-call) 2.1  190 17   error 35    930 280   timeout 970   9000 8400 unknown 110    280 1100   unknown 9.6   460   140    error - divine failed with signal 6 (.../lart/abstract/util.cpp: 190: encountered unknown parent instruction:) 1.8   220   29    timeout 900     330 12000    timeout 960   5900 6800 disqualified 89   870   1000 error(unknown, verification-finished) 5.3  190 50   timeout 900   3600 12000 timeout 900   2500 13000 timeout 900   2100 10000 out of memory 100     15000   1100    
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--media--video--mem2mem_testdev.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i unreach-call error (134) .89  68 7.3  out of memory 65    13000   790   false(unreach-call) .80 58 8.0 false(unreach-call) 14    510 120   false(unreach-call) 12   520 100 unknown 39    110 460   unknown 9.0   440   120    error - divine failed with signal 11 1.7   210   22    unknown .48  120 6.5  false(unreach-call) 58   1500 600 disqualified 9.9 200   130 error(unknown, cex-confirmation) 1.2  46 14   unknown 400   5000 4400 error (7) 720   3500 8300 unknown 400   4300 4000 false(unreach-call) 80     1100   970    
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--media--video--vivi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i unreach-call error (134) 1.1   84 8.1  out of memory 68    14000   860   error (134) 88    4000 540   error 31    1000 240   timeout 960   7700 9800 unknown 47    130 530   unknown 8.9   440   110    error - divine failed with signal 6 (.../lart/abstract/util.cpp: 190: encountered unknown parent instruction:) 1.7   210   26    unknown .59  140 5.5  false(unreach-call) 270   2100 2700 disqualified 880   280   11000 error(unknown, verification-finished) .96 60 11   timeout 900   4400 9300 timeout 900   4700 14000 timeout 900   5300 7800 false(unreach-call) 640     1300   4700    
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--mtd--chips--cfi_cmdset_0001.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i unreach-call error (134) 1.5   130 14    error 880    740   8300   error (42) 880    4200 11000   false(unreach-call) 13    530 110   false(unreach-call) 12   440 95 unknown 74    190 800   unknown 9.1   450   120    error - divine failed with signal 6 (.../lart/abstract/util.cpp: 190: encountered unknown parent instruction:) 1.7   210   21    unknown .89  150 11    false(unreach-call) 240   2700 2200 disqualified 14   190   210 error(unknown, verification-finished) 1.2  32 19   unknown 480   2900 3100 error (7) 180   850 1900 unknown 470   2900 3100 timeout 900     320   12000    
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--net--phy--dp83640.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i unreach-call error (134) 1.1   79 9.1  out of memory 51    13000   580   error (134) 3.5  330 44   false(unreach-call) 20    620 160   false(unreach-call) 46   2000 420 unknown 900    600 11000   error - divine failed with exitcode 1 1.7   210   20    error - divine failed with signal 11 1.7   210   25    false(unreach-call) 2.4   140 27    false(unreach-call) 170   2000 1800 disqualified 23   260   300 error(unknown, verification-finished) .89 52 10   timeout 900   3400 8900 timeout 900   4800 6900 timeout 900   4400 9300 false(unreach-call) 56     1200   610    
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--net--wireless--p54--p54usb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i unreach-call error (139) 320     190 3500    error 880    4300   4800   false(unreach-call) 2.2  210 30   false(unreach-call) 14    520 120   false(unreach-call) 13   530 95 false(unreach-call) .71 100 8.4 unknown 8.9   440   100    error - divine failed with signal 11 1.7   210   22    false(unreach-call) .65  94 6.9  false(unreach-call) 230   1800 2800 disqualified 24   410   310 error(unknown, verification-finished) .77 28 9.1 timeout 900   4400 11000 error (7) 170   1200 1800 timeout 900   4500 13000 false(unreach-call) 90     1100   1000    
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--scsi--libfc--libfc.ko-ldv_main5_sequence_infinite_withcheck_stateful.cil.out.i unreach-call out of memory 110     15000 830    error 880    8300   7200   false(unreach-call) 8.7  600 79   error 42    1400 370   false(unreach-call) 55   1100 510 false(unreach-call) 15    990 170   unknown 12     520   170    error - divine failed with signal 6 (.../lart/abstract/util.cpp: 190: encountered unknown parent instruction:) 2.3   250   31    timeout 900     1700 12000    timeout 910   1700 4700 disqualified 900   1500   7100 error(returned 1, slicing) 3.0  73 36   error (7) 650   5300 8100 timeout 900   3900 11000 error (7) 650   5300 8400 timeout 900     2500   5200    
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--staging--keucr--keucr.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.i unreach-call out of memory 110     15000 860    error 880    2600   5600   false(unreach-call) 4.2  320 40   false(unreach-call) 19    570 140   false(unreach-call) 360   1300 3000 false(unreach-call) 1.3  220 13   unknown 9.4   450   130    error - divine failed with signal 6 (.../lart/abstract/util.cpp: 190: encountered unknown parent instruction:) 1.8   220   27    false(unreach-call) 1.5   220 15    timeout 960   5400 7300 disqualified 900   11000   11000 timeout (verification) 900    3100 8500   error (7) 110   1900 1100 error (7) 500   2500 7400 error (7) 160   4700 1900 unknown 39     450   350    
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--usb--image--microtek.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i unreach-call error (134) .52  56 4.5  false(unreach-call) 35    2200   330   error (134) 17    600 190   false(unreach-call) 9.8  510 83   false(unreach-call) 8.4 400 80 false(unreach-call) .40 65 5.7 unknown 8.4   440   110    error - divine failed with signal 11 1.6   200   23    false(unreach-call) .34  58 4.6  false(unreach-call) 29   1200 300 disqualified 7.0 120   83 false(unreach-call) .70 22 9.3 unknown 48   870 380 error (7) 110   620 1400 unknown 47   830 430 false(unreach-call) 45     680   490    
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--usb--storage--usb-storage.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i unreach-call timeout 900     15000 10000    error 880    1700   11000   false(unreach-call) 8.3  570 73   false(unreach-call) 17    570 140   false(unreach-call) 23   780 220 false(unreach-call) 1.3  220 13   unknown 9.2   450   120    error - divine failed with signal 6 (.../lart/abstract/util.cpp: 190: encountered unknown parent instruction:) 1.8   220   25    false(unreach-call) 1.2   210 12    false(unreach-call) 320   2900 3600 disqualified 900   4700   10000 error(unknown, verification-finished) 1.5  51 16   error (7) 440   5200 5000 error (7) 810   4800 8600 error (7) 450   5100 6100 unknown 42     500   340    
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--vhost--vhost_net.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.i unreach-call error (134) 110     3000 1100    error (42) 880    6800   5700   error (134) 3.0  230 35   false(unreach-call) 20    610 160   false(unreach-call) 14   550 120 false(unreach-call) 5.2  270 76   error - divine failed with exitcode 1 1.8   220   21    error - divine failed with signal 6 (.../lart/abstract/util.cpp: 190: encountered unknown parent instruction:) 1.8   220   22    false(unreach-call) 7.2   310 85    false(unreach-call) 290   1600 2400 disqualified 35   720   460 error(unknown, verification-finished) 1.8  78 25   timeout 900   6200 7000 error (7) 510   2400 5000 timeout 900   6000 5800 unknown 190     1400   2300    
ldv-linux-3.4-simple/32_7_cilled_false-unreach-call_const_ok_linux-32_1-drivers--video--aty--atyfb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i unreach-call error (134) 13     1100 97    error 880    4300   5900   false(unreach-call) 2.6  180 23   timeout 900    6200 11000   timeout 960   7600 9000 unknown 900    1900 8300   unknown 9.4   460   130    error - divine failed with signal 6 (.../lart/abstract/util.cpp: 190: encountered unknown parent instruction:) 1.8   220   22    true 190     910 1600    timeout 960   5900 9200 disqualified 900   410   11000 error(unknown, verification-finished) 3.0  130 43   timeout 900   5100 8700 timeout 900   4000 11000 timeout 900   6400 12000 unknown 330     6400   2300    
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-mtd-chips-cfi_cmdset_0001.cil.out.i unreach-call error (134) 1.2   180 10    false(unreach-call) 830    2300   8700   out of memory 200    15000 2500   error (parsing failed) 9.7  720 83   error (parsing failed) 9.9 730 82 unknown 20    190 280   unknown 9.2   440   140    error - divine failed with signal 6 (.../lart/abstract/util.cpp: 190: encountered unknown parent instruction:) 1.8   210   26    unknown .42  110 4.9  error (parsing failed) 9.8 710 76 disqualified 7.7 140   96 error(unknown, verification-finished) 1.0  33 13   error (7) 17   530 130 error (7) 16   510 150 error (7) 17   500 140 unknown 45     380   400    
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-phy-dp83640.cil.out.i unreach-call error (134) 2.1   260 18    out of memory 39    12000   570   error (134) 5.0  240 57   error 44    2300 410   false(unreach-call) 86   4000 760 unknown 25    250 330   error - divine failed with exitcode 1 1.9   210   21    error - divine failed with signal 11 1.9   210   24    unknown .73  180 7.7  false(unreach-call) 540   4100 3200 disqualified 12   210   160 timeout (verification) 900    2600 9000   error (7) 18   660 160 error (7) 18   650 140 error (7) 17   580 140 false(unreach-call) 180     2900   2000    
ldv-linux-3.4-simple/32_7_cpp_false-unreach-call_single_drivers-net-wireless-mwl8k.cil.out.i unreach-call error (134) 560     1400 5700