@@ -6,15 +6,15 @@ package main
6
6
func f0a (a []int ) int {
7
7
x := 0
8
8
for i := range a { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
9
- x += a [i ] // ERROR "Proved IsInBounds$"
9
+ x += a [i ] // ERROR "(\([0-9]+\) )? Proved IsInBounds$"
10
10
}
11
11
return x
12
12
}
13
13
14
14
func f0b (a []int ) int {
15
15
x := 0
16
16
for i := range a { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
17
- b := a [i :] // ERROR "Proved IsSliceInBounds$"
17
+ b := a [i :] // ERROR "(\([0-9]+\) )? Proved IsSliceInBounds$"
18
18
x += b [0 ]
19
19
}
20
20
return x
@@ -23,7 +23,7 @@ func f0b(a []int) int {
23
23
func f0c (a []int ) int {
24
24
x := 0
25
25
for i := range a { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
26
- b := a [:i + 1 ] // ERROR "Proved IsSliceInBounds$"
26
+ b := a [:i + 1 ] // ERROR "(\([0-9]+\) )? Proved IsSliceInBounds$"
27
27
x += b [0 ]
28
28
}
29
29
return x
@@ -40,15 +40,15 @@ func f1(a []int) int {
40
40
func f2 (a []int ) int {
41
41
x := 0
42
42
for i := 1 ; i < len (a ); i ++ { // ERROR "Induction variable: limits \[1,\?\), increment 1$"
43
- x += a [i ] // ERROR "Proved IsInBounds$"
43
+ x += a [i ] // ERROR "(\([0-9]+\) )? Proved IsInBounds$"
44
44
}
45
45
return x
46
46
}
47
47
48
48
func f4 (a [10 ]int ) int {
49
49
x := 0
50
50
for i := 0 ; i < len (a ); i += 2 { // ERROR "Induction variable: limits \[0,10\), increment 2$"
51
- x += a [i ] // ERROR "Proved IsInBounds$"
51
+ x += a [i ] // ERROR "(\([0-9]+\) )? Proved IsInBounds$"
52
52
}
53
53
return x
54
54
}
@@ -63,55 +63,55 @@ func f5(a [10]int) int {
63
63
64
64
func f6 (a []int ) {
65
65
for i := range a { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
66
- b := a [0 :i ] // ERROR "Proved IsSliceInBounds$"
66
+ b := a [0 :i ] // ERROR "(\([0-9]+\) )? Proved IsSliceInBounds$" "(\([0-9]+\) )?Proved Geq64 $"
67
67
f6 (b )
68
68
}
69
69
}
70
70
71
71
func g0a (a string ) int {
72
72
x := 0
73
73
for i := 0 ; i < len (a ); i ++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
74
- x += int (a [i ]) // ERROR "Proved IsInBounds$"
74
+ x += int (a [i ]) // ERROR "(\([0-9]+\) )? Proved IsInBounds$"
75
75
}
76
76
return x
77
77
}
78
78
79
79
func g0b (a string ) int {
80
80
x := 0
81
81
for i := 0 ; len (a ) > i ; i ++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
82
- x += int (a [i ]) // ERROR "Proved IsInBounds$"
82
+ x += int (a [i ]) // ERROR "(\([0-9]+\) )? Proved IsInBounds$"
83
83
}
84
84
return x
85
85
}
86
86
87
87
func g0c (a string ) int {
88
88
x := 0
89
89
for i := len (a ); i > 0 ; i -- { // ERROR "Induction variable: limits \(0,\?\], increment 1$"
90
- x += int (a [i - 1 ]) // ERROR "Proved IsInBounds$"
90
+ x += int (a [i - 1 ]) // ERROR "(\([0-9]+\) )? Proved IsInBounds$"
91
91
}
92
92
return x
93
93
}
94
94
95
95
func g0d (a string ) int {
96
96
x := 0
97
97
for i := len (a ); 0 < i ; i -- { // ERROR "Induction variable: limits \(0,\?\], increment 1$"
98
- x += int (a [i - 1 ]) // ERROR "Proved IsInBounds$"
98
+ x += int (a [i - 1 ]) // ERROR "(\([0-9]+\) )? Proved IsInBounds$"
99
99
}
100
100
return x
101
101
}
102
102
103
103
func g0e (a string ) int {
104
104
x := 0
105
105
for i := len (a ) - 1 ; i >= 0 ; i -- { // ERROR "Induction variable: limits \[0,\?\], increment 1$"
106
- x += int (a [i ]) // ERROR "Proved IsInBounds$"
106
+ x += int (a [i ]) // ERROR "(\([0-9]+\) )? Proved IsInBounds$"
107
107
}
108
108
return x
109
109
}
110
110
111
111
func g0f (a string ) int {
112
112
x := 0
113
113
for i := len (a ) - 1 ; 0 <= i ; i -- { // ERROR "Induction variable: limits \[0,\?\], increment 1$"
114
- x += int (a [i ]) // ERROR "Proved IsInBounds$"
114
+ x += int (a [i ]) // ERROR "(\([0-9]+\) )? Proved IsInBounds$"
115
115
}
116
116
return x
117
117
}
@@ -120,7 +120,7 @@ func g1() int {
120
120
a := "evenlength"
121
121
x := 0
122
122
for i := 0 ; i < len (a ); i += 2 { // ERROR "Induction variable: limits \[0,10\), increment 2$"
123
- x += int (a [i ]) // ERROR "Proved IsInBounds$"
123
+ x += int (a [i ]) // ERROR "(\([0-9]+\) )? Proved IsInBounds$"
124
124
}
125
125
return x
126
126
}
@@ -130,7 +130,7 @@ func g2() int {
130
130
x := 0
131
131
for i := 0 ; i < len (a ); i += 2 { // ERROR "Induction variable: limits \[0,10\), increment 2$"
132
132
j := i
133
- if a [i ] == 'e' { // ERROR "Proved IsInBounds$"
133
+ if a [i ] == 'e' { // ERROR "(\([0-9]+\) )? Proved IsInBounds$"
134
134
j = j + 1
135
135
}
136
136
x += int (a [j ])
@@ -141,27 +141,27 @@ func g2() int {
141
141
func g3a () {
142
142
a := "this string has length 25"
143
143
for i := 0 ; i < len (a ); i += 5 { // ERROR "Induction variable: limits \[0,25\), increment 5$"
144
- useString (a [i :]) // ERROR "Proved IsSliceInBounds$"
144
+ useString (a [i :]) // ERROR "(\([0-9]+\) )? Proved IsSliceInBounds$"
145
145
useString (a [:i + 3 ])
146
146
}
147
147
}
148
148
149
149
func g3b (a string ) {
150
150
for i := 0 ; i < len (a ); i ++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
151
- useString (a [i + 1 :]) // ERROR "Proved IsSliceInBounds$"
151
+ useString (a [i + 1 :]) // ERROR "(\([0-9]+\) )? Proved IsSliceInBounds$"
152
152
}
153
153
}
154
154
155
155
func g3c (a string ) {
156
156
for i := 0 ; i < len (a ); i ++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
157
- useString (a [:i + 1 ]) // ERROR "Proved IsSliceInBounds$"
157
+ useString (a [:i + 1 ]) // ERROR "(\([0-9]+\) )? Proved IsSliceInBounds$"
158
158
}
159
159
}
160
160
161
161
func h1 (a []byte ) {
162
162
c := a [:128 ]
163
163
for i := range c { // ERROR "Induction variable: limits \[0,128\), increment 1$"
164
- c [i ] = byte (i ) // ERROR "Proved IsInBounds$"
164
+ c [i ] = byte (i ) // ERROR "(\([0-9]+\) )? Proved IsInBounds$"
165
165
}
166
166
}
167
167
@@ -174,25 +174,25 @@ func h2(a []byte) {
174
174
func k0 (a [100 ]int ) [100 ]int {
175
175
for i := 10 ; i < 90 ; i ++ { // ERROR "Induction variable: limits \[10,90\), increment 1$"
176
176
a [i - 11 ] = i
177
- a [i - 10 ] = i // ERROR "Proved IsInBounds$"
178
- a [i - 5 ] = i // ERROR "Proved IsInBounds$"
179
- a [i ] = i // ERROR "Proved IsInBounds$"
180
- a [i + 5 ] = i // ERROR "Proved IsInBounds$"
181
- a [i + 10 ] = i // ERROR "Proved IsInBounds$"
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
182
a [i + 11 ] = i
183
183
}
184
184
return a
185
185
}
186
186
187
187
func k1 (a [100 ]int ) [100 ]int {
188
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 "Proved IsSliceInBounds$"
191
- useSlice (a [:i - 5 ]) // ERROR "Proved IsSliceInBounds$"
192
- useSlice (a [:i ]) // ERROR "Proved IsSliceInBounds$"
193
- useSlice (a [:i + 5 ]) // ERROR "Proved IsSliceInBounds$"
194
- useSlice (a [:i + 10 ]) // ERROR "Proved IsSliceInBounds$"
195
- useSlice (a [:i + 11 ]) // ERROR "Proved IsSliceInBounds$"
189
+ useSlice (a [:i - 11 ]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
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$" "(\([0-9]+\) )?Proved Geq64 $"
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
196
useSlice (a [:i + 12 ])
197
197
198
198
}
@@ -202,12 +202,12 @@ func k1(a [100]int) [100]int {
202
202
func k2 (a [100 ]int ) [100 ]int {
203
203
for i := 10 ; i < 90 ; i ++ { // ERROR "Induction variable: limits \[10,90\), increment 1$"
204
204
useSlice (a [i - 11 :])
205
- useSlice (a [i - 10 :]) // ERROR "Proved IsSliceInBounds$"
206
- useSlice (a [i - 5 :]) // ERROR "Proved IsSliceInBounds$"
207
- useSlice (a [i :]) // ERROR "Proved IsSliceInBounds$"
208
- useSlice (a [i + 5 :]) // ERROR "Proved IsSliceInBounds$"
209
- useSlice (a [i + 10 :]) // ERROR "Proved IsSliceInBounds$"
210
- useSlice (a [i + 11 :]) // ERROR "Proved IsSliceInBounds$"
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
211
useSlice (a [i + 12 :])
212
212
}
213
213
return a
@@ -216,7 +216,7 @@ func k2(a [100]int) [100]int {
216
216
func k3 (a [100 ]int ) [100 ]int {
217
217
for i := - 10 ; i < 90 ; i ++ { // ERROR "Induction variable: limits \[-10,90\), increment 1$"
218
218
a [i + 9 ] = i
219
- a [i + 10 ] = i // ERROR "Proved IsInBounds$"
219
+ a [i + 10 ] = i // ERROR "(\([0-9]+\) )? Proved IsInBounds$"
220
220
a [i + 11 ] = i
221
221
}
222
222
return a
@@ -225,7 +225,7 @@ func k3(a [100]int) [100]int {
225
225
func k3neg (a [100 ]int ) [100 ]int {
226
226
for i := 89 ; i > - 11 ; i -- { // ERROR "Induction variable: limits \(-11,89\], increment 1$"
227
227
a [i + 9 ] = i
228
- a [i + 10 ] = i // ERROR "Proved IsInBounds$"
228
+ a [i + 10 ] = i // ERROR "(\([0-9]+\) )? Proved IsInBounds$"
229
229
a [i + 11 ] = i
230
230
}
231
231
return a
@@ -234,7 +234,7 @@ func k3neg(a [100]int) [100]int {
234
234
func k3neg2 (a [100 ]int ) [100 ]int {
235
235
for i := 89 ; i >= - 10 ; i -- { // ERROR "Induction variable: limits \[-10,89\], increment 1$"
236
236
a [i + 9 ] = i
237
- a [i + 10 ] = i // ERROR "Proved IsInBounds$"
237
+ a [i + 10 ] = i // ERROR "(\([0-9]+\) )? Proved IsInBounds$"
238
238
a [i + 11 ] = i
239
239
}
240
240
return a
@@ -243,16 +243,16 @@ func k3neg2(a [100]int) [100]int {
243
243
func k4 (a [100 ]int ) [100 ]int {
244
244
min := (- 1 ) << 63
245
245
for i := min ; i < min + 50 ; i ++ { // ERROR "Induction variable: limits \[-9223372036854775808,-9223372036854775758\), increment 1$"
246
- a [i - min ] = i // ERROR "Proved IsInBounds$"
246
+ a [i - min ] = i // ERROR "(\([0-9]+\) )? Proved IsInBounds$"
247
247
}
248
248
return a
249
249
}
250
250
251
251
func k5 (a [100 ]int ) [100 ]int {
252
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 "Proved IsInBounds$"
255
- a [i - (max - 70 )] = i // ERROR "Proved IsInBounds$"
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
256
}
257
257
return a
258
258
}
@@ -275,17 +275,17 @@ func nobce1() {
275
275
276
276
func nobce2 (a string ) {
277
277
for i := int64 (0 ); i < int64 (len (a )); i ++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
278
- useString (a [i :]) // ERROR "Proved IsSliceInBounds$"
278
+ useString (a [i :]) // ERROR "(\([0-9]+\) )? Proved IsSliceInBounds$"
279
279
}
280
280
for i := int64 (0 ); i < int64 (len (a ))- 31337 ; i ++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
281
- useString (a [i :]) // ERROR "Proved IsSliceInBounds$"
281
+ useString (a [i :]) // ERROR "(\([0-9]+\) )? Proved IsSliceInBounds$"
282
282
}
283
283
for i := int64 (0 ); i < int64 (len (a ))+ int64 (- 1 << 63 ); i ++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
284
- useString (a [i :]) // ERROR "Proved IsSliceInBounds$"
284
+ useString (a [i :]) // ERROR "(\([0-9]+\) )? Proved IsSliceInBounds$"
285
285
}
286
286
j := int64 (len (a )) - 123
287
287
for i := int64 (0 ); i < j + 123 + int64 (- 1 << 63 ); i ++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
288
- useString (a [i :]) // ERROR "Proved IsSliceInBounds$"
288
+ useString (a [i :]) // ERROR "(\([0-9]+\) )? Proved IsSliceInBounds$"
289
289
}
290
290
for i := int64 (0 ); i < j + 122 + int64 (- 1 << 63 ); i ++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
291
291
// len(a)-123+122+MinInt overflows when len(a) == 0, so a bound check is needed here
0 commit comments