@@ -9,15 +9,15 @@ import "math"
99func f0a (a []int ) int {
1010 x := 0
1111 for i := range a { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
12- x += a [i ] // ERROR "(\([0-9]+\) )? Proved IsInBounds$"
12+ x += a [i ] // ERROR "Proved IsInBounds$"
1313 }
1414 return x
1515}
1616
1717func f0b (a []int ) int {
1818 x := 0
1919 for i := range a { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
20- b := a [i :] // ERROR "(\([0-9]+\) )? Proved IsSliceInBounds$"
20+ b := a [i :] // ERROR "Proved IsSliceInBounds$"
2121 x += b [0 ]
2222 }
2323 return x
@@ -26,8 +26,8 @@ func f0b(a []int) int {
2626func f0c (a []int ) int {
2727 x := 0
2828 for i := range a { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
29- b := a [:i + 1 ] // ERROR "(\([0-9]+\) )? Proved IsSliceInBounds$"
30- x += b [0 ] // ERROR "(\([0-9]+\) )? Proved IsInBounds$"
29+ b := a [:i + 1 ] // ERROR "Proved IsSliceInBounds$"
30+ x += b [0 ] // ERROR "Proved IsInBounds$"
3131 }
3232 return x
3333}
@@ -43,15 +43,15 @@ func f1(a []int) int {
4343func f2 (a []int ) int {
4444 x := 0
4545 for i := 1 ; i < len (a ); i ++ { // ERROR "Induction variable: limits \[1,\?\), increment 1$"
46- x += a [i ] // ERROR "(\([0-9]+\) )? Proved IsInBounds$"
46+ x += a [i ] // ERROR "Proved IsInBounds$"
4747 }
4848 return x
4949}
5050
5151func f4 (a [10 ]int ) int {
5252 x := 0
5353 for i := 0 ; i < len (a ); i += 2 { // ERROR "Induction variable: limits \[0,8\], increment 2$"
54- x += a [i ] // ERROR "(\([0-9]+\) )? Proved IsInBounds$"
54+ x += a [i ] // ERROR "Proved IsInBounds$"
5555 }
5656 return x
5757}
@@ -91,55 +91,55 @@ func f5_int8(a [10]int) int {
9191//go:noinline
9292func f6 (a []int ) {
9393 for i := range a { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
94- b := a [0 :i ] // ERROR "(\([0-9]+\) )? Proved IsSliceInBounds$"
94+ b := a [0 :i ] // ERROR "Proved IsSliceInBounds$"
9595 f6 (b )
9696 }
9797}
9898
9999func g0a (a string ) int {
100100 x := 0
101101 for i := 0 ; i < len (a ); i ++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
102- x += int (a [i ]) // ERROR "(\([0-9]+\) )? Proved IsInBounds$"
102+ x += int (a [i ]) // ERROR "Proved IsInBounds$"
103103 }
104104 return x
105105}
106106
107107func g0b (a string ) int {
108108 x := 0
109109 for i := 0 ; len (a ) > i ; i ++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
110- x += int (a [i ]) // ERROR "(\([0-9]+\) )? Proved IsInBounds$"
110+ x += int (a [i ]) // ERROR "Proved IsInBounds$"
111111 }
112112 return x
113113}
114114
115115func g0c (a string ) int {
116116 x := 0
117117 for i := len (a ); i > 0 ; i -- { // ERROR "Induction variable: limits \(0,\?\], increment 1$"
118- x += int (a [i - 1 ]) // ERROR "(\([0-9]+\) )? Proved IsInBounds$"
118+ x += int (a [i - 1 ]) // ERROR "Proved IsInBounds$"
119119 }
120120 return x
121121}
122122
123123func g0d (a string ) int {
124124 x := 0
125125 for i := len (a ); 0 < i ; i -- { // ERROR "Induction variable: limits \(0,\?\], increment 1$"
126- x += int (a [i - 1 ]) // ERROR "(\([0-9]+\) )? Proved IsInBounds$"
126+ x += int (a [i - 1 ]) // ERROR "Proved IsInBounds$"
127127 }
128128 return x
129129}
130130
131131func g0e (a string ) int {
132132 x := 0
133133 for i := len (a ) - 1 ; i >= 0 ; i -- { // ERROR "Induction variable: limits \[0,\?\], increment 1$"
134- x += int (a [i ]) // ERROR "(\([0-9]+\) )? Proved IsInBounds$"
134+ x += int (a [i ]) // ERROR "Proved IsInBounds$"
135135 }
136136 return x
137137}
138138
139139func g0f (a string ) int {
140140 x := 0
141141 for i := len (a ) - 1 ; 0 <= i ; i -- { // ERROR "Induction variable: limits \[0,\?\], increment 1$"
142- x += int (a [i ]) // ERROR "(\([0-9]+\) )? Proved IsInBounds$"
142+ x += int (a [i ]) // ERROR "Proved IsInBounds$"
143143 }
144144 return x
145145}
@@ -148,7 +148,7 @@ func g1() int {
148148 a := "evenlength"
149149 x := 0
150150 for i := 0 ; i < len (a ); i += 2 { // ERROR "Induction variable: limits \[0,8\], increment 2$"
151- x += int (a [i ]) // ERROR "(\([0-9]+\) )? Proved IsInBounds$"
151+ x += int (a [i ]) // ERROR "Proved IsInBounds$"
152152 }
153153 return x
154154}
@@ -158,7 +158,7 @@ func g2() int {
158158 x := 0
159159 for i := 0 ; i < len (a ); i += 2 { // ERROR "Induction variable: limits \[0,8\], increment 2$"
160160 j := i
161- if a [i ] == 'e' { // ERROR "(\([0-9]+\) )? Proved IsInBounds$"
161+ if a [i ] == 'e' { // ERROR "Proved IsInBounds$"
162162 j = j + 1
163163 }
164164 x += int (a [j ])
@@ -169,29 +169,29 @@ func g2() int {
169169func g3a () {
170170 a := "this string has length 25"
171171 for i := 0 ; i < len (a ); i += 5 { // ERROR "Induction variable: limits \[0,20\], increment 5$"
172- useString (a [i :]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds $"
173- useString (a [:i + 3 ]) // ERROR "(\([0-9]+\) )? Proved IsSliceInBounds$"
174- useString (a [:i + 5 ]) // ERROR "(\([0-9]+\) )? Proved IsSliceInBounds$"
172+ useString (a [i :]) // ERROR "Proved IsSliceInBounds$" "Proved slicemask not needed \(by limit\) $"
173+ useString (a [:i + 3 ]) // ERROR "Proved IsSliceInBounds$"
174+ useString (a [:i + 5 ]) // ERROR "Proved IsSliceInBounds$"
175175 useString (a [:i + 6 ])
176176 }
177177}
178178
179179func g3b (a string ) {
180180 for i := 0 ; i < len (a ); i ++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
181- useString (a [i + 1 :]) // ERROR "(\([0-9]+\) )? Proved IsSliceInBounds$"
181+ useString (a [i + 1 :]) // ERROR "Proved IsSliceInBounds$"
182182 }
183183}
184184
185185func g3c (a string ) {
186186 for i := 0 ; i < len (a ); i ++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
187- useString (a [:i + 1 ]) // ERROR "(\([0-9]+\) )? Proved IsSliceInBounds$"
187+ useString (a [:i + 1 ]) // ERROR "Proved IsSliceInBounds$"
188188 }
189189}
190190
191191func h1 (a []byte ) {
192192 c := a [:128 ]
193193 for i := range c { // ERROR "Induction variable: limits \[0,128\), increment 1$"
194- c [i ] = byte (i ) // ERROR "(\([0-9]+\) )? Proved IsInBounds$"
194+ c [i ] = byte (i ) // ERROR "Proved IsInBounds$"
195195 }
196196}
197197
@@ -208,11 +208,11 @@ func k0(a [100]int) [100]int {
208208 continue
209209 }
210210 a [i - 11 ] = i
211- a [i - 10 ] = i // ERROR "(\([0-9]+\) )? Proved IsInBounds$"
212- a [i - 5 ] = i // ERROR "(\([0-9]+\) )? Proved IsInBounds$"
213- a [i ] = i // ERROR "(\([0-9]+\) )? Proved IsInBounds$"
214- a [i + 5 ] = i // ERROR "(\([0-9]+\) )? Proved IsInBounds$"
215- a [i + 10 ] = i // ERROR "(\([0-9]+\) )? Proved IsInBounds$"
211+ a [i - 10 ] = i // ERROR "Proved IsInBounds$"
212+ a [i - 5 ] = i // ERROR "Proved IsInBounds$"
213+ a [i ] = i // ERROR "Proved IsInBounds$"
214+ a [i + 5 ] = i // ERROR "Proved IsInBounds$"
215+ a [i + 10 ] = i // ERROR "Proved IsInBounds$"
216216 a [i + 11 ] = i
217217 }
218218 return a
@@ -225,12 +225,12 @@ func k1(a [100]int) [100]int {
225225 continue
226226 }
227227 useSlice (a [:i - 11 ])
228- useSlice (a [:i - 10 ]) // ERROR "(\([0-9]+\) )? Proved IsSliceInBounds$"
229- useSlice (a [:i - 5 ]) // ERROR "(\([0-9]+\) )? Proved IsSliceInBounds$"
230- useSlice (a [:i ]) // ERROR "(\([0-9]+\) )? Proved IsSliceInBounds$"
231- useSlice (a [:i + 5 ]) // ERROR "(\([0-9]+\) )? Proved IsSliceInBounds$"
232- useSlice (a [:i + 10 ]) // ERROR "(\([0-9]+\) )? Proved IsSliceInBounds$"
233- useSlice (a [:i + 11 ]) // ERROR "(\([0-9]+\) )? Proved IsSliceInBounds$"
228+ useSlice (a [:i - 10 ]) // ERROR "Proved IsSliceInBounds$"
229+ useSlice (a [:i - 5 ]) // ERROR "Proved IsSliceInBounds$"
230+ useSlice (a [:i ]) // ERROR "Proved IsSliceInBounds$"
231+ useSlice (a [:i + 5 ]) // ERROR "Proved IsSliceInBounds$"
232+ useSlice (a [:i + 10 ]) // ERROR "Proved IsSliceInBounds$"
233+ useSlice (a [:i + 11 ]) // ERROR "Proved IsSliceInBounds$"
234234 useSlice (a [:i + 12 ])
235235
236236 }
@@ -243,13 +243,13 @@ func k2(a [100]int) [100]int {
243243 // This is a trick to prohibit sccp to optimize out the following out of bound check
244244 continue
245245 }
246- useSlice (a [i - 11 :])
247- useSlice (a [i - 10 :]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds $"
248- useSlice (a [i - 5 :]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds $"
249- useSlice (a [i :]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds $"
250- useSlice (a [i + 5 :]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds $"
251- useSlice (a [i + 10 :]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds $"
252- useSlice (a [i + 11 :]) // ERROR "(\([0-9]+\) )? Proved IsSliceInBounds$"
246+ useSlice (a [i - 11 :]) // ERROR "Proved slicemask not needed \(by limit\)$"
247+ useSlice (a [i - 10 :]) // ERROR "Proved IsSliceInBounds$" "Proved slicemask not needed \(by limit\) $"
248+ useSlice (a [i - 5 :]) // ERROR "Proved IsSliceInBounds$" "Proved slicemask not needed \(by limit\) $"
249+ useSlice (a [i :]) // ERROR "Proved IsSliceInBounds$" "Proved slicemask not needed \(by limit\) $"
250+ useSlice (a [i + 5 :]) // ERROR "Proved IsSliceInBounds$" "Proved slicemask not needed \(by limit\) $"
251+ useSlice (a [i + 10 :]) // ERROR "Proved IsSliceInBounds$" "Proved slicemask not needed \(by limit\) $"
252+ useSlice (a [i + 11 :]) // ERROR "Proved IsSliceInBounds$"
253253 useSlice (a [i + 12 :])
254254 }
255255 return a
@@ -262,7 +262,7 @@ func k3(a [100]int) [100]int {
262262 continue
263263 }
264264 a [i + 9 ] = i
265- a [i + 10 ] = i // ERROR "(\([0-9]+\) )? Proved IsInBounds$"
265+ a [i + 10 ] = i // ERROR "Proved IsInBounds$"
266266 a [i + 11 ] = i
267267 }
268268 return a
@@ -275,7 +275,7 @@ func k3neg(a [100]int) [100]int {
275275 continue
276276 }
277277 a [i + 9 ] = i
278- a [i + 10 ] = i // ERROR "(\([0-9]+\) )? Proved IsInBounds$"
278+ a [i + 10 ] = i // ERROR "Proved IsInBounds$"
279279 a [i + 11 ] = i
280280 }
281281 return a
@@ -288,7 +288,7 @@ func k3neg2(a [100]int) [100]int {
288288 continue
289289 }
290290 a [i + 9 ] = i
291- a [i + 10 ] = i // ERROR "(\([0-9]+\) )? Proved IsInBounds$"
291+ a [i + 10 ] = i // ERROR "Proved IsInBounds$"
292292 a [i + 11 ] = i
293293 }
294294 return a
@@ -299,16 +299,16 @@ func k4(a [100]int) [100]int {
299299 // and it isn't worth adding that special case to prove.
300300 min := (- 1 )<< 63 + 1
301301 for i := min ; i < min + 50 ; i ++ { // ERROR "Induction variable: limits \[-9223372036854775807,-9223372036854775757\), increment 1$"
302- a [i - min ] = i // ERROR "(\([0-9]+\) )? Proved IsInBounds$"
302+ a [i - min ] = i // ERROR "Proved IsInBounds$"
303303 }
304304 return a
305305}
306306
307307func k5 (a [100 ]int ) [100 ]int {
308308 max := (1 << 63 ) - 1
309309 for i := max - 50 ; i < max ; i ++ { // ERROR "Induction variable: limits \[9223372036854775757,9223372036854775807\), increment 1$"
310- a [i - max + 50 ] = i // ERROR "(\([0-9]+\) )? Proved IsInBounds$"
311- a [i - (max - 70 )] = i // ERROR "(\([0-9]+\) )? Proved IsInBounds$"
310+ a [i - max + 50 ] = i // ERROR "Proved IsInBounds$"
311+ a [i - (max - 70 )] = i // ERROR "Proved IsInBounds$"
312312 }
313313 return a
314314}
@@ -374,22 +374,22 @@ func d4() {
374374}
375375
376376func d5 () {
377- for i := int64 (math .MinInt64 + 9 ); i > math .MinInt64 + 2 ; i -= 4 { // ERROR "Induction variable: limits \[-9223372036854775803,-9223372036854775799\], increment 4"
377+ for i := int64 (math .MinInt64 + 9 ); i > math .MinInt64 + 2 ; i -= 4 { // ERROR "Induction variable: limits \[-9223372036854775803,-9223372036854775799\], increment 4$ "
378378 useString ("foo" )
379379 }
380- for i := int64 (math .MinInt64 + 8 ); i > math .MinInt64 + 2 ; i -= 4 { // ERROR "Induction variable: limits \[-9223372036854775804,-9223372036854775800\], increment 4"
380+ for i := int64 (math .MinInt64 + 8 ); i > math .MinInt64 + 2 ; i -= 4 { // ERROR "Induction variable: limits \[-9223372036854775804,-9223372036854775800\], increment 4$ "
381381 useString ("foo" )
382382 }
383383 for i := int64 (math .MinInt64 + 7 ); i > math .MinInt64 + 2 ; i -= 4 {
384384 useString ("foo" )
385385 }
386- for i := int64 (math .MinInt64 + 6 ); i > math .MinInt64 + 2 ; i -= 4 { // ERROR "Induction variable: limits \[-9223372036854775802,-9223372036854775802\], increment 4"
386+ for i := int64 (math .MinInt64 + 6 ); i > math .MinInt64 + 2 ; i -= 4 { // ERROR "Induction variable: limits \[-9223372036854775802,-9223372036854775802\], increment 4$ "
387387 useString ("foo" )
388388 }
389- for i := int64 (math .MinInt64 + 9 ); i >= math .MinInt64 + 2 ; i -= 4 { // ERROR "Induction variable: limits \[-9223372036854775803,-9223372036854775799\], increment 4"
389+ for i := int64 (math .MinInt64 + 9 ); i >= math .MinInt64 + 2 ; i -= 4 { // ERROR "Induction variable: limits \[-9223372036854775803,-9223372036854775799\], increment 4$ "
390390 useString ("foo" )
391391 }
392- for i := int64 (math .MinInt64 + 8 ); i >= math .MinInt64 + 2 ; i -= 4 { // ERROR "Induction variable: limits \[-9223372036854775804,-9223372036854775800\], increment 4"
392+ for i := int64 (math .MinInt64 + 8 ); i >= math .MinInt64 + 2 ; i -= 4 { // ERROR "Induction variable: limits \[-9223372036854775804,-9223372036854775800\], increment 4$ "
393393 useString ("foo" )
394394 }
395395 for i := int64 (math .MinInt64 + 7 ); i >= math .MinInt64 + 2 ; i -= 4 {
@@ -410,23 +410,23 @@ func bce1() {
410410 panic ("invalid test: modulos should differ" )
411411 }
412412
413- for i := b ; i < a ; i += z { // ERROR "Induction variable: limits \[-1547,9223372036854772720\], increment 1337"
413+ for i := b ; i < a ; i += z { // ERROR "Induction variable: limits \[-1547,9223372036854772720\], increment 1337$ "
414414 useString ("foobar" )
415415 }
416416}
417417
418418func nobce2 (a string ) {
419419 for i := int64 (0 ); i < int64 (len (a )); i ++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
420- useString (a [i :]) // ERROR "(\([0-9]+\) )? Proved IsSliceInBounds$"
420+ useString (a [i :]) // ERROR "Proved IsSliceInBounds$"
421421 }
422422 for i := int64 (0 ); i < int64 (len (a ))- 31337 ; i ++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
423- useString (a [i :]) // ERROR "(\([0-9]+\) )? Proved IsSliceInBounds$"
423+ useString (a [i :]) // ERROR "Proved IsSliceInBounds$"
424424 }
425- for i := int64 (0 ); i < int64 (len (a ))+ int64 (- 1 << 63 ); i ++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$" "Disproved Less64 "
425+ for i := int64 (0 ); i < int64 (len (a ))+ int64 (- 1 << 63 ); i ++ { // ERROR "Disproved Less64$" " Induction variable: limits \[0,\?\), increment 1$"
426426 useString (a [i :])
427427 }
428428 j := int64 (len (a )) - 123
429- for i := int64 (0 ); i < j + 123 + int64 (- 1 << 63 ); i ++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$" "Disproved Less64 "
429+ for i := int64 (0 ); i < j + 123 + int64 (- 1 << 63 ); i ++ { // ERROR "Disproved Less64$" " Induction variable: limits \[0,\?\), increment 1$"
430430 useString (a [i :])
431431 }
432432 for i := int64 (0 ); i < j + 122 + int64 (- 1 << 63 ); i ++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
@@ -455,16 +455,16 @@ func issue26116a(a []int) {
455455
456456func stride1 (x * [7 ]int ) int {
457457 s := 0
458- for i := 0 ; i <= 8 ; i += 3 { // ERROR "Induction variable: limits \[0,6\], increment 3"
459- s += x [i ] // ERROR "Proved IsInBounds"
458+ for i := 0 ; i <= 8 ; i += 3 { // ERROR "Induction variable: limits \[0,6\], increment 3$ "
459+ s += x [i ] // ERROR "Proved IsInBounds$ "
460460 }
461461 return s
462462}
463463
464464func stride2 (x * [7 ]int ) int {
465465 s := 0
466- for i := 0 ; i < 9 ; i += 3 { // ERROR "Induction variable: limits \[0,6\], increment 3"
467- s += x [i ] // ERROR "Proved IsInBounds"
466+ for i := 0 ; i < 9 ; i += 3 { // ERROR "Induction variable: limits \[0,6\], increment 3$ "
467+ s += x [i ] // ERROR "Proved IsInBounds$ "
468468 }
469469 return s
470470}
0 commit comments