aboutsummaryrefslogtreecommitdiff
path: root/test/prove.go
diff options
context:
space:
mode:
authorGiovanni Bajo <rasky@develer.com>2018-04-03 18:58:01 +0200
committerGiovanni Bajo <rasky@develer.com>2018-04-03 20:25:34 +0000
commitac43de3ae5027f61e6b028c806f6b83f80ee5d3b (patch)
treec3d475d6f15a36e856a2d7353bcbec0282be5e1b /test/prove.go
parentb846edfd5979d1cf53d55ea8fd6e4bbcfefb2e75 (diff)
downloadgo-ac43de3ae5027f61e6b028c806f6b83f80ee5d3b.tar.gz
go-ac43de3ae5027f61e6b028c806f6b83f80ee5d3b.zip
cmd/compile: in prove, complete support for OpIsInBounds/OpIsSliceInBounds
The logic in addBranchRestrictions didn't allow to correctly model OpIs(Slice)Bound for signed domain, and it was also partly implemented within addRestrictions. Thanks to the previous changes, it is now possible to handle the negative conditions correctly, so that we can learn both signed/LT + unsigned/LT on the positive side, and signed/GE + unsigned/GE on the negative side (but only if the index can be proved to be non-negative). This is able to prove ~50 more slice accesses in std+cmd. Change-Id: I9858080dc03b16f85993a55983dbc4b00f8491b0 Reviewed-on: https://go-review.googlesource.com/104037 Run-TryBot: Giovanni Bajo <rasky@develer.com> TryBot-Result: Gobot Gobot <gobot@golang.org> Reviewed-by: Austin Clements <austin@google.com>
Diffstat (limited to 'test/prove.go')
-rw-r--r--test/prove.go15
1 files changed, 15 insertions, 0 deletions
diff --git a/test/prove.go b/test/prove.go
index 97614939ac..197bdb0aef 100644
--- a/test/prove.go
+++ b/test/prove.go
@@ -475,6 +475,21 @@ func f17(b []int) {
}
}
+func f18(b []int, x int, y uint) {
+ _ = b[x]
+ _ = b[y]
+
+ if x > len(b) { // ERROR "Disproved Greater64$"
+ return
+ }
+ if y > uint(len(b)) { // ERROR "Disproved Greater64U$"
+ return
+ }
+ if int(y) > len(b) { // ERROR "Disproved Greater64$"
+ return
+ }
+}
+
func sm1(b []int, x int) {
// Test constant argument to slicemask.
useSlice(b[2:8]) // ERROR "Proved slicemask not needed$"