@@ -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