1// +build amd64 2// errorcheck -0 -d=ssa/prove/debug=1 3 4package main 5 6func f0a(a []int) int { 7 x := 0 8 for i := range a { // ERROR "Induction variable: limits \[0,\?\), increment 1$" 9 x += a[i] // ERROR "(\([0-9]+\) )?Proved IsInBounds$" 10 } 11 return x 12} 13 14func f0b(a []int) int { 15 x := 0 16 for i := range a { // ERROR "Induction variable: limits \[0,\?\), increment 1$" 17 b := a[i:] // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$" 18 x += b[0] 19 } 20 return x 21} 22 23func f0c(a []int) int { 24 x := 0 25 for i := range a { // ERROR "Induction variable: limits \[0,\?\), increment 1$" 26 b := a[:i+1] // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$" 27 x += b[0] 28 } 29 return x 30} 31 32func f1(a []int) int { 33 x := 0 34 for _, i := range a { // ERROR "Induction variable: limits \[0,\?\), increment 1$" 35 x += i 36 } 37 return x 38} 39 40func f2(a []int) int { 41 x := 0 42 for i := 1; i < len(a); i++ { // ERROR "Induction variable: limits \[1,\?\), increment 1$" 43 x += a[i] // ERROR "(\([0-9]+\) )?Proved IsInBounds$" 44 } 45 return x 46} 47 48func f4(a [10]int) int { 49 x := 0 50 for i := 0; i < len(a); i += 2 { // ERROR "Induction variable: limits \[0,10\), increment 2$" 51 x += a[i] // ERROR "(\([0-9]+\) )?Proved IsInBounds$" 52 } 53 return x 54} 55 56func f5(a [10]int) int { 57 x := 0 58 for i := -10; i < len(a); i += 2 { // ERROR "Induction variable: limits \[-10,10\), increment 2$" 59 x += a[i] 60 } 61 return x 62} 63 64func f6(a []int) { 65 for i := range a { // ERROR "Induction variable: limits \[0,\?\), increment 1$" 66 b := a[0:i] // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$" 67 f6(b) 68 } 69} 70 71func g0a(a string) int { 72 x := 0 73 for i := 0; i < len(a); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$" 74 x += int(a[i]) // ERROR "(\([0-9]+\) )?Proved IsInBounds$" 75 } 76 return x 77} 78 79func g0b(a string) int { 80 x := 0 81 for i := 0; len(a) > i; i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$" 82 x += int(a[i]) // ERROR "(\([0-9]+\) )?Proved IsInBounds$" 83 } 84 return x 85} 86 87func g0c(a string) int { 88 x := 0 89 for i := len(a); i > 0; i-- { // ERROR "Induction variable: limits \(0,\?\], increment 1$" 90 x += int(a[i-1]) // ERROR "(\([0-9]+\) )?Proved IsInBounds$" 91 } 92 return x 93} 94 95func g0d(a string) int { 96 x := 0 97 for i := len(a); 0 < i; i-- { // ERROR "Induction variable: limits \(0,\?\], increment 1$" 98 x += int(a[i-1]) // ERROR "(\([0-9]+\) )?Proved IsInBounds$" 99 } 100 return x 101} 102 103func g0e(a string) int { 104 x := 0 105 for i := len(a) - 1; i >= 0; i-- { // ERROR "Induction variable: limits \[0,\?\], increment 1$" 106 x += int(a[i]) // ERROR "(\([0-9]+\) )?Proved IsInBounds$" 107 } 108 return x 109} 110 111func g0f(a string) int { 112 x := 0 113 for i := len(a) - 1; 0 <= i; i-- { // ERROR "Induction variable: limits \[0,\?\], increment 1$" 114 x += int(a[i]) // ERROR "(\([0-9]+\) )?Proved IsInBounds$" 115 } 116 return x 117} 118 119func g1() int { 120 a := "evenlength" 121 x := 0 122 for i := 0; i < len(a); i += 2 { // ERROR "Induction variable: limits \[0,10\), increment 2$" 123 x += int(a[i]) // ERROR "(\([0-9]+\) )?Proved IsInBounds$" 124 } 125 return x 126} 127 128func g2() int { 129 a := "evenlength" 130 x := 0 131 for i := 0; i < len(a); i += 2 { // ERROR "Induction variable: limits \[0,10\), increment 2$" 132 j := i 133 if a[i] == 'e' { // ERROR "(\([0-9]+\) )?Proved IsInBounds$" 134 j = j + 1 135 } 136 x += int(a[j]) 137 } 138 return x 139} 140 141func g3a() { 142 a := "this string has length 25" 143 for i := 0; i < len(a); i += 5 { // ERROR "Induction variable: limits \[0,25\), increment 5$" 144 useString(a[i:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$" 145 useString(a[:i+3]) 146 } 147} 148 149func g3b(a string) { 150 for i := 0; i < len(a); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$" 151 useString(a[i+1:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$" 152 } 153} 154 155func g3c(a string) { 156 for i := 0; i < len(a); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$" 157 useString(a[:i+1]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$" 158 } 159} 160 161func h1(a []byte) { 162 c := a[:128] 163 for i := range c { // ERROR "Induction variable: limits \[0,128\), increment 1$" 164 c[i] = byte(i) // ERROR "(\([0-9]+\) )?Proved IsInBounds$" 165 } 166} 167 168func h2(a []byte) { 169 for i := range a[:128] { // ERROR "Induction variable: limits \[0,128\), increment 1$" 170 a[i] = byte(i) 171 } 172} 173 174func k0(a [100]int) [100]int { 175 for i := 10; i < 90; i++ { // ERROR "Induction variable: limits \[10,90\), increment 1$" 176 a[i-11] = i 177 a[i-10] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$" 178 a[i-5] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$" 179 a[i] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$" 180 a[i+5] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$" 181 a[i+10] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$" 182 a[i+11] = i 183 } 184 return a 185} 186 187func k1(a [100]int) [100]int { 188 for i := 10; i < 90; i++ { // ERROR "Induction variable: limits \[10,90\), increment 1$" 189 useSlice(a[:i-11]) 190 useSlice(a[:i-10]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$" 191 useSlice(a[:i-5]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$" 192 useSlice(a[:i]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$" 193 useSlice(a[:i+5]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$" 194 useSlice(a[:i+10]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$" 195 useSlice(a[:i+11]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$" 196 useSlice(a[:i+12]) 197 198 } 199 return a 200} 201 202func k2(a [100]int) [100]int { 203 for i := 10; i < 90; i++ { // ERROR "Induction variable: limits \[10,90\), increment 1$" 204 useSlice(a[i-11:]) 205 useSlice(a[i-10:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$" 206 useSlice(a[i-5:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$" 207 useSlice(a[i:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$" 208 useSlice(a[i+5:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$" 209 useSlice(a[i+10:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$" 210 useSlice(a[i+11:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$" 211 useSlice(a[i+12:]) 212 } 213 return a 214} 215 216func k3(a [100]int) [100]int { 217 for i := -10; i < 90; i++ { // ERROR "Induction variable: limits \[-10,90\), increment 1$" 218 a[i+9] = i 219 a[i+10] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$" 220 a[i+11] = i 221 } 222 return a 223} 224 225func k3neg(a [100]int) [100]int { 226 for i := 89; i > -11; i-- { // ERROR "Induction variable: limits \(-11,89\], increment 1$" 227 a[i+9] = i 228 a[i+10] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$" 229 a[i+11] = i 230 } 231 return a 232} 233 234func k3neg2(a [100]int) [100]int { 235 for i := 89; i >= -10; i-- { // ERROR "Induction variable: limits \[-10,89\], increment 1$" 236 a[i+9] = i 237 a[i+10] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$" 238 a[i+11] = i 239 } 240 return a 241} 242 243func k4(a [100]int) [100]int { 244 min := (-1) << 63 245 for i := min; i < min+50; i++ { // ERROR "Induction variable: limits \[-9223372036854775808,-9223372036854775758\), increment 1$" 246 a[i-min] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$" 247 } 248 return a 249} 250 251func k5(a [100]int) [100]int { 252 max := (1 << 63) - 1 253 for i := max - 50; i < max; i++ { // ERROR "Induction variable: limits \[9223372036854775757,9223372036854775807\), increment 1$" 254 a[i-max+50] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$" 255 a[i-(max-70)] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$" 256 } 257 return a 258} 259 260func d1(a [100]int) [100]int { 261 for i := 0; i < 100; i++ { // ERROR "Induction variable: limits \[0,100\), increment 1$" 262 for j := 0; j < i; j++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$" 263 a[j] = 0 // ERROR "Proved IsInBounds$" 264 a[j+1] = 0 // FIXME: this boundcheck should be eliminated 265 a[j+2] = 0 266 } 267 } 268 return a 269} 270 271func d2(a [100]int) [100]int { 272 for i := 0; i < 100; i++ { // ERROR "Induction variable: limits \[0,100\), increment 1$" 273 for j := 0; i > j; j++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$" 274 a[j] = 0 // ERROR "Proved IsInBounds$" 275 a[j+1] = 0 // FIXME: this boundcheck should be eliminated 276 a[j+2] = 0 277 } 278 } 279 return a 280} 281 282func d3(a [100]int) [100]int { 283 for i := 0; i <= 99; i++ { // ERROR "Induction variable: limits \[0,99\], increment 1$" 284 for j := 0; j <= i-1; j++ { // ERROR "Induction variable: limits \[0,\?\], increment 1$" 285 a[j] = 0 // ERROR "Proved IsInBounds$" 286 a[j+1] = 0 // ERROR "Proved IsInBounds$" 287 a[j+2] = 0 288 } 289 } 290 return a 291} 292 293func nobce1() { 294 // tests overflow of max-min 295 a := int64(9223372036854774057) 296 b := int64(-1547) 297 z := int64(1337) 298 299 if a%z == b%z { 300 panic("invalid test: modulos should differ") 301 } 302 303 for i := b; i < a; i += z { 304 // No induction variable is possible because i will overflow a first iteration. 305 useString("foobar") 306 } 307} 308 309func nobce2(a string) { 310 for i := int64(0); i < int64(len(a)); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$" 311 useString(a[i:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$" 312 } 313 for i := int64(0); i < int64(len(a))-31337; i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$" 314 useString(a[i:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$" 315 } 316 for i := int64(0); i < int64(len(a))+int64(-1<<63); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$" 317 useString(a[i:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$" 318 } 319 j := int64(len(a)) - 123 320 for i := int64(0); i < j+123+int64(-1<<63); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$" 321 useString(a[i:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$" 322 } 323 for i := int64(0); i < j+122+int64(-1<<63); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$" 324 // len(a)-123+122+MinInt overflows when len(a) == 0, so a bound check is needed here 325 useString(a[i:]) 326 } 327} 328 329func nobce3(a [100]int64) [100]int64 { 330 min := int64((-1) << 63) 331 max := int64((1 << 63) - 1) 332 for i := min; i < max; i++ { // ERROR "Induction variable: limits \[-9223372036854775808,9223372036854775807\), increment 1$" 333 a[i] = i 334 } 335 return a 336} 337 338func issue26116a(a []int) { 339 // There is no induction variable here. The comparison is in the wrong direction. 340 for i := 3; i > 6; i++ { 341 a[i] = 0 342 } 343 for i := 7; i < 3; i-- { 344 a[i] = 1 345 } 346} 347 348//go:noinline 349func useString(a string) { 350} 351 352//go:noinline 353func useSlice(a []int) { 354} 355 356func main() { 357} 358