ft := newFactsTable(f)
ft.checkpoint()
+ var lensVars map[*Block][]*Value
+
// Find length and capacity ops.
for _, b := range f.Blocks {
for _, v := range b.Values {
}
ft.lens[v.Args[0].ID] = v
ft.update(b, v, ft.zero, signed, gt|eq)
+ if v.Args[0].Op == OpSliceMake {
+ if lensVars == nil {
+ lensVars = make(map[*Block][]*Value)
+ }
+ lensVars[b] = append(lensVars[b], v)
+ }
case OpSliceCap:
if ft.caps == nil {
ft.caps = map[ID]*Value{}
}
ft.caps[v.Args[0].ID] = v
ft.update(b, v, ft.zero, signed, gt|eq)
+ if v.Args[0].Op == OpSliceMake {
+ if lensVars == nil {
+ lensVars = make(map[*Block][]*Value)
+ }
+ lensVars[b] = append(lensVars[b], v)
+ }
}
}
}
switch node.state {
case descend:
ft.checkpoint()
+
+ // Entering the block, add the block-depending facts that we collected
+ // at the beginning: induction variables and lens/caps of slices.
if iv, ok := indVars[node.block]; ok {
addIndVarRestrictions(ft, parent, iv)
}
+ if lens, ok := lensVars[node.block]; ok {
+ for _, v := range lens {
+ switch v.Op {
+ case OpSliceLen:
+ ft.update(node.block, v, v.Args[0].Args[1], signed, eq)
+ case OpSliceCap:
+ ft.update(node.block, v, v.Args[0].Args[2], signed, eq)
+ }
+ }
+ }
if branch != unknown {
addBranchRestrictions(ft, parent, branch)
}
}
+func atexit(foobar []func()) {
+ for i := len(foobar) - 1; i >= 0; i-- { // ERROR "Induction variable: limits \[0,\?\], increment 1"
+ f := foobar[i]
+ foobar = foobar[:i] // ERROR "IsSliceInBounds"
+ f()
+ }
+}
+
+func make1(n int) []int {
+ s := make([]int, n)
+ for i := 0; i < n; i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1"
+ s[i] = 1 // ERROR "Proved IsInBounds$"
+ }
+ return s
+}
+
+func make2(n int) []int {
+ s := make([]int, n)
+ for i := range s { // ERROR "Induction variable: limits \[0,\?\), increment 1"
+ s[i] = 1 // ERROR "Proved IsInBounds$"
+ }
+ return s
+}
+
// The range tests below test the index variable of range loops.
// range1 compiles to the "efficiently indexable" form of a range loop.
return 0
}
if j8 >= 0 && j8 < 22 {
- return x[j8] // ERROR "Proved IsInBounds$"
+ return x[j8] // ERROR "Proved IsInBounds$"
}
if j16 >= 0 && j16 < 22 {
- return x[j16] // ERROR "Proved IsInBounds$"
+ return x[j16] // ERROR "Proved IsInBounds$"
}
if j32 >= 0 && j32 < 22 {
- return x[j32] // ERROR "Proved IsInBounds$"
+ return x[j32] // ERROR "Proved IsInBounds$"
}
return 0
}
return 0
}
if j8 >= 0 && j8 < 22 {
- return x[j8] // ERROR "Proved IsInBounds$"
+ return x[j8] // ERROR "Proved IsInBounds$"
}
if j16 >= 0 && j16 < 22 {
- return x[j16] // ERROR "Proved IsInBounds$"
+ return x[j16] // ERROR "Proved IsInBounds$"
}
if j32 >= 0 && j32 < 22 {
- return x[j32] // ERROR "Proved IsInBounds$"
+ return x[j32] // ERROR "Proved IsInBounds$"
}
return 0
}
if x[j] != 0 {
return 1
}
- if j > 0 && x[j-1] != 0 { // ERROR "Proved IsInBounds$"
+ if j > 0 && x[j-1] != 0 { // ERROR "Proved IsInBounds$"
return 1
}
return 0
if x[j] != 0 {
return 1
}
- if j > 0 && x[j-1] != 0 { // ERROR "Proved IsInBounds$"
+ if j > 0 && x[j-1] != 0 { // ERROR "Proved IsInBounds$"
return 1
}
return 0