2 // errorcheck -0 -d=ssa/prove/debug=1
4 // Copyright 2016 The Go Authors. All rights reserved.
5 // Use of this source code is governed by a BSD-style
6 // license that can be found in the LICENSE file.
12 func f0(a []int) int {
14 a[0] = 1 // ERROR "Proved IsInBounds$"
16 a[6] = 1 // ERROR "Proved IsInBounds$"
17 a[5] = 1 // ERROR "Proved IsInBounds$"
18 a[5] = 1 // ERROR "Proved IsInBounds$"
22 func f1(a []int) int {
26 a[0] = 1 // ERROR "Proved IsInBounds$"
27 a[0] = 1 // ERROR "Proved IsInBounds$"
29 a[6] = 1 // ERROR "Proved IsInBounds$"
30 a[5] = 1 // ERROR "Proved IsInBounds$"
31 a[5] = 1 // ERROR "Proved IsInBounds$"
35 func f1b(a []int, i int, j uint) int {
36 if i >= 0 && i < len(a) {
37 return a[i] // ERROR "Proved IsInBounds$"
39 if i >= 10 && i < len(a) {
40 return a[i] // ERROR "Proved IsInBounds$"
42 if i >= 10 && i < len(a) {
43 return a[i] // ERROR "Proved IsInBounds$"
45 if i >= 10 && i < len(a) { // todo: handle this case
49 return a[j] // ERROR "Proved IsInBounds$"
54 func f1c(a []int, i int64) int {
55 c := uint64(math.MaxInt64 + 10) // overflows int
57 if i >= d && i < int64(len(a)) {
58 // d overflows, should not be handled.
64 func f2(a []int) int {
67 a[i+1] = i // ERROR "Proved IsInBounds$"
72 func f3(a []uint) int {
73 for i := uint(0); i < uint(len(a)); i++ {
74 a[i] = i // ERROR "Proved IsInBounds$"
79 func f4a(a, b, c int) int {
81 if a == b { // ERROR "Disproved Eq64$"
84 if a > b { // ERROR "Disproved Greater64$"
87 if a < b { // ERROR "Proved Less64$"
90 // We can't get to this point and prove knows that, so
91 // there's no message for the next (obvious) branch.
100 func f4b(a, b, c int) int {
103 if a == b { // ERROR "Proved Eq64$"
113 func f4c(a, b, c int) int {
116 if a != b { // ERROR "Disproved Neq64$"
126 func f4d(a, b, c int) int {
129 if a < b { // ERROR "Proved Less64$"
130 if a < c { // ERROR "Proved Less64$"
142 func f4e(a, b, c int) int {
144 if b > a { // ERROR "Proved Greater64$"
152 func f4f(a, b, c int) int {
155 if b == a { // ERROR "Disproved Eq64$"
160 if b >= a { // ERROR "Proved Geq64$"
161 if b == a { // ERROR "Proved Eq64$"
171 func f5(a, b uint) int {
173 if a <= b { // ERROR "Proved Leq64U$"
181 // These comparisons are compile time constants.
182 func f6a(a uint8) int {
183 if a < a { // ERROR "Disproved Less8U$"
189 func f6b(a uint8) int {
190 if a < a { // ERROR "Disproved Less8U$"
196 func f6x(a uint8) int {
197 if a > a { // ERROR "Disproved Greater8U$"
203 func f6d(a uint8) int {
204 if a <= a { // ERROR "Proved Leq8U$"
210 func f6e(a uint8) int {
211 if a >= a { // ERROR "Proved Geq8U$"
217 func f7(a []int, b int) int {
220 if b < len(a) { // ERROR "Proved Less64$"
221 a[b] = 5 // ERROR "Proved IsInBounds$"
227 func f8(a, b uint) int {
234 if a < b { // ERROR "Proved Less64U$"
240 func f9(a, b bool) int {
244 if a || b { // ERROR "Disproved Arg$"
250 func f10(a string) int {
252 // We optimize comparisons with small constant strings (see cmd/compile/internal/gc/walk.go),
253 // so this string literal must be long.
254 if a[:n>>1] == "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa" {
260 func f11a(a []int, i int) {
262 useInt(a[i]) // ERROR "Proved IsInBounds$"
265 func f11b(a []int, i int) {
267 useSlice(a[i:]) // ERROR "Proved IsSliceInBounds$"
270 func f11c(a []int, i int) {
272 useSlice(a[:i]) // ERROR "Proved IsSliceInBounds$"
275 func f11d(a []int, i int) {
277 useInt(a[2*i+7]) // ERROR "Proved IsInBounds$"
280 func f12(a []int, b int) {
284 func f13a(a, b, c int, x bool) int {
287 if a < 12 { // ERROR "Disproved Less64$"
292 if a <= 12 { // ERROR "Disproved Leq64$"
297 if a == 12 { // ERROR "Disproved Eq64$"
302 if a >= 12 { // ERROR "Proved Geq64$"
307 if a > 12 { // ERROR "Proved Greater64$"
316 func f13b(a int, x bool) int {
319 if a < -9 { // ERROR "Disproved Less64$"
324 if a <= -9 { // ERROR "Proved Leq64$"
329 if a == -9 { // ERROR "Proved Eq64$"
334 if a >= -9 { // ERROR "Proved Geq64$"
339 if a > -9 { // ERROR "Disproved Greater64$"
348 func f13c(a int, x bool) int {
351 if a < 90 { // ERROR "Proved Less64$"
356 if a <= 90 { // ERROR "Proved Leq64$"
361 if a == 90 { // ERROR "Disproved Eq64$"
366 if a >= 90 { // ERROR "Disproved Geq64$"
371 if a > 90 { // ERROR "Disproved Greater64$"
380 func f13d(a int) int {
382 if a < 9 { // ERROR "Proved Less64$"
389 func f13e(a int) int {
391 if a > 5 { // ERROR "Proved Greater64$"
398 func f13f(a int64) int64 {
399 if a > math.MaxInt64 {
400 // Unreachable, but prove doesn't know that.
408 func f13g(a int) int {
415 if a == 3 { // ERROR "Proved Eq64$"
421 func f13h(a int) int {
424 if a == 2 { // ERROR "Proved Eq64$"
432 func f13i(a uint) int {
436 if a > 0 { // ERROR "Proved Greater64U$"
442 func f14(p, q *int, a []int) {
443 // This crazy ordering usually gives i1 the lowest value ID,
444 // j the middle value ID, and i2 the highest value ID.
445 // That used to confuse CSE because it ordered the args
446 // of the two + ops below differently.
447 // That in turn foiled bounds check elimination.
452 useInt(a[i2+j]) // ERROR "Proved IsInBounds$"
455 func f15(s []int, x int) {
457 useSlice(s[:x]) // ERROR "Proved IsSliceInBounds$"
460 func f16(s []int) []int {
462 return s[:10] // ERROR "Proved IsSliceInBounds$"
468 for i := 0; i < len(b); i++ {
469 useSlice(b[i:]) // Learns i <= len
470 // This tests for i <= cap, which we can only prove
471 // using the derived relation between len and cap.
472 // This depends on finding the contradiction, since we
473 // don't query this condition directly.
474 useSlice(b[:i]) // ERROR "Proved IsSliceInBounds$"
478 func sm1(b []int, x int) {
479 // Test constant argument to slicemask.
480 useSlice(b[2:8]) // ERROR "Proved slicemask not needed$"
481 // Test non-constant argument with known limits.
483 useSlice(b[2:]) // ERROR "Proved slicemask not needed$"
487 func lim1(x, y, z int) {
488 // Test relations between signed and unsigned limits.
490 if uint(x) > 5 { // ERROR "Proved Greater64U$"
495 if uint(y) > 4 { // ERROR "Disproved Greater64U$"
498 if uint(y) < 5 { // ERROR "Proved Less64U$"
503 if uint(z) > 4 { // Not provable without disjunctions.
509 // fence1–4 correspond to the four fence-post implications.
511 func fence1(b []int, x, y int) {
512 // Test proofs that rely on fence-post implications.
514 if x < y { // ERROR "Disproved Less64$"
519 // This eliminates the growslice path.
520 b = append(b, 1) // ERROR "Disproved Greater64$"
524 func fence2(x, y int) {
526 if x > y { // ERROR "Disproved Greater64$"
532 func fence3(b []int, x, y int64) {
534 if x <= y { // Can't prove because x may have wrapped.
539 if x != math.MinInt64 && x-1 >= y {
540 if x <= y { // ERROR "Disproved Leq64$"
545 if n := len(b); n > 0 {
546 b[n-1] = 0 // ERROR "Proved IsInBounds$"
550 func fence4(x, y int64) {
556 if y != math.MaxInt64 && x >= y+1 {
557 if x <= y { // ERROR "Disproved Leq64$"
568 func useSlice(a []int) {