blob: 8bcc9ae61406f36d11bede3e90df673dc6749ad3 [file] [log] [blame]
 // +build amd64 // errorcheck -0 -d=ssa/prove/debug=3 // Copyright 2016 The Go Authors. All rights reserved. // Use of this source code is governed by a BSD-style // license that can be found in the LICENSE file. package main import "math" func f0(a []int) int { a[0] = 1 a[0] = 1 // ERROR "Proved boolean IsInBounds\$" a[6] = 1 a[6] = 1 // ERROR "Proved boolean IsInBounds\$" a[5] = 1 // ERROR "Proved IsInBounds\$" a[5] = 1 // ERROR "Proved boolean IsInBounds\$" return 13 } func f1(a []int) int { if len(a) <= 5 { return 18 } a[0] = 1 // ERROR "Proved non-negative bounds IsInBounds\$" a[0] = 1 // ERROR "Proved boolean IsInBounds\$" a[6] = 1 a[6] = 1 // ERROR "Proved boolean IsInBounds\$" a[5] = 1 // ERROR "Proved IsInBounds\$" a[5] = 1 // ERROR "Proved boolean IsInBounds\$" return 26 } func f1b(a []int, i int, j uint) int { if i >= 0 && i < len(a) { return a[i] // ERROR "Proved non-negative bounds IsInBounds\$" } if i >= 10 && i < len(a) { return a[i] // ERROR "Proved non-negative bounds IsInBounds\$" } if i >= 10 && i < len(a) { return a[i] // ERROR "Proved non-negative bounds IsInBounds\$" } if i >= 10 && i < len(a) { // todo: handle this case return a[i-10] } if j < uint(len(a)) { return a[j] // ERROR "Proved IsInBounds\$" } return 0 } func f1c(a []int, i int64) int { c := uint64(math.MaxInt64 + 10) // overflows int d := int64(c) if i >= d && i < int64(len(a)) { // d overflows, should not be handled. return a[i] } return 0 } func f2(a []int) int { for i := range a { a[i+1] = i a[i+1] = i // ERROR "Proved boolean IsInBounds\$" } return 34 } func f3(a []uint) int { for i := uint(0); i < uint(len(a)); i++ { a[i] = i // ERROR "Proved IsInBounds\$" } return 41 } func f4a(a, b, c int) int { if a < b { if a == b { // ERROR "Disproved Eq64\$" return 47 } if a > b { // ERROR "Disproved Greater64\$" return 50 } if a < b { // ERROR "Proved boolean Less64\$" return 53 } if a == b { // ERROR "Disproved boolean Eq64\$" return 56 } if a > b { // ERROR "Disproved boolean Greater64\$" return 59 } return 61 } return 63 } func f4b(a, b, c int) int { if a <= b { if a >= b { if a == b { // ERROR "Proved Eq64\$" return 70 } return 75 } return 77 } return 79 } func f4c(a, b, c int) int { if a <= b { if a >= b { if a != b { // ERROR "Disproved Neq64\$" return 73 } return 75 } return 77 } return 79 } func f4d(a, b, c int) int { if a < b { if a < c { if a < b { // ERROR "Proved boolean Less64\$" if a < c { // ERROR "Proved boolean Less64\$" return 87 } return 89 } return 91 } return 93 } return 95 } func f4e(a, b, c int) int { if a < b { if b > a { // ERROR "Proved Greater64\$" return 101 } return 103 } return 105 } func f4f(a, b, c int) int { if a <= b { if b > a { if b == a { // ERROR "Disproved Eq64\$" return 112 } return 114 } if b >= a { // ERROR "Proved Geq64\$" if b == a { // ERROR "Proved Eq64\$" return 118 } return 120 } return 122 } return 124 } func f5(a, b uint) int { if a == b { if a <= b { // ERROR "Proved Leq64U\$" return 130 } return 132 } return 134 } // These comparisons are compile time constants. func f6a(a uint8) int { if a < a { // ERROR "Disproved Less8U\$" return 140 } return 151 } func f6b(a uint8) int { if a < a { // ERROR "Disproved Less8U\$" return 140 } return 151 } func f6x(a uint8) int { if a > a { // ERROR "Disproved Greater8U\$" return 143 } return 151 } func f6d(a uint8) int { if a <= a { // ERROR "Proved Leq8U\$" return 146 } return 151 } func f6e(a uint8) int { if a >= a { // ERROR "Proved Geq8U\$" return 149 } return 151 } func f7(a []int, b int) int { if b < len(a) { a[b] = 3 if b < len(a) { // ERROR "Proved boolean Less64\$" a[b] = 5 // ERROR "Proved boolean IsInBounds\$" } } return 161 } func f8(a, b uint) int { if a == b { return 166 } if a > b { return 169 } if a < b { // ERROR "Proved Less64U\$" return 172 } return 174 } func f9(a, b bool) int { if a { return 1 } if a || b { // ERROR "Disproved boolean Arg\$" return 2 } return 3 } func f10(a string) int { n := len(a) if a[:n>>1] == "aaa" { return 0 } return 1 } func f11a(a []int, i int) { useInt(a[i]) useInt(a[i]) // ERROR "Proved boolean IsInBounds\$" } func f11b(a []int, i int) { useSlice(a[i:]) useSlice(a[i:]) // ERROR "Proved boolean IsSliceInBounds\$" } func f11c(a []int, i int) { useSlice(a[:i]) useSlice(a[:i]) // ERROR "Proved boolean IsSliceInBounds\$" } func f11d(a []int, i int) { useInt(a[2*i+7]) useInt(a[2*i+7]) } func f12(a []int, b int) { useSlice(a[:b]) } func f13a(a, b, c int, x bool) int { if a > 12 { if x { if a < 12 { // ERROR "Disproved Less64\$" return 1 } } if x { if a <= 12 { // ERROR "Disproved Leq64\$" return 2 } } if x { if a == 12 { // ERROR "Disproved Eq64\$" return 3 } } if x { if a >= 12 { // ERROR "Proved Geq64\$" return 4 } } if x { if a > 12 { // ERROR "Proved boolean Greater64\$" return 5 } } return 6 } return 0 } func f13b(a int, x bool) int { if a == -9 { if x { if a < -9 { // ERROR "Disproved Less64\$" return 7 } } if x { if a <= -9 { // ERROR "Proved Leq64\$" return 8 } } if x { if a == -9 { // ERROR "Proved boolean Eq64\$" return 9 } } if x { if a >= -9 { // ERROR "Proved Geq64\$" return 10 } } if x { if a > -9 { // ERROR "Disproved Greater64\$" return 11 } } return 12 } return 0 } func f13c(a int, x bool) int { if a < 90 { if x { if a < 90 { // ERROR "Proved boolean Less64\$" return 13 } } if x { if a <= 90 { // ERROR "Proved Leq64\$" return 14 } } if x { if a == 90 { // ERROR "Disproved Eq64\$" return 15 } } if x { if a >= 90 { // ERROR "Disproved Geq64\$" return 16 } } if x { if a > 90 { // ERROR "Disproved Greater64\$" return 17 } } return 18 } return 0 } func f13d(a int) int { if a < 5 { if a < 9 { // ERROR "Proved Less64\$" return 1 } } return 0 } func f13e(a int) int { if a > 9 { if a > 5 { // ERROR "Proved Greater64\$" return 1 } } return 0 } func f13f(a int64) int64 { if a > math.MaxInt64 { // Unreachable, but prove doesn't know that. if a == 0 { return 1 } } return 0 } func f13g(a int) int { if a < 3 { return 5 } if a > 3 { return 6 } if a == 3 { // ERROR "Proved Eq64\$" return 7 } return 8 } func f13h(a int) int { if a < 3 { if a > 1 { if a == 2 { // ERROR "Proved Eq64\$" return 5 } } } return 0 } func f13i(a uint) int { if a == 0 { return 1 } if a > 0 { // ERROR "Proved Greater64U\$" return 2 } return 3 } //go:noinline func useInt(a int) { } //go:noinline func useSlice(a []int) { } func main() { }