1 files changed, 207 insertions, 0 deletions
diff --git a/test/prove.go b/test/prove.go
new file mode 100644
index 0000000000..0f5b8ce87f
--- /dev/null
+++ b/test/prove.go
@@ -0,0 +1,207 @@
+// +build amd64
+// errorcheck -0 -d=ssa/prove/debug=3
+
+package main
+
+func f0(a []int) int {
+	a[0] = 1
+	a[0] = 1 // ERROR "Proved IsInBounds$"
+	a[6] = 1
+	a[6] = 1 // ERROR "Proved IsInBounds$"
+	a[5] = 1
+	a[5] = 1 // ERROR "Proved IsInBounds$"
+	return 13
+}
+
+func f1(a []int) int {
+	if len(a) <= 5 {
+		return 18
+	}
+	a[0] = 1
+	a[0] = 1 // ERROR "Proved IsInBounds$"
+	a[6] = 1
+	a[6] = 1 // ERROR "Proved IsInBounds$"
+	a[5] = 1 // ERROR "Proved constant IsInBounds$"
+	a[5] = 1 // ERROR "Proved IsInBounds$"
+	return 26
+}
+
+func f2(a []int) int {
+	for i := range a {
+		a[i] = i
+		a[i] = i // ERROR "Proved 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 Less64$"
+			return 53
+		}
+		if a == b { // ERROR "Disproved Eq64$"
+			return 56
+		}
+		if a > b {
+			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 Less64$"
+				if a < c { // ERROR "Proved 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 Less64$"
+			a[b] = 5 // ERROR "Proved 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 main() {
+}