test/loopbce.go

   1 // +build amd64
   2 // errorcheck -0 -d=ssa/prove/debug=1
   3
   4 package main
   5
   6 func f0a(a []int) int {
   7         x := 0
   8         for i := range a { // ERROR "Induction variable with minimum 0 and increment 1$"
   9                 x += a[i] // ERROR "Proved IsInBounds$"
  10         }
  11         return x
  12 }
  13
  14 func f0b(a []int) int {
  15         x := 0
  16         for i := range a { // ERROR "Induction variable with minimum 0 and increment 1$"
  17                 b := a[i:] // ERROR "Proved IsSliceInBounds$"
  18                 x += b[0]
  19         }
  20         return x
  21 }
  22
  23 func f0c(a []int) int {
  24         x := 0
  25         for i := range a { // ERROR "Induction variable with minimum 0 and increment 1$"
  26                 b := a[:i+1] // ERROR "Proved IsSliceInBounds$"
  27                 x += b[0]
  28         }
  29         return x
  30 }
  31
  32 func f1(a []int) int {
  33         x := 0
  34         for _, i := range a { // ERROR "Induction variable with minimum 0 and increment 1"
  35                 x += i
  36         }
  37         return x
  38 }
  39
  40 func f2(a []int) int {
  41         x := 0
  42         for i := 1; i < len(a); i++ { // ERROR "Induction variable with minimum 1 and increment 1$"
  43                 x += a[i] // ERROR "Proved IsInBounds$"
  44         }
  45         return x
  46 }
  47
  48 func f4(a [10]int) int {
  49         x := 0
  50         for i := 0; i < len(a); i += 2 { // ERROR "Induction variable with minimum 0 and increment 2$"
  51                 x += a[i] // ERROR "Proved IsInBounds$"
  52         }
  53         return x
  54 }
  55
  56 func f5(a [10]int) int {
  57         x := 0
  58         for i := -10; i < len(a); i += 2 { // ERROR "Induction variable with minimum -10 and increment 2$"
  59                 x += a[i]
  60         }
  61         return x
  62 }
  63
  64 func f6(a []int) {
  65         for i := range a { // ERROR "Induction variable with minimum 0 and increment 1$"
  66                 b := a[0:i] // ERROR "Proved IsSliceInBounds$"
  67                 f6(b)
  68         }
  69 }
  70
  71 func g0a(a string) int {
  72         x := 0
  73         for i := 0; i < len(a); i++ { // ERROR "Induction variable with minimum 0 and increment 1$"
  74                 x += int(a[i]) // ERROR "Proved IsInBounds$"
  75         }
  76         return x
  77 }
  78
  79 func g0b(a string) int {
  80         x := 0
  81         for i := 0; len(a) > i; i++ { // ERROR "Induction variable with minimum 0 and increment 1$"
  82                 x += int(a[i]) // ERROR "Proved IsInBounds$"
  83         }
  84         return x
  85 }
  86
  87 func g1() int {
  88         a := "evenlength"
  89         x := 0
  90         for i := 0; i < len(a); i += 2 { // ERROR "Induction variable with minimum 0 and increment 2$"
  91                 x += int(a[i]) // ERROR "Proved IsInBounds$"
  92         }
  93         return x
  94 }
  95
  96 func g2() int {
  97         a := "evenlength"
  98         x := 0
  99         for i := 0; i < len(a); i += 2 { // ERROR "Induction variable with minimum 0 and increment 2$"
 100                 j := i
 101                 if a[i] == 'e' { // ERROR "Proved IsInBounds$"
 102                         j = j + 1
 103                 }
 104                 x += int(a[j])
 105         }
 106         return x
 107 }
 108
 109 func g3a() {
 110         a := "this string has length 25"
 111         for i := 0; i < len(a); i += 5 { // ERROR "Induction variable with minimum 0 and increment 5$"
 112                 useString(a[i:]) // ERROR "Proved IsSliceInBounds$"
 113                 useString(a[:i+3])
 114         }
 115 }
 116
 117 func g3b(a string) {
 118         for i := 0; i < len(a); i++ { // ERROR "Induction variable with minimum 0 and increment 1$"
 119                 useString(a[i+1:]) // ERROR "Proved IsSliceInBounds$"
 120         }
 121 }
 122
 123 func g3c(a string) {
 124         for i := 0; i < len(a); i++ { // ERROR "Induction variable with minimum 0 and increment 1$"
 125                 useString(a[:i+1]) // ERROR "Proved IsSliceInBounds$"
 126         }
 127 }
 128
 129 func h1(a []byte) {
 130         c := a[:128]
 131         for i := range c { // ERROR "Induction variable with minimum 0 and increment 1$"
 132                 c[i] = byte(i) // ERROR "Proved IsInBounds$"
 133         }
 134 }
 135
 136 func h2(a []byte) {
 137         for i := range a[:128] { // ERROR "Induction variable with minimum 0 and increment 1$"
 138                 a[i] = byte(i)
 139         }
 140 }
 141
 142 func k0(a [100]int) [100]int {
 143         for i := 10; i < 90; i++ { // ERROR "Induction variable with minimum 10 and increment 1$"
 144                 a[i-11] = i
 145                 a[i-10] = i // ERROR "Proved IsInBounds$"
 146                 a[i-5] = i  // ERROR "Proved IsInBounds$"
 147                 a[i] = i    // ERROR "Proved IsInBounds$"
 148                 a[i+5] = i  // ERROR "Proved IsInBounds$"
 149                 a[i+10] = i // ERROR "Proved IsInBounds$"
 150                 a[i+11] = i
 151         }
 152         return a
 153 }
 154
 155 func k1(a [100]int) [100]int {
 156         for i := 10; i < 90; i++ { // ERROR "Induction variable with minimum 10 and increment 1$"
 157                 useSlice(a[:i-11])
 158                 useSlice(a[:i-10]) // ERROR "Proved IsSliceInBounds$"
 159                 useSlice(a[:i-5])  // ERROR "Proved IsSliceInBounds$"
 160                 useSlice(a[:i])    // ERROR "Proved IsSliceInBounds$"
 161                 useSlice(a[:i+5])  // ERROR "Proved IsSliceInBounds$"
 162                 useSlice(a[:i+10]) // ERROR "Proved IsSliceInBounds$"
 163                 useSlice(a[:i+11]) // ERROR "Proved IsSliceInBounds$"
 164                 useSlice(a[:i+12])
 165
 166         }
 167         return a
 168 }
 169
 170 func k2(a [100]int) [100]int {
 171         for i := 10; i < 90; i++ { // ERROR "Induction variable with minimum 10 and increment 1$"
 172                 useSlice(a[i-11:])
 173                 useSlice(a[i-10:]) // ERROR "Proved IsSliceInBounds$"
 174                 useSlice(a[i-5:])  // ERROR "Proved IsSliceInBounds$"
 175                 useSlice(a[i:])    // ERROR "Proved IsSliceInBounds$"
 176                 useSlice(a[i+5:])  // ERROR "Proved IsSliceInBounds$"
 177                 useSlice(a[i+10:]) // ERROR "Proved IsSliceInBounds$"
 178                 useSlice(a[i+11:]) // ERROR "Proved IsSliceInBounds$"
 179                 useSlice(a[i+12:])
 180         }
 181         return a
 182 }
 183
 184 func k3(a [100]int) [100]int {
 185         for i := -10; i < 90; i++ { // ERROR "Induction variable with minimum -10 and increment 1$"
 186                 a[i+9] = i
 187                 a[i+10] = i // ERROR "Proved IsInBounds$"
 188                 a[i+11] = i
 189         }
 190         return a
 191 }
 192
 193 func k4(a [100]int) [100]int {
 194         min := (-1) << 63
 195         for i := min; i < min+50; i++ { // ERROR "Induction variable with minimum -9223372036854775808 and increment 1$"
 196                 a[i-min] = i // ERROR "Proved IsInBounds$"
 197         }
 198         return a
 199 }
 200
 201 func k5(a [100]int) [100]int {
 202         max := (1 << 63) - 1
 203         for i := max - 50; i < max; i++ { // ERROR "Induction variable with minimum 9223372036854775757 and increment 1$"
 204                 a[i-max+50] = i   // ERROR "Proved IsInBounds$"
 205                 a[i-(max-70)] = i // ERROR "Proved IsInBounds$"
 206         }
 207         return a
 208 }
 209
 210 func nobce1() {
 211         // tests overflow of max-min
 212         a := int64(9223372036854774057)
 213         b := int64(-1547)
 214         z := int64(1337)
 215
 216         if a%z == b%z {
 217                 panic("invalid test: modulos should differ")
 218         }
 219
 220         for i := b; i < a; i += z {
 221                 // No induction variable is possible because i will overflow a first iteration.
 222                 useString("foobar")
 223         }
 224 }
 225
 226 func nobce2(a string) {
 227         for i := int64(0); i < int64(len(a)); i++ { // ERROR "Induction variable with minimum 0 and increment 1$"
 228                 useString(a[i:]) // ERROR "Proved IsSliceInBounds$"
 229         }
 230         for i := int64(0); i < int64(len(a))-31337; i++ { // ERROR "Induction variable with minimum 0 and increment 1$"
 231                 useString(a[i:]) // ERROR "Proved IsSliceInBounds$"
 232         }
 233         for i := int64(0); i < int64(len(a))+int64(-1<<63); i++ { // ERROR "Induction variable with minimum 0 and increment 1$"
 234                 // tests an overflow of StringLen-MinInt64
 235                 useString(a[i:])
 236         }
 237 }
 238
 239 func nobce3(a [100]int64) [100]int64 {
 240         min := int64((-1) << 63)
 241         max := int64((1 << 63) - 1)
 242         for i := min; i < max; i++ { // ERROR "Induction variable with minimum -9223372036854775808 and increment 1$"
 243                 a[i] = i
 244         }
 245         return a
 246 }
 247
 248 //go:noinline
 249 func useString(a string) {
 250 }
 251
 252 //go:noinline
 253 func useSlice(a []int) {
 254 }
 255
 256 func main() {
 257 }