diff options
| author | Giovanni Bajo <rasky@develer.com> | 2018-04-02 01:57:49 +0200 |
|---|---|---|
| committer | Giovanni Bajo <rasky@develer.com> | 2018-04-29 09:37:35 +0000 |
| commit | 7ec25d0acfed3f40fe634be518f0857704e5b642 (patch) | |
| tree | 91b61b67232ce3d3bee6c94b24fbda21a0cdc3e7 /test/prove.go | |
| parent | 29162ec9a7d4ee08a558729236cd9bf50febee09 (diff) | |
| download | go-git-7ec25d0acfed3f40fe634be518f0857704e5b642.tar.gz | |
cmd/compile: implement loop BCE in prove
Reuse findIndVar to discover induction variables, and then
register the facts we know about them into the facts table
when entering the loop block.
Moreover, handle "x+delta > w" while updating the facts table,
to be able to prove accesses to slices with constant offsets
such as slice[i-10].
Change-Id: I2a63d050ed58258136d54712ac7015b25c893d71
Reviewed-on: https://go-review.googlesource.com/104038
Run-TryBot: Giovanni Bajo <rasky@develer.com>
Reviewed-by: David Chase <drchase@google.com>
Diffstat (limited to 'test/prove.go')
| -rw-r--r-- | test/prove.go | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/test/prove.go b/test/prove.go index f7b3ef0847..a4eedbb717 100644 --- a/test/prove.go +++ b/test/prove.go @@ -62,7 +62,7 @@ func f1c(a []int, i int64) int { } func f2(a []int) int { - for i := range a { + for i := range a { // ERROR "Induction variable with minimum 0 and increment 1" a[i+1] = i a[i+1] = i // ERROR "Proved IsInBounds$" } @@ -464,8 +464,7 @@ func f16(s []int) []int { } func f17(b []int) { - for i := 0; i < len(b); i++ { - useSlice(b[i:]) // Learns i <= len + for i := 0; i < len(b); i++ { // ERROR "Induction variable with minimum 0 and increment 1" // This tests for i <= cap, which we can only prove // using the derived relation between len and cap. // This depends on finding the contradiction, since we |