This commit is contained in:
Yi Yang 2023-05-16 15:15:54 +08:00
parent df71e02284
commit a9d80f68e6
2 changed files with 5 additions and 13 deletions

View File

@ -136,8 +136,7 @@ func g4(a [100]int) {
useInt(a[i+25])
useInt(a[i+50])
// The following are out of bounds.
useInt(a[i-11]) // ERROR "Found IsInBounds$"
// The following access is out of bounds.
useInt(a[i+51]) // ERROR "Found IsInBounds$"
}
}

View File

@ -58,7 +58,7 @@ func f4(a [10]int) int {
func f5(a [10]int) int {
x := 0
for i := -10; i < len(a); i += 2 { // ERROR "Induction variable: limits \[-10,8\], increment 2$"
x += a[i]
x += a[i+10]
}
return x
}
@ -66,7 +66,7 @@ func f5(a [10]int) int {
func f5_int32(a [10]int) int {
x := 0
for i := int32(-10); i < int32(len(a)); i += 2 { // ERROR "Induction variable: limits \[-10,8\], increment 2$"
x += a[i]
x += a[i+10]
}
return x
}
@ -74,7 +74,7 @@ func f5_int32(a [10]int) int {
func f5_int16(a [10]int) int {
x := 0
for i := int16(-10); i < int16(len(a)); i += 2 { // ERROR "Induction variable: limits \[-10,8\], increment 2$"
x += a[i]
x += a[i+10]
}
return x
}
@ -82,7 +82,7 @@ func f5_int16(a [10]int) int {
func f5_int8(a [10]int) int {
x := 0
for i := int8(-10); i < int8(len(a)); i += 2 { // ERROR "Induction variable: limits \[-10,8\], increment 2$"
x += a[i]
x += a[i+10]
}
return x
}
@ -201,7 +201,6 @@ func h2(a []byte) {
func k0(a [100]int) [100]int {
for i := 10; i < 90; i++ { // ERROR "Induction variable: limits \[10,90\), increment 1$"
a[i-11] = i
a[i-10] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
a[i-5] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
a[i] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
@ -214,7 +213,6 @@ func k0(a [100]int) [100]int {
func k1(a [100]int) [100]int {
for i := 10; i < 90; i++ { // ERROR "Induction variable: limits \[10,90\), increment 1$"
useSlice(a[:i-11])
useSlice(a[:i-10]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
useSlice(a[:i-5]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
useSlice(a[:i]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
@ -229,7 +227,6 @@ func k1(a [100]int) [100]int {
func k2(a [100]int) [100]int {
for i := 10; i < 90; i++ { // ERROR "Induction variable: limits \[10,90\), increment 1$"
useSlice(a[i-11:])
useSlice(a[i-10:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
useSlice(a[i-5:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
useSlice(a[i:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
@ -243,7 +240,6 @@ func k2(a [100]int) [100]int {
func k3(a [100]int) [100]int {
for i := -10; i < 90; i++ { // ERROR "Induction variable: limits \[-10,90\), increment 1$"
a[i+9] = i
a[i+10] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
a[i+11] = i
}
@ -254,7 +250,6 @@ func k3neg(a [100]int) [100]int {
for i := 89; i > -11; i-- { // ERROR "Induction variable: limits \(-11,89\], increment 1$"
a[i+9] = i
a[i+10] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
a[i+11] = i
}
return a
}
@ -263,7 +258,6 @@ func k3neg2(a [100]int) [100]int {
for i := 89; i >= -10; i-- { // ERROR "Induction variable: limits \[-10,89\], increment 1$"
a[i+9] = i
a[i+10] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
a[i+11] = i
}
return a
}
@ -411,7 +405,6 @@ func nobce3(a [100]int64) [100]int64 {
min := int64((-1) << 63)
max := int64((1 << 63) - 1)
for i := min; i < max; i++ { // ERROR "Induction variable: limits \[-9223372036854775808,9223372036854775807\), increment 1$"
a[i] = i
}
return a
}