Source file test/prove.go

     1  // errorcheck -0 -d=ssa/prove/debug=1
     2  
     3  //go:build amd64 || arm64
     4  
     5  // Copyright 2016 The Go Authors. All rights reserved.
     6  // Use of this source code is governed by a BSD-style
     7  // license that can be found in the LICENSE file.
     8  
     9  package main
    10  
    11  import (
    12  	"math"
    13  	"math/bits"
    14  )
    15  
    16  func f0(a []int) int {
    17  	a[0] = 1
    18  	a[0] = 1 // ERROR "Proved IsInBounds$"
    19  	a[6] = 1
    20  	a[6] = 1 // ERROR "Proved IsInBounds$"
    21  	a[5] = 1 // ERROR "Proved IsInBounds$"
    22  	a[5] = 1 // ERROR "Proved IsInBounds$"
    23  	return 13
    24  }
    25  
    26  func f1(a []int) int {
    27  	if len(a) <= 5 {
    28  		return 18
    29  	}
    30  	a[0] = 1 // ERROR "Proved IsInBounds$"
    31  	a[0] = 1 // ERROR "Proved IsInBounds$"
    32  	a[6] = 1
    33  	a[6] = 1 // ERROR "Proved IsInBounds$"
    34  	a[5] = 1 // ERROR "Proved IsInBounds$"
    35  	a[5] = 1 // ERROR "Proved IsInBounds$"
    36  	return 26
    37  }
    38  
    39  func f1b(a []int, i int, j uint) int {
    40  	if i >= 0 && i < len(a) {
    41  		return a[i] // ERROR "Proved IsInBounds$"
    42  	}
    43  	if i >= 10 && i < len(a) {
    44  		return a[i] // ERROR "Proved IsInBounds$"
    45  	}
    46  	if i >= 10 && i < len(a) {
    47  		return a[i] // ERROR "Proved IsInBounds$"
    48  	}
    49  	if i >= 10 && i < len(a) {
    50  		return a[i-10] // ERROR "Proved IsInBounds$"
    51  	}
    52  	if j < uint(len(a)) {
    53  		return a[j] // ERROR "Proved IsInBounds$"
    54  	}
    55  	return 0
    56  }
    57  
    58  func f1c(a []int, i int64) int {
    59  	c := uint64(math.MaxInt64 + 10) // overflows int
    60  	d := int64(c)
    61  	if i >= d && i < int64(len(a)) {
    62  		// d overflows, should not be handled.
    63  		return a[i]
    64  	}
    65  	return 0
    66  }
    67  
    68  func f2(a []int) int {
    69  	for i := range a { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
    70  		a[i+1] = i
    71  		a[i+1] = i // ERROR "Proved IsInBounds$"
    72  	}
    73  	return 34
    74  }
    75  
    76  func f3(a []uint) int {
    77  	for i := uint(0); i < uint(len(a)); i++ {
    78  		a[i] = i // ERROR "Proved IsInBounds$"
    79  	}
    80  	return 41
    81  }
    82  
    83  func f4a(a, b, c int) int {
    84  	if a < b {
    85  		if a == b { // ERROR "Disproved Eq64$"
    86  			return 47
    87  		}
    88  		if a > b { // ERROR "Disproved Less64$"
    89  			return 50
    90  		}
    91  		if a < b { // ERROR "Proved Less64$"
    92  			return 53
    93  		}
    94  		// We can't get to this point and prove knows that, so
    95  		// there's no message for the next (obvious) branch.
    96  		if a != a {
    97  			return 56
    98  		}
    99  		return 61
   100  	}
   101  	return 63
   102  }
   103  
   104  func f4b(a, b, c int) int {
   105  	if a <= b {
   106  		if a >= b {
   107  			if a == b { // ERROR "Proved Eq64$"
   108  				return 70
   109  			}
   110  			return 75
   111  		}
   112  		return 77
   113  	}
   114  	return 79
   115  }
   116  
   117  func f4c(a, b, c int) int {
   118  	if a <= b {
   119  		if a >= b {
   120  			if a != b { // ERROR "Disproved Neq64$"
   121  				return 73
   122  			}
   123  			return 75
   124  		}
   125  		return 77
   126  	}
   127  	return 79
   128  }
   129  
   130  func f4d(a, b, c int) int {
   131  	if a < b {
   132  		if a < c {
   133  			if a < b { // ERROR "Proved Less64$"
   134  				if a < c { // ERROR "Proved Less64$"
   135  					return 87
   136  				}
   137  				return 89
   138  			}
   139  			return 91
   140  		}
   141  		return 93
   142  	}
   143  	return 95
   144  }
   145  
   146  func f4e(a, b, c int) int {
   147  	if a < b {
   148  		if b > a { // ERROR "Proved Less64$"
   149  			return 101
   150  		}
   151  		return 103
   152  	}
   153  	return 105
   154  }
   155  
   156  func f4f(a, b, c int) int {
   157  	if a <= b {
   158  		if b > a {
   159  			if b == a { // ERROR "Disproved Eq64$"
   160  				return 112
   161  			}
   162  			return 114
   163  		}
   164  		if b >= a { // ERROR "Proved Leq64$"
   165  			if b == a { // ERROR "Proved Eq64$"
   166  				return 118
   167  			}
   168  			return 120
   169  		}
   170  		return 122
   171  	}
   172  	return 124
   173  }
   174  
   175  func f5(a, b uint) int {
   176  	if a == b {
   177  		if a <= b { // ERROR "Proved Leq64U$"
   178  			return 130
   179  		}
   180  		return 132
   181  	}
   182  	return 134
   183  }
   184  
   185  // These comparisons are compile time constants.
   186  func f6a(a uint8) int {
   187  	if a < a { // ERROR "Disproved Less8U$"
   188  		return 140
   189  	}
   190  	return 151
   191  }
   192  
   193  func f6b(a uint8) int {
   194  	if a < a { // ERROR "Disproved Less8U$"
   195  		return 140
   196  	}
   197  	return 151
   198  }
   199  
   200  func f6x(a uint8) int {
   201  	if a > a { // ERROR "Disproved Less8U$"
   202  		return 143
   203  	}
   204  	return 151
   205  }
   206  
   207  func f6d(a uint8) int {
   208  	if a <= a { // ERROR "Proved Leq8U$"
   209  		return 146
   210  	}
   211  	return 151
   212  }
   213  
   214  func f6e(a uint8) int {
   215  	if a >= a { // ERROR "Proved Leq8U$"
   216  		return 149
   217  	}
   218  	return 151
   219  }
   220  
   221  func f7(a []int, b int) int {
   222  	if b < len(a) {
   223  		a[b] = 3
   224  		if b < len(a) { // ERROR "Proved Less64$"
   225  			a[b] = 5 // ERROR "Proved IsInBounds$"
   226  		}
   227  	}
   228  	return 161
   229  }
   230  
   231  func f8(a, b uint) int {
   232  	if a == b {
   233  		return 166
   234  	}
   235  	if a > b {
   236  		return 169
   237  	}
   238  	if a < b { // ERROR "Proved Less64U$"
   239  		return 172
   240  	}
   241  	return 174
   242  }
   243  
   244  func f9(a, b bool) int {
   245  	if a {
   246  		return 1
   247  	}
   248  	if a || b { // ERROR "Disproved Arg$"
   249  		return 2
   250  	}
   251  	return 3
   252  }
   253  
   254  func f10(a string) int {
   255  	n := len(a)
   256  	b := a[:n>>1] // ERROR "(Proved IsSliceInBounds|Proved Rsh64x64 is unsigned)$"
   257  	// We optimize comparisons with small constant strings (see cmd/compile/internal/gc/walk.go),
   258  	// so this string literal must be long.
   259  	if b == "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa" {
   260  		return 0
   261  	}
   262  	return 1
   263  }
   264  
   265  func f11a(a []int, i int) {
   266  	useInt(a[i])
   267  	useInt(a[i]) // ERROR "Proved IsInBounds$"
   268  }
   269  
   270  func f11b(a []int, i int) {
   271  	useSlice(a[i:])
   272  	useSlice(a[i:]) // ERROR "Proved IsSliceInBounds$"
   273  }
   274  
   275  func f11c(a []int, i int) {
   276  	useSlice(a[:i])
   277  	useSlice(a[:i]) // ERROR "Proved IsSliceInBounds$"
   278  }
   279  
   280  func f11d(a []int, i int) {
   281  	useInt(a[2*i+7])
   282  	useInt(a[2*i+7]) // ERROR "Proved IsInBounds$"
   283  }
   284  
   285  func f12(a []int, b int) {
   286  	useSlice(a[:b])
   287  }
   288  
   289  func f13a(a, b, c int, x bool) int {
   290  	if a > 12 {
   291  		if x {
   292  			if a < 12 { // ERROR "Disproved Less64$"
   293  				return 1
   294  			}
   295  		}
   296  		if x {
   297  			if a <= 12 { // ERROR "Disproved Leq64$"
   298  				return 2
   299  			}
   300  		}
   301  		if x {
   302  			if a == 12 { // ERROR "Disproved Eq64$"
   303  				return 3
   304  			}
   305  		}
   306  		if x {
   307  			if a >= 12 { // ERROR "Proved Leq64$"
   308  				return 4
   309  			}
   310  		}
   311  		if x {
   312  			if a > 12 { // ERROR "Proved Less64$"
   313  				return 5
   314  			}
   315  		}
   316  		return 6
   317  	}
   318  	return 0
   319  }
   320  
   321  func f13b(a int, x bool) int {
   322  	if a == -9 {
   323  		if x {
   324  			if a < -9 { // ERROR "Disproved Less64$"
   325  				return 7
   326  			}
   327  		}
   328  		if x {
   329  			if a <= -9 { // ERROR "Proved Leq64$"
   330  				return 8
   331  			}
   332  		}
   333  		if x {
   334  			if a == -9 { // ERROR "Proved Eq64$"
   335  				return 9
   336  			}
   337  		}
   338  		if x {
   339  			if a >= -9 { // ERROR "Proved Leq64$"
   340  				return 10
   341  			}
   342  		}
   343  		if x {
   344  			if a > -9 { // ERROR "Disproved Less64$"
   345  				return 11
   346  			}
   347  		}
   348  		return 12
   349  	}
   350  	return 0
   351  }
   352  
   353  func f13c(a int, x bool) int {
   354  	if a < 90 {
   355  		if x {
   356  			if a < 90 { // ERROR "Proved Less64$"
   357  				return 13
   358  			}
   359  		}
   360  		if x {
   361  			if a <= 90 { // ERROR "Proved Leq64$"
   362  				return 14
   363  			}
   364  		}
   365  		if x {
   366  			if a == 90 { // ERROR "Disproved Eq64$"
   367  				return 15
   368  			}
   369  		}
   370  		if x {
   371  			if a >= 90 { // ERROR "Disproved Leq64$"
   372  				return 16
   373  			}
   374  		}
   375  		if x {
   376  			if a > 90 { // ERROR "Disproved Less64$"
   377  				return 17
   378  			}
   379  		}
   380  		return 18
   381  	}
   382  	return 0
   383  }
   384  
   385  func f13d(a int) int {
   386  	if a < 5 {
   387  		if a < 9 { // ERROR "Proved Less64$"
   388  			return 1
   389  		}
   390  	}
   391  	return 0
   392  }
   393  
   394  func f13e(a int) int {
   395  	if a > 9 {
   396  		if a > 5 { // ERROR "Proved Less64$"
   397  			return 1
   398  		}
   399  	}
   400  	return 0
   401  }
   402  
   403  func f13f(a, b int64) int64 {
   404  	if b != math.MaxInt64 {
   405  		return 42
   406  	}
   407  	if a > b { // ERROR "Disproved Less64$"
   408  		if a == 0 {
   409  			return 1
   410  		}
   411  	}
   412  	return 0
   413  }
   414  
   415  func f13g(a int) int {
   416  	if a < 3 {
   417  		return 5
   418  	}
   419  	if a > 3 {
   420  		return 6
   421  	}
   422  	if a == 3 { // ERROR "Proved Eq64$"
   423  		return 7
   424  	}
   425  	return 8
   426  }
   427  
   428  func f13h(a int) int {
   429  	if a < 3 {
   430  		if a > 1 {
   431  			if a == 2 { // ERROR "Proved Eq64$"
   432  				return 5
   433  			}
   434  		}
   435  	}
   436  	return 0
   437  }
   438  
   439  func f13i(a uint) int {
   440  	if a == 0 {
   441  		return 1
   442  	}
   443  	if a > 0 { // ERROR "Proved Less64U$"
   444  		return 2
   445  	}
   446  	return 3
   447  }
   448  
   449  func f14(p, q *int, a []int) {
   450  	// This crazy ordering usually gives i1 the lowest value ID,
   451  	// j the middle value ID, and i2 the highest value ID.
   452  	// That used to confuse CSE because it ordered the args
   453  	// of the two + ops below differently.
   454  	// That in turn foiled bounds check elimination.
   455  	i1 := *p
   456  	j := *q
   457  	i2 := *p
   458  	useInt(a[i1+j])
   459  	useInt(a[i2+j]) // ERROR "Proved IsInBounds$"
   460  }
   461  
   462  func f14mem(q *int, a []int) (r int) {
   463  	p := &r
   464  	i1 := *q
   465  	*p = 1 // CSE of the "q" pointer load across disjoint store to "p"
   466  	i2 := *q
   467  	useInt(a[i1])
   468  	useInt(a[i2]) // ERROR "Proved IsInBounds$"
   469  	return r
   470  }
   471  
   472  func sliceptr(a *[]int, i int) int {
   473  	var x, y int
   474  	px, py := &x, &y
   475  	*px = (*a)[i]
   476  	*py = (*a)[i] // ERROR "Proved IsInBounds$"
   477  	return x + y
   478  }
   479  
   480  func f15(s []int, x int) {
   481  	useSlice(s[x:])
   482  	useSlice(s[:x]) // ERROR "Proved IsSliceInBounds$"
   483  }
   484  
   485  func f16(s []int) []int {
   486  	if len(s) >= 10 {
   487  		return s[:10] // ERROR "Proved IsSliceInBounds$"
   488  	}
   489  	return nil
   490  }
   491  
   492  func f17(b []int) {
   493  	for i := 0; i < len(b); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
   494  		// This tests for i <= cap, which we can only prove
   495  		// using the derived relation between len and cap.
   496  		// This depends on finding the contradiction, since we
   497  		// don't query this condition directly.
   498  		useSlice(b[:i]) // ERROR "Proved IsSliceInBounds$"
   499  	}
   500  }
   501  
   502  func f18(b []int, x int, y uint) {
   503  	_ = b[x]
   504  	_ = b[y]
   505  
   506  	if x > len(b) { // ERROR "Disproved Less64$"
   507  		return
   508  	}
   509  	if y > uint(len(b)) { // ERROR "Disproved Less64U$"
   510  		return
   511  	}
   512  	if int(y) > len(b) { // ERROR "Disproved Less64$"
   513  		return
   514  	}
   515  }
   516  
   517  func f19() (e int64, err error) {
   518  	// Issue 29502: slice[:0] is incorrectly disproved.
   519  	var stack []int64
   520  	stack = append(stack, 123)
   521  	if len(stack) > 1 {
   522  		panic("too many elements")
   523  	}
   524  	last := len(stack) - 1
   525  	e = stack[last]
   526  	// Buggy compiler prints "Disproved Leq64" for the next line.
   527  	stack = stack[:last]
   528  	return e, nil
   529  }
   530  
   531  func sm1(b []int, x int) {
   532  	// Test constant argument to slicemask.
   533  	useSlice(b[2:8]) // optimized away earlier by rewrite
   534  	// Test non-constant argument with known limits.
   535  	if cap(b) > 10 {
   536  		useSlice(b[2:]) // ERROR "Proved slicemask not needed$"
   537  	}
   538  }
   539  
   540  func lim1(x, y, z int) {
   541  	// Test relations between signed and unsigned limits.
   542  	if x > 5 {
   543  		if uint(x) > 5 { // ERROR "Proved Less64U$"
   544  			return
   545  		}
   546  	}
   547  	if y >= 0 && y < 4 {
   548  		if uint(y) > 4 { // ERROR "Disproved Less64U$"
   549  			return
   550  		}
   551  		if uint(y) < 5 { // ERROR "Proved Less64U$"
   552  			return
   553  		}
   554  	}
   555  	if z < 4 {
   556  		if uint(z) > 4 { // Not provable without disjunctions.
   557  			return
   558  		}
   559  	}
   560  }
   561  
   562  // fence1–4 correspond to the four fence-post implications.
   563  
   564  func fence1(b []int, x, y int) {
   565  	// Test proofs that rely on fence-post implications.
   566  	if x+1 > y {
   567  		if x < y { // ERROR "Disproved Less64$"
   568  			return
   569  		}
   570  	}
   571  	if len(b) < cap(b) {
   572  		// This eliminates the growslice path.
   573  		b = append(b, 1) // ERROR "Disproved Less64U$"
   574  	}
   575  }
   576  
   577  func fence2(x, y int) {
   578  	if x-1 < y {
   579  		if x > y { // ERROR "Disproved Less64$"
   580  			return
   581  		}
   582  	}
   583  }
   584  
   585  func fence3(b, c []int, x, y int64) {
   586  	if x-1 >= y {
   587  		if x <= y { // Can't prove because x may have wrapped.
   588  			return
   589  		}
   590  	}
   591  
   592  	if x != math.MinInt64 && x-1 >= y {
   593  		if x <= y { // ERROR "Disproved Leq64$"
   594  			return
   595  		}
   596  	}
   597  
   598  	c[len(c)-1] = 0 // Can't prove because len(c) might be 0
   599  
   600  	if n := len(b); n > 0 {
   601  		b[n-1] = 0 // ERROR "Proved IsInBounds$"
   602  	}
   603  }
   604  
   605  func fence4(x, y int64) {
   606  	if x >= y+1 {
   607  		if x <= y {
   608  			return
   609  		}
   610  	}
   611  	if y != math.MaxInt64 && x >= y+1 {
   612  		if x <= y { // ERROR "Disproved Leq64$"
   613  			return
   614  		}
   615  	}
   616  }
   617  
   618  // Check transitive relations
   619  func trans1(x, y int64) {
   620  	if x > 5 {
   621  		if y > x {
   622  			if y > 2 { // ERROR "Proved Less64$"
   623  				return
   624  			}
   625  		} else if y == x {
   626  			if y > 5 { // ERROR "Proved Less64$"
   627  				return
   628  			}
   629  		}
   630  	}
   631  	if x >= 10 {
   632  		if y > x {
   633  			if y > 10 { // ERROR "Proved Less64$"
   634  				return
   635  			}
   636  		}
   637  	}
   638  }
   639  
   640  func trans2(a, b []int, i int) {
   641  	if len(a) != len(b) {
   642  		return
   643  	}
   644  
   645  	_ = a[i]
   646  	_ = b[i] // ERROR "Proved IsInBounds$"
   647  }
   648  
   649  func trans3(a, b []int, i int) {
   650  	if len(a) > len(b) {
   651  		return
   652  	}
   653  
   654  	_ = a[i]
   655  	_ = b[i] // ERROR "Proved IsInBounds$"
   656  }
   657  
   658  func trans4(b []byte, x int) {
   659  	// Issue #42603: slice len/cap transitive relations.
   660  	switch x {
   661  	case 0:
   662  		if len(b) < 20 {
   663  			return
   664  		}
   665  		_ = b[:2] // ERROR "Proved IsSliceInBounds$"
   666  	case 1:
   667  		if len(b) < 40 {
   668  			return
   669  		}
   670  		_ = b[:2] // ERROR "Proved IsSliceInBounds$"
   671  	}
   672  }
   673  
   674  // Derived from nat.cmp
   675  func natcmp(x, y []uint) (r int) {
   676  	m := len(x)
   677  	n := len(y)
   678  	if m != n || m == 0 {
   679  		return
   680  	}
   681  
   682  	i := m - 1
   683  	for i > 0 && // ERROR "Induction variable: limits \(0,\?\], increment 1$"
   684  		x[i] == // ERROR "Proved IsInBounds$"
   685  			y[i] { // ERROR "Proved IsInBounds$"
   686  		i--
   687  	}
   688  
   689  	switch {
   690  	case x[i] < // todo, cannot prove this because it's dominated by i<=0 || x[i]==y[i]
   691  		y[i]: // ERROR "Proved IsInBounds$"
   692  		r = -1
   693  	case x[i] > // ERROR "Proved IsInBounds$"
   694  		y[i]: // ERROR "Proved IsInBounds$"
   695  		r = 1
   696  	}
   697  	return
   698  }
   699  
   700  func suffix(s, suffix string) bool {
   701  	// Note: issue 76304
   702  	return len(s) >= len(suffix) && s[len(s)-len(suffix):] == suffix // ERROR "Proved IsSliceInBounds"
   703  }
   704  
   705  func constsuffix(s string) bool {
   706  	return suffix(s, "abc") // ERROR "Proved IsSliceInBounds$" "Proved slicemask not needed$" "Proved Eq64$"
   707  }
   708  
   709  func atexit(foobar []func()) {
   710  	for i := len(foobar) - 1; i >= 0; i-- { // ERROR "Induction variable: limits \[0,\?\], increment 1"
   711  		f := foobar[i]
   712  		foobar = foobar[:i] // ERROR "IsSliceInBounds"
   713  		f()
   714  	}
   715  }
   716  
   717  func make1(n int) []int {
   718  	s := make([]int, n)
   719  	for i := 0; i < n; i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1"
   720  		s[i] = 1 // ERROR "Proved IsInBounds$"
   721  	}
   722  	return s
   723  }
   724  
   725  func make2(n int) []int {
   726  	s := make([]int, n)
   727  	for i := range s { // ERROR "Induction variable: limits \[0,\?\), increment 1"
   728  		s[i] = 1 // ERROR "Proved IsInBounds$"
   729  	}
   730  	return s
   731  }
   732  
   733  // The range tests below test the index variable of range loops.
   734  
   735  // range1 compiles to the "efficiently indexable" form of a range loop.
   736  func range1(b []int) {
   737  	for i, v := range b { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
   738  		b[i] = v + 1    // ERROR "Proved IsInBounds$"
   739  		if i < len(b) { // ERROR "Proved Less64$"
   740  			println("x")
   741  		}
   742  		if i >= 0 { // ERROR "Proved Leq64$"
   743  			println("x")
   744  		}
   745  	}
   746  }
   747  
   748  // range2 elements are larger, so they use the general form of a range loop.
   749  func range2(b [][32]int) {
   750  	for i, v := range b { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
   751  		b[i][0] = v[0] + 1 // ERROR "Proved IsInBounds$"
   752  		if i < len(b) {    // ERROR "Proved Less64$"
   753  			println("x")
   754  		}
   755  		if i >= 0 { // ERROR "Proved Leq64$"
   756  			println("x")
   757  		}
   758  	}
   759  }
   760  
   761  // signhint1-2 test whether the hint (int >= 0) is propagated into the loop.
   762  func signHint1(i int, data []byte) {
   763  	if i >= 0 {
   764  		for i < len(data) { // ERROR "Induction variable: limits \[\?,\?\), increment 1$"
   765  			_ = data[i] // ERROR "Proved IsInBounds$"
   766  			i++
   767  		}
   768  	}
   769  }
   770  
   771  func signHint2(b []byte, n int) {
   772  	if n < 0 {
   773  		panic("")
   774  	}
   775  	_ = b[25]
   776  	for i := n; i <= 25; i++ { // ERROR "Induction variable: limits \[\?,25\], increment 1$"
   777  		b[i] = 123 // ERROR "Proved IsInBounds$"
   778  	}
   779  }
   780  
   781  // indexGT0 tests whether prove learns int index >= 0 from bounds check.
   782  func indexGT0(b []byte, n int) {
   783  	_ = b[n]
   784  	_ = b[25]
   785  
   786  	for i := n; i <= 25; i++ { // ERROR "Induction variable: limits \[\?,25\], increment 1$"
   787  		b[i] = 123 // ERROR "Proved IsInBounds$"
   788  	}
   789  }
   790  
   791  // Induction variable in unrolled loop.
   792  func unrollUpExcl(a []int) int {
   793  	var i, x int
   794  	for i = 0; i < len(a)-1; i += 2 { // ERROR "Induction variable: limits \[0,\?\), increment 2$"
   795  		x += a[i]   // ERROR "Proved IsInBounds$"
   796  		x += a[i+1] // ERROR "Proved IsInBounds( for blocked indexing)?$"
   797  	}
   798  	if i == len(a)-1 {
   799  		x += a[i]
   800  	}
   801  	return x
   802  }
   803  
   804  // Induction variable in unrolled loop.
   805  func unrollUpIncl(a []int) int {
   806  	var i, x int
   807  	for i = 0; i <= len(a)-2; i += 2 { // ERROR "Induction variable: limits \[0,\?\], increment 2$"
   808  		x += a[i]   // ERROR "Proved IsInBounds$"
   809  		x += a[i+1] // ERROR "Proved IsInBounds( for blocked indexing)?$"
   810  	}
   811  	if i == len(a)-1 {
   812  		x += a[i]
   813  	}
   814  	return x
   815  }
   816  
   817  // Induction variable in unrolled loop.
   818  func unrollDownExcl0(a []int) int {
   819  	var i, x int
   820  	for i = len(a) - 1; i > 0; i -= 2 { // ERROR "Induction variable: limits \(0,\?\], increment 2$"
   821  		x += a[i]   // ERROR "Proved IsInBounds$"
   822  		x += a[i-1] // ERROR "Proved IsInBounds$"
   823  	}
   824  	if i == 0 {
   825  		x += a[i]
   826  	}
   827  	return x
   828  }
   829  
   830  // Induction variable in unrolled loop.
   831  func unrollDownExcl1(a []int) int {
   832  	var i, x int
   833  	for i = len(a) - 1; i >= 1; i -= 2 { // ERROR "Induction variable: limits \(0,\?\], increment 2$"
   834  		x += a[i]   // ERROR "Proved IsInBounds$"
   835  		x += a[i-1] // ERROR "Proved IsInBounds$"
   836  	}
   837  	if i == 0 {
   838  		x += a[i]
   839  	}
   840  	return x
   841  }
   842  
   843  // Induction variable in unrolled loop.
   844  func unrollDownInclStep(a []int) int {
   845  	var i, x int
   846  	for i = len(a); i >= 2; i -= 2 { // ERROR "Induction variable: limits \[2,\?\], increment 2$"
   847  		x += a[i-1] // ERROR "Proved IsInBounds$"
   848  		x += a[i-2] // ERROR "Proved IsInBounds$"
   849  	}
   850  	if i == 1 {
   851  		x += a[i-1]
   852  	}
   853  	return x
   854  }
   855  
   856  // Not an induction variable (step too large)
   857  func unrollExclStepTooLarge(a []int) int {
   858  	var i, x int
   859  	for i = 0; i < len(a)-1; i += 3 {
   860  		x += a[i]
   861  		x += a[i+1] // ERROR "Proved IsInBounds( for blocked indexing)?$"
   862  	}
   863  	if i == len(a)-1 {
   864  		x += a[i]
   865  	}
   866  	return x
   867  }
   868  
   869  // Not an induction variable (step too large)
   870  func unrollInclStepTooLarge(a []int) int {
   871  	var i, x int
   872  	for i = 0; i <= len(a)-2; i += 3 {
   873  		x += a[i]
   874  		x += a[i+1] // ERROR "Proved IsInBounds( for blocked indexing)?$"
   875  	}
   876  	if i == len(a)-1 {
   877  		x += a[i]
   878  	}
   879  	return x
   880  }
   881  
   882  // Not an induction variable (min too small, iterating down)
   883  func unrollDecMin(a []int, b int) int {
   884  	if b != math.MinInt64 {
   885  		return 42
   886  	}
   887  	var i, x int
   888  	for i = len(a); i >= b; i -= 2 { // ERROR "Proved Leq64"
   889  		x += a[i-1]
   890  		x += a[i-2]
   891  	}
   892  	if i == 1 {
   893  		x += a[i-1]
   894  	}
   895  	return x
   896  }
   897  
   898  // Not an induction variable (min too small, iterating up -- perhaps could allow, but why bother?)
   899  func unrollIncMin(a []int, b int) int {
   900  	if b != math.MinInt64 {
   901  		return 42
   902  	}
   903  	var i, x int
   904  	for i = len(a); i >= b; i += 2 { // ERROR "Proved Leq64"
   905  		x += a[i-1]
   906  		x += a[i-2]
   907  	}
   908  	if i == 1 {
   909  		x += a[i-1]
   910  	}
   911  	return x
   912  }
   913  
   914  // The 4 xxxxExtNto64 functions below test whether prove is looking
   915  // through value-preserving sign/zero extensions of index values (issue #26292).
   916  
   917  // Look through all extensions
   918  func signExtNto64(x []int, j8 int8, j16 int16, j32 int32) int {
   919  	if len(x) < 22 {
   920  		return 0
   921  	}
   922  	if j8 >= 0 && j8 < 22 {
   923  		return x[j8] // ERROR "Proved IsInBounds$"
   924  	}
   925  	if j16 >= 0 && j16 < 22 {
   926  		return x[j16] // ERROR "Proved IsInBounds$"
   927  	}
   928  	if j32 >= 0 && j32 < 22 {
   929  		return x[j32] // ERROR "Proved IsInBounds$"
   930  	}
   931  	return 0
   932  }
   933  
   934  func zeroExtNto64(x []int, j8 uint8, j16 uint16, j32 uint32) int {
   935  	if len(x) < 22 {
   936  		return 0
   937  	}
   938  	if j8 >= 0 && j8 < 22 {
   939  		return x[j8] // ERROR "Proved IsInBounds$"
   940  	}
   941  	if j16 >= 0 && j16 < 22 {
   942  		return x[j16] // ERROR "Proved IsInBounds$"
   943  	}
   944  	if j32 >= 0 && j32 < 22 {
   945  		return x[j32] // ERROR "Proved IsInBounds$"
   946  	}
   947  	return 0
   948  }
   949  
   950  // Process fence-post implications through 32to64 extensions (issue #29964)
   951  func signExt32to64Fence(x []int, j int32) int {
   952  	if x[j] != 0 {
   953  		return 1
   954  	}
   955  	if j > 0 && x[j-1] != 0 { // ERROR "Proved IsInBounds$"
   956  		return 1
   957  	}
   958  	return 0
   959  }
   960  
   961  func zeroExt32to64Fence(x []int, j uint32) int {
   962  	if x[j] != 0 {
   963  		return 1
   964  	}
   965  	if j > 0 && x[j-1] != 0 { // ERROR "Proved IsInBounds$"
   966  		return 1
   967  	}
   968  	return 0
   969  }
   970  
   971  // Ensure that bounds checks with negative indexes are not incorrectly removed.
   972  func negIndex() {
   973  	n := make([]int, 1)
   974  	for i := -1; i <= 0; i++ { // ERROR "Induction variable: limits \[-1,0\], increment 1$"
   975  		n[i] = 1
   976  	}
   977  }
   978  func negIndex2(n int) {
   979  	a := make([]int, 5)
   980  	b := make([]int, 5)
   981  	c := make([]int, 5)
   982  	for i := -1; i <= 0; i-- {
   983  		b[i] = i
   984  		n++
   985  		if n > 10 {
   986  			break
   987  		}
   988  	}
   989  	useSlice(a)
   990  	useSlice(c)
   991  }
   992  
   993  // These cases are division of a positive signed integer by a power of 2.
   994  // The opt pass doesnt have sufficient information to see that n is positive.
   995  // So, instead, opt rewrites the division with a less-than-optimal replacement.
   996  // Prove, which can see that n is nonnegative, cannot see the division because
   997  // opt, an earlier pass, has already replaced it.
   998  // The fix for this issue allows prove to zero a right shift that was added as
   999  // part of the less-than-optimal reqwrite. That change by prove then allows
  1000  // lateopt to clean up all the unnecessary parts of the original division
  1001  // replacement. See issue #36159.
  1002  func divShiftClean(n int) int {
  1003  	if n < 0 {
  1004  		return n
  1005  	}
  1006  	return n / int(8) // ERROR "Proved Div64 is unsigned$"
  1007  }
  1008  
  1009  func divShiftClean64(n int64) int64 {
  1010  	if n < 0 {
  1011  		return n
  1012  	}
  1013  	return n / int64(16) // ERROR "Proved Div64 is unsigned$"
  1014  }
  1015  
  1016  func divShiftClean32(n int32) int32 {
  1017  	if n < 0 {
  1018  		return n
  1019  	}
  1020  	return n / int32(16) // ERROR "Proved Div32 is unsigned$"
  1021  }
  1022  
  1023  // Bounds check elimination
  1024  
  1025  func sliceBCE1(p []string, h uint) string {
  1026  	if len(p) == 0 {
  1027  		return ""
  1028  	}
  1029  
  1030  	i := h & uint(len(p)-1)
  1031  	return p[i] // ERROR "Proved IsInBounds$"
  1032  }
  1033  
  1034  func sliceBCE2(p []string, h int) string {
  1035  	if len(p) == 0 {
  1036  		return ""
  1037  	}
  1038  	i := h & (len(p) - 1)
  1039  	return p[i] // ERROR "Proved IsInBounds$"
  1040  }
  1041  
  1042  func and(p []byte) ([]byte, []byte) { // issue #52563
  1043  	const blocksize = 16
  1044  	fullBlocks := len(p) &^ (blocksize - 1)
  1045  	blk := p[:fullBlocks] // ERROR "Proved IsSliceInBounds$"
  1046  	rem := p[fullBlocks:] // ERROR "Proved IsSliceInBounds$"
  1047  	return blk, rem
  1048  }
  1049  
  1050  func rshu(x, y uint) int {
  1051  	z := x >> y
  1052  	if z <= x { // ERROR "Proved Leq64U$"
  1053  		return 1
  1054  	}
  1055  	return 0
  1056  }
  1057  
  1058  func divu(x, y uint) int {
  1059  	z := x / y
  1060  	if z <= x { // ERROR "Proved Leq64U$"
  1061  		return 1
  1062  	}
  1063  	return 0
  1064  }
  1065  
  1066  func divuRoundUp(x, y, z uint) int {
  1067  	x &= ^uint(0) >> 8 // can't overflow in add
  1068  	y = min(y, 0xff-1)
  1069  	z = max(z, 0xff)
  1070  	r := (x + y) / z // ERROR "Proved Neq64$"
  1071  	if r <= x {      // ERROR "Proved Leq64U$"
  1072  		return 1
  1073  	}
  1074  	return 0
  1075  }
  1076  
  1077  func divuRoundUpSlice(x []string) {
  1078  	halfRoundedUp := uint(len(x)+1) / 2
  1079  	_ = x[:halfRoundedUp] // ERROR "Proved IsSliceInBounds$"
  1080  	_ = x[halfRoundedUp:] // ERROR "Proved IsSliceInBounds$"
  1081  }
  1082  
  1083  func modu1(x, y uint) int {
  1084  	z := x % y
  1085  	if z < y { // ERROR "Proved Less64U$"
  1086  		return 1
  1087  	}
  1088  	return 0
  1089  }
  1090  
  1091  func modu2(x, y uint) int {
  1092  	z := x % y
  1093  	if z <= x { // ERROR "Proved Leq64U$"
  1094  		return 1
  1095  	}
  1096  	return 0
  1097  }
  1098  
  1099  func issue57077(s []int) (left, right []int) {
  1100  	middle := len(s) / 2 // ERROR "Proved Div64 is unsigned$"
  1101  	left = s[:middle]    // ERROR "Proved IsSliceInBounds$"
  1102  	right = s[middle:]   // ERROR "Proved IsSliceInBounds$"
  1103  	return
  1104  }
  1105  
  1106  func issue76332(s []int) (left, right []int) {
  1107  	middle := len(s) >> 1 // ERROR "Proved Rsh64x64 is unsigned$"
  1108  	left = s[:middle]     // ERROR "Proved IsSliceInBounds$"
  1109  	right = s[middle:]    // ERROR "Proved IsSliceInBounds$"
  1110  	return
  1111  }
  1112  
  1113  func issue51622(b []byte) int {
  1114  	if len(b) >= 3 && b[len(b)-3] == '#' { // ERROR "Proved IsInBounds$"
  1115  		return len(b)
  1116  	}
  1117  	return 0
  1118  }
  1119  
  1120  func issue45928(x int) {
  1121  	combinedFrac := x / (x | (1 << 31)) // ERROR "Proved Neq64$"
  1122  	useInt(combinedFrac)
  1123  }
  1124  
  1125  func constantBounds1(i, j uint) int {
  1126  	var a [10]int
  1127  	if j < 11 && i < j {
  1128  		return a[i] // ERROR "Proved IsInBounds$"
  1129  	}
  1130  	return 0
  1131  }
  1132  
  1133  func constantBounds2(i, j uint) int {
  1134  	var a [10]int
  1135  	if i < j && j < 11 {
  1136  		return a[i] // ERROR "Proved IsInBounds"
  1137  	}
  1138  	return 0
  1139  }
  1140  
  1141  func constantBounds3(i, j, k, l uint) int {
  1142  	var a [8]int
  1143  	if i < j && j < k && k < l && l < 11 {
  1144  		return a[i] // ERROR "Proved IsInBounds"
  1145  	}
  1146  	return 0
  1147  }
  1148  
  1149  func equalityPropagation(a [1]int, i, j uint) int {
  1150  	if i == j && i == 5 {
  1151  		return a[j-5] // ERROR "Proved IsInBounds"
  1152  	}
  1153  	return 0
  1154  }
  1155  func inequalityPropagation(a [1]int, i, j uint) int {
  1156  	if i != j && j >= 5 && j <= 6 && i == 5 {
  1157  		return a[j-6] // ERROR "Proved IsInBounds"
  1158  	}
  1159  	return 0
  1160  }
  1161  
  1162  func issue66826a(a [21]byte) {
  1163  	for i := 0; i <= 10; i++ { // ERROR "Induction variable: limits \[0,10\], increment 1$"
  1164  		_ = a[2*i] // ERROR "Proved IsInBounds"
  1165  	}
  1166  }
  1167  func issue66826b(a [31]byte, i int) {
  1168  	if i < 0 || i > 10 {
  1169  		return
  1170  	}
  1171  	_ = a[3*i] // ERROR "Proved IsInBounds"
  1172  }
  1173  
  1174  func f20(a, b bool) int {
  1175  	if a == b {
  1176  		if a {
  1177  			if b { // ERROR "Proved Arg"
  1178  				return 1
  1179  			}
  1180  		}
  1181  	}
  1182  	return 0
  1183  }
  1184  
  1185  func f21(a, b *int) int {
  1186  	if a == b {
  1187  		if a != nil {
  1188  			if b != nil { // ERROR "Proved IsNonNil"
  1189  				return 1
  1190  			}
  1191  		}
  1192  	}
  1193  	return 0
  1194  }
  1195  
  1196  func f22(b bool, x, y int) int {
  1197  	b2 := x < y
  1198  	if b == b2 {
  1199  		if b {
  1200  			if x >= y { // ERROR "Disproved Leq64$"
  1201  				return 1
  1202  			}
  1203  		}
  1204  	}
  1205  	return 0
  1206  }
  1207  
  1208  func ctz64(x uint64, ensureBothBranchesCouldHappen bool) int {
  1209  	const max = math.MaxUint64
  1210  	sz := bits.Len64(max)
  1211  
  1212  	log2half := uint64(max) >> (sz / 2)
  1213  	if x >= log2half || x == 0 {
  1214  		return 42
  1215  	}
  1216  
  1217  	y := bits.TrailingZeros64(x) // ERROR "Proved Ctz64 non-zero$""
  1218  
  1219  	z := sz / 2
  1220  	if ensureBothBranchesCouldHappen {
  1221  		if y < z { // ERROR "Proved Less64$"
  1222  			return -42
  1223  		}
  1224  	} else {
  1225  		if y >= z { // ERROR "Disproved Leq64$"
  1226  			return 1337
  1227  		}
  1228  	}
  1229  
  1230  	return y
  1231  }
  1232  func ctz32(x uint32, ensureBothBranchesCouldHappen bool) int {
  1233  	const max = math.MaxUint32
  1234  	sz := bits.Len32(max)
  1235  
  1236  	log2half := uint32(max) >> (sz / 2)
  1237  	if x >= log2half || x == 0 {
  1238  		return 42
  1239  	}
  1240  
  1241  	y := bits.TrailingZeros32(x) // ERROR "Proved Ctz32 non-zero$""
  1242  
  1243  	z := sz / 2
  1244  	if ensureBothBranchesCouldHappen {
  1245  		if y < z { // ERROR "Proved Less64$"
  1246  			return -42
  1247  		}
  1248  	} else {
  1249  		if y >= z { // ERROR "Disproved Leq64$"
  1250  			return 1337
  1251  		}
  1252  	}
  1253  
  1254  	return y
  1255  }
  1256  func ctz16(x uint16, ensureBothBranchesCouldHappen bool) int {
  1257  	const max = math.MaxUint16
  1258  	sz := bits.Len16(max)
  1259  
  1260  	log2half := uint16(max) >> (sz / 2)
  1261  	if x >= log2half || x == 0 {
  1262  		return 42
  1263  	}
  1264  
  1265  	y := bits.TrailingZeros16(x) // ERROR "Proved Ctz16 non-zero$""
  1266  
  1267  	z := sz / 2
  1268  	if ensureBothBranchesCouldHappen {
  1269  		if y < z { // ERROR "Proved Less64$"
  1270  			return -42
  1271  		}
  1272  	} else {
  1273  		if y >= z { // ERROR "Disproved Leq64$"
  1274  			return 1337
  1275  		}
  1276  	}
  1277  
  1278  	return y
  1279  }
  1280  func ctz8(x uint8, ensureBothBranchesCouldHappen bool) int {
  1281  	const max = math.MaxUint8
  1282  	sz := bits.Len8(max)
  1283  
  1284  	log2half := uint8(max) >> (sz / 2)
  1285  	if x >= log2half || x == 0 {
  1286  		return 42
  1287  	}
  1288  
  1289  	y := bits.TrailingZeros8(x) // ERROR "Proved Ctz8 non-zero$""
  1290  
  1291  	z := sz / 2
  1292  	if ensureBothBranchesCouldHappen {
  1293  		if y < z { // ERROR "Proved Less64$"
  1294  			return -42
  1295  		}
  1296  	} else {
  1297  		if y >= z { // ERROR "Disproved Leq64$"
  1298  			return 1337
  1299  		}
  1300  	}
  1301  
  1302  	return y
  1303  }
  1304  
  1305  func bitLen64(x uint64, ensureBothBranchesCouldHappen bool) int {
  1306  	const max = math.MaxUint64
  1307  	sz := bits.Len64(max)
  1308  
  1309  	if x >= max>>3 {
  1310  		return 42
  1311  	}
  1312  	if x <= max>>6 {
  1313  		return 42
  1314  	}
  1315  
  1316  	y := bits.Len64(x)
  1317  
  1318  	if ensureBothBranchesCouldHappen {
  1319  		if sz-6 <= y && y <= sz-3 { // ERROR "Proved Leq64$"
  1320  			return -42
  1321  		}
  1322  	} else {
  1323  		if y < sz-6 || sz-3 < y { // ERROR "Disproved Less64$"
  1324  			return 1337
  1325  		}
  1326  	}
  1327  	return y
  1328  }
  1329  func bitLen32(x uint32, ensureBothBranchesCouldHappen bool) int {
  1330  	const max = math.MaxUint32
  1331  	sz := bits.Len32(max)
  1332  
  1333  	if x >= max>>3 {
  1334  		return 42
  1335  	}
  1336  	if x <= max>>6 {
  1337  		return 42
  1338  	}
  1339  
  1340  	y := bits.Len32(x)
  1341  
  1342  	if ensureBothBranchesCouldHappen {
  1343  		if sz-6 <= y && y <= sz-3 { // ERROR "Proved Leq64$"
  1344  			return -42
  1345  		}
  1346  	} else {
  1347  		if y < sz-6 || sz-3 < y { // ERROR "Disproved Less64$"
  1348  			return 1337
  1349  		}
  1350  	}
  1351  	return y
  1352  }
  1353  func bitLen16(x uint16, ensureBothBranchesCouldHappen bool) int {
  1354  	const max = math.MaxUint16
  1355  	sz := bits.Len16(max)
  1356  
  1357  	if x >= max>>3 {
  1358  		return 42
  1359  	}
  1360  	if x <= max>>6 {
  1361  		return 42
  1362  	}
  1363  
  1364  	y := bits.Len16(x)
  1365  
  1366  	if ensureBothBranchesCouldHappen {
  1367  		if sz-6 <= y && y <= sz-3 { // ERROR "Proved Leq64$"
  1368  			return -42
  1369  		}
  1370  	} else {
  1371  		if y < sz-6 || sz-3 < y { // ERROR "Disproved Less64$"
  1372  			return 1337
  1373  		}
  1374  	}
  1375  	return y
  1376  }
  1377  func bitLen8(x uint8, ensureBothBranchesCouldHappen bool) int {
  1378  	const max = math.MaxUint8
  1379  	sz := bits.Len8(max)
  1380  
  1381  	if x >= max>>3 {
  1382  		return 42
  1383  	}
  1384  	if x <= max>>6 {
  1385  		return 42
  1386  	}
  1387  
  1388  	y := bits.Len8(x)
  1389  
  1390  	if ensureBothBranchesCouldHappen {
  1391  		if sz-6 <= y && y <= sz-3 { // ERROR "Proved Leq64$"
  1392  			return -42
  1393  		}
  1394  	} else {
  1395  		if y < sz-6 || sz-3 < y { // ERROR "Disproved Less64$"
  1396  			return 1337
  1397  		}
  1398  	}
  1399  	return y
  1400  }
  1401  
  1402  func xor64(a, b uint64, ensureBothBranchesCouldHappen bool) int {
  1403  	a = min(a, 0xff)
  1404  	b = min(b, 0xfff)
  1405  
  1406  	z := a ^ b
  1407  
  1408  	if ensureBothBranchesCouldHappen {
  1409  		if z > 0xfff { // ERROR "Disproved Less64U$"
  1410  			return 42
  1411  		}
  1412  	} else {
  1413  		if z <= 0xfff { // ERROR "Proved Leq64U$"
  1414  			return 1337
  1415  		}
  1416  	}
  1417  	return int(z)
  1418  }
  1419  
  1420  func or64(a, b uint64, ensureBothBranchesCouldHappen bool) int {
  1421  	a = min(a, 0xff)
  1422  	b = min(b, 0xfff)
  1423  
  1424  	z := a | b
  1425  
  1426  	if ensureBothBranchesCouldHappen {
  1427  		if z > 0xfff { // ERROR "Disproved Less64U$"
  1428  			return 42
  1429  		}
  1430  	} else {
  1431  		if z <= 0xfff { // ERROR "Proved Leq64U$"
  1432  			return 1337
  1433  		}
  1434  	}
  1435  	return int(z)
  1436  }
  1437  
  1438  func mod64uWithSmallerDividendMax(a, b uint64, ensureBothBranchesCouldHappen bool) int {
  1439  	a = min(a, 0xff)
  1440  	b = min(b, 0xfff)
  1441  
  1442  	z := bits.Len64(a % b) // see go.dev/issue/68857 for bits.Len64
  1443  
  1444  	if ensureBothBranchesCouldHappen {
  1445  		if z > bits.Len64(0xff) { // ERROR "Disproved Less64$"
  1446  			return 42
  1447  		}
  1448  	} else {
  1449  		if z <= bits.Len64(0xff) { // ERROR "Proved Leq64$"
  1450  			return 1337
  1451  		}
  1452  	}
  1453  	return z
  1454  }
  1455  func mod64uWithSmallerDivisorMax(a, b uint64, ensureBothBranchesCouldHappen bool) int {
  1456  	a = min(a, 0xfff)
  1457  	b = min(b, 0x10) // we need bits.Len64(b.umax) != bits.Len64(b.umax-1)
  1458  
  1459  	z := bits.Len64(a % b) // see go.dev/issue/68857 for bits.Len64
  1460  
  1461  	if ensureBothBranchesCouldHappen {
  1462  		if z > bits.Len64(0x10-1) { // ERROR "Disproved Less64$"
  1463  			return 42
  1464  		}
  1465  	} else {
  1466  		if z <= bits.Len64(0x10-1) { // ERROR "Proved Leq64$"
  1467  			return 1337
  1468  		}
  1469  	}
  1470  	return z
  1471  }
  1472  func mod64uWithIdenticalMax(a, b uint64, ensureBothBranchesCouldHappen bool) int {
  1473  	a = min(a, 0x10)
  1474  	b = min(b, 0x10) // we need bits.Len64(b.umax) != bits.Len64(b.umax-1)
  1475  
  1476  	z := bits.Len64(a % b) // see go.dev/issue/68857 for bits.Len64
  1477  
  1478  	if ensureBothBranchesCouldHappen {
  1479  		if z > bits.Len64(0x10-1) { // ERROR "Disproved Less64$"
  1480  			return 42
  1481  		}
  1482  	} else {
  1483  		if z <= bits.Len64(0x10-1) { // ERROR "Proved Leq64$"
  1484  			return 1337
  1485  		}
  1486  	}
  1487  	return z
  1488  }
  1489  func mod64sPositiveWithSmallerDividendMax(a, b int64, ensureBothBranchesCouldHappen bool) int64 {
  1490  	if a < 0 || b < 0 {
  1491  		return 42
  1492  	}
  1493  	a = min(a, 0xff)
  1494  	b = min(b, 0xfff)
  1495  
  1496  	z := a % b // ERROR "Proved Mod64 is unsigned$"
  1497  
  1498  	if ensureBothBranchesCouldHappen {
  1499  		if z > 0xff { // ERROR "Disproved Less64$"
  1500  			return 42
  1501  		}
  1502  	} else {
  1503  		if z <= 0xff { // ERROR "Proved Leq64$"
  1504  			return 1337
  1505  		}
  1506  	}
  1507  	return z
  1508  }
  1509  func mod64sPositiveWithSmallerDivisorMax(a, b int64, ensureBothBranchesCouldHappen bool) int64 {
  1510  	if a < 0 || b < 0 {
  1511  		return 42
  1512  	}
  1513  	a = min(a, 0xfff)
  1514  	b = min(b, 0xff)
  1515  
  1516  	z := a % b // ERROR "Proved Mod64 is unsigned$"
  1517  
  1518  	if ensureBothBranchesCouldHappen {
  1519  		if z > 0xff-1 { // ERROR "Disproved Less64$"
  1520  			return 42
  1521  		}
  1522  	} else {
  1523  		if z <= 0xff-1 { // ERROR "Proved Leq64$"
  1524  			return 1337
  1525  		}
  1526  	}
  1527  	return z
  1528  }
  1529  func mod64sPositiveWithIdenticalMax(a, b int64, ensureBothBranchesCouldHappen bool) int64 {
  1530  	if a < 0 || b < 0 {
  1531  		return 42
  1532  	}
  1533  	a = min(a, 0xfff)
  1534  	b = min(b, 0xfff)
  1535  
  1536  	z := a % b // ERROR "Proved Mod64 is unsigned$"
  1537  
  1538  	if ensureBothBranchesCouldHappen {
  1539  		if z > 0xfff-1 { // ERROR "Disproved Less64$"
  1540  			return 42
  1541  		}
  1542  	} else {
  1543  		if z <= 0xfff-1 { // ERROR "Proved Leq64$"
  1544  			return 1337
  1545  		}
  1546  	}
  1547  	return z
  1548  }
  1549  
  1550  func div64u(a, b uint64, ensureAllBranchesCouldHappen func() bool) uint64 {
  1551  	a = min(a, 0xffff)
  1552  	a = max(a, 0xfff)
  1553  	b = min(b, 0xff)
  1554  	b = max(b, 0xf)
  1555  
  1556  	z := a / b // ERROR "Proved Neq64$"
  1557  
  1558  	if ensureAllBranchesCouldHappen() && z > 0xffff/0xf { // ERROR "Disproved Less64U$"
  1559  		return 42
  1560  	}
  1561  	if ensureAllBranchesCouldHappen() && z <= 0xffff/0xf { // ERROR "Proved Leq64U$"
  1562  		return 1337
  1563  	}
  1564  	if ensureAllBranchesCouldHappen() && z < 0xfff/0xff { // ERROR "Disproved Less64U$"
  1565  		return 42
  1566  	}
  1567  	if ensureAllBranchesCouldHappen() && z >= 0xfff/0xff { // ERROR "Proved Leq64U$"
  1568  		return 42
  1569  	}
  1570  	return z
  1571  }
  1572  func div64s(a, b int64, ensureAllBranchesCouldHappen func() bool) int64 {
  1573  	if a < 0 || b < 0 {
  1574  		return 42
  1575  	}
  1576  	a = min(a, 0xffff)
  1577  	a = max(a, 0xfff)
  1578  	b = min(b, 0xff)
  1579  	b = max(b, 0xf)
  1580  
  1581  	z := a / b // ERROR "Proved Div64 is unsigned|Proved Neq64"
  1582  
  1583  	if ensureAllBranchesCouldHappen() && z > 0xffff/0xf { // ERROR "Disproved Less64$"
  1584  		return 42
  1585  	}
  1586  	if ensureAllBranchesCouldHappen() && z <= 0xffff/0xf { // ERROR "Proved Leq64$"
  1587  		return 1337
  1588  	}
  1589  	if ensureAllBranchesCouldHappen() && z < 0xfff/0xff { // ERROR "Disproved Less64$"
  1590  		return 42
  1591  	}
  1592  	if ensureAllBranchesCouldHappen() && z >= 0xfff/0xff { // ERROR "Proved Leq64$"
  1593  		return 42
  1594  	}
  1595  	return z
  1596  }
  1597  
  1598  func trunc64to16(a uint64, ensureAllBranchesCouldHappen func() bool) uint16 {
  1599  	a = min(a, 0xfff)
  1600  	a = max(a, 0xff)
  1601  
  1602  	z := uint16(a)
  1603  	if ensureAllBranchesCouldHappen() && z > 0xfff { // ERROR "Disproved Less16U$"
  1604  		return 42
  1605  	}
  1606  	if ensureAllBranchesCouldHappen() && z <= 0xfff { // ERROR "Proved Leq16U$"
  1607  		return 1337
  1608  	}
  1609  	if ensureAllBranchesCouldHappen() && z < 0xff { // ERROR "Disproved Less16U$"
  1610  		return 42
  1611  	}
  1612  	if ensureAllBranchesCouldHappen() && z >= 0xff { // ERROR "Proved Leq16U$"
  1613  		return 1337
  1614  	}
  1615  	return z
  1616  }
  1617  
  1618  func com64(a uint64, ensureAllBranchesCouldHappen func() bool) uint64 {
  1619  	a = min(a, 0xffff)
  1620  	a = max(a, 0xff)
  1621  
  1622  	z := ^a
  1623  
  1624  	if ensureAllBranchesCouldHappen() && z > ^uint64(0xff) { // ERROR "Disproved Less64U$"
  1625  		return 42
  1626  	}
  1627  	if ensureAllBranchesCouldHappen() && z <= ^uint64(0xff) { // ERROR "Proved Leq64U$"
  1628  		return 1337
  1629  	}
  1630  	if ensureAllBranchesCouldHappen() && z < ^uint64(0xffff) { // ERROR "Disproved Less64U$"
  1631  		return 42
  1632  	}
  1633  	if ensureAllBranchesCouldHappen() && z >= ^uint64(0xffff) { // ERROR "Proved Leq64U$"
  1634  		return 1337
  1635  	}
  1636  	return z
  1637  }
  1638  
  1639  func neg64(a uint64, ensureAllBranchesCouldHappen func() bool) uint64 {
  1640  	var lo, hi uint64 = 0xff, 0xfff
  1641  	a = min(a, hi)
  1642  	a = max(a, lo)
  1643  
  1644  	z := -a
  1645  
  1646  	if ensureAllBranchesCouldHappen() && z > -lo { // ERROR "Disproved Less64U$"
  1647  		return 42
  1648  	}
  1649  	if ensureAllBranchesCouldHappen() && z <= -lo { // ERROR "Proved Leq64U$"
  1650  		return 1337
  1651  	}
  1652  	if ensureAllBranchesCouldHappen() && z < -hi { // ERROR "Disproved Less64U$"
  1653  		return 42
  1654  	}
  1655  	if ensureAllBranchesCouldHappen() && z >= -hi { // ERROR "Proved Leq64U$"
  1656  		return 1337
  1657  	}
  1658  	return z
  1659  }
  1660  func neg64mightOverflowDuringNeg(a uint64, ensureAllBranchesCouldHappen func() bool) uint64 {
  1661  	var lo, hi uint64 = 0, 0xfff
  1662  	a = min(a, hi)
  1663  	a = max(a, lo)
  1664  
  1665  	z := -a
  1666  
  1667  	if ensureAllBranchesCouldHappen() && z > -lo {
  1668  		return 42
  1669  	}
  1670  	if ensureAllBranchesCouldHappen() && z <= -lo {
  1671  		return 1337
  1672  	}
  1673  	if ensureAllBranchesCouldHappen() && z < -hi {
  1674  		return 42
  1675  	}
  1676  	if ensureAllBranchesCouldHappen() && z >= -hi {
  1677  		return 1337
  1678  	}
  1679  	return z
  1680  }
  1681  
  1682  func phiMin(a, b []byte) {
  1683  	_ = a[:min(len(a), len(b))] // ERROR "Proved IsSliceInBounds"
  1684  	_ = b[:min(len(a), len(b))] // ERROR "Proved IsSliceInBounds"
  1685  	_ = a[:max(len(a), len(b))]
  1686  	_ = b[:max(len(a), len(b))]
  1687  	x := len(a)
  1688  	if x > len(b) {
  1689  		x = len(b)
  1690  		useInt(0)
  1691  	}
  1692  	_ = a[:x] // ERROR "Proved IsSliceInBounds"
  1693  	y := len(a)
  1694  	if y > len(b) {
  1695  		y = len(b)
  1696  		useInt(0)
  1697  	} else {
  1698  		useInt(1)
  1699  	}
  1700  	_ = b[:y] // ERROR "Proved IsSliceInBounds"
  1701  }
  1702  
  1703  func minPhiLeq[T uint | int](x, y T) (z T) {
  1704  	if x <= y {
  1705  		z = x
  1706  	} else {
  1707  		z = y
  1708  	}
  1709  	return z
  1710  }
  1711  func maxPhiLeq[T uint | int](x, y T) (z T) {
  1712  	if y <= x {
  1713  		z = x
  1714  	} else {
  1715  		z = y
  1716  	}
  1717  	return z
  1718  }
  1719  func mathBasedOnPhiLosangeMinUFirstLeq(x uint, ensureAllBranchesCouldHappen func() bool) uint {
  1720  	const maxc = 0xf2a
  1721  	const minc = 0xf0a
  1722  	x = minPhiLeq(x, maxc)
  1723  	x = maxPhiLeq(x, minc)
  1724  
  1725  	const k = 1
  1726  	x += k
  1727  
  1728  	if ensureAllBranchesCouldHappen() && x > maxc+k { // ERROR "Disproved Less64U$"
  1729  		return 42
  1730  	}
  1731  	if ensureAllBranchesCouldHappen() && x <= maxc+k { // ERROR "Proved Leq64U$"
  1732  		return 4242
  1733  	}
  1734  	if ensureAllBranchesCouldHappen() && x < minc+k { // ERROR "Disproved Less64U$"
  1735  		return 424242
  1736  	}
  1737  	if ensureAllBranchesCouldHappen() && x >= minc+k { // ERROR "Proved Leq64U$"
  1738  		return 42424242
  1739  	}
  1740  	return x
  1741  }
  1742  func mathBasedOnPhiLosangeMinUSecondLeq(x uint, ensureAllBranchesCouldHappen func() bool) uint {
  1743  	const maxc = 0xf2a
  1744  	const minc = 0xf0a
  1745  	x = maxPhiLeq(x, minc)
  1746  	x = minPhiLeq(x, maxc)
  1747  
  1748  	const k = 1
  1749  	x += k
  1750  
  1751  	if ensureAllBranchesCouldHappen() && x > maxc+k { // ERROR "Disproved Less64U$"
  1752  		return 42
  1753  	}
  1754  	if ensureAllBranchesCouldHappen() && x <= maxc+k { // ERROR "Proved Leq64U$"
  1755  		return 4242
  1756  	}
  1757  	if ensureAllBranchesCouldHappen() && x < minc+k { // ERROR "Disproved Less64U$"
  1758  		return 424242
  1759  	}
  1760  	if ensureAllBranchesCouldHappen() && x >= minc+k { // ERROR "Proved Leq64U$"
  1761  		return 42424242
  1762  	}
  1763  	return x
  1764  }
  1765  func mathBasedOnPhiLosangeMinFirstLeq(x int, ensureAllBranchesCouldHappen func() bool) int {
  1766  	const maxc = 0xf2a
  1767  	const minc = 0xf0a
  1768  	x = minPhiLeq(x, maxc)
  1769  	x = maxPhiLeq(x, minc)
  1770  
  1771  	const k = 1
  1772  	x += k
  1773  
  1774  	if ensureAllBranchesCouldHappen() && x > maxc+k { // ERROR "Disproved Less64$"
  1775  		return 42
  1776  	}
  1777  	if ensureAllBranchesCouldHappen() && x <= maxc+k { // ERROR "Proved Leq64$"
  1778  		return 4242
  1779  	}
  1780  	if ensureAllBranchesCouldHappen() && x < minc+k { // ERROR "Disproved Less64$"
  1781  		return 424242
  1782  	}
  1783  	if ensureAllBranchesCouldHappen() && x >= minc+k { // ERROR "Proved Leq64$"
  1784  		return 42424242
  1785  	}
  1786  	return x
  1787  }
  1788  func mathBasedOnPhiLosangeMinSecondLeq(x int, ensureAllBranchesCouldHappen func() bool) int {
  1789  	const maxc = 0xf2a
  1790  	const minc = 0xf0a
  1791  	x = maxPhiLeq(x, minc)
  1792  	x = minPhiLeq(x, maxc)
  1793  
  1794  	const k = 1
  1795  	x += k
  1796  
  1797  	if ensureAllBranchesCouldHappen() && x > maxc+k { // ERROR "Disproved Less64$"
  1798  		return 42
  1799  	}
  1800  	if ensureAllBranchesCouldHappen() && x <= maxc+k { // ERROR "Proved Leq64$"
  1801  		return 4242
  1802  	}
  1803  	if ensureAllBranchesCouldHappen() && x < minc+k { // ERROR "Disproved Less64$"
  1804  		return 424242
  1805  	}
  1806  	if ensureAllBranchesCouldHappen() && x >= minc+k { // ERROR "Proved Leq64$"
  1807  		return 42424242
  1808  	}
  1809  	return x
  1810  }
  1811  
  1812  func minPhiLess[T uint | int](x, y T) (z T) {
  1813  	if x < y {
  1814  		z = x
  1815  	} else {
  1816  		z = y
  1817  	}
  1818  	return z
  1819  }
  1820  func maxPhiLess[T uint | int](x, y T) (z T) {
  1821  	if y < x {
  1822  		z = x
  1823  	} else {
  1824  		z = y
  1825  	}
  1826  	return z
  1827  }
  1828  func mathBasedOnPhiLosangeMinUFirstLess(x uint, ensureAllBranchesCouldHappen func() bool) uint {
  1829  	const maxc = 0xf2a
  1830  	const minc = 0xf0a
  1831  	x = minPhiLess(x, maxc)
  1832  	x = maxPhiLess(x, minc)
  1833  
  1834  	const k = 1
  1835  	x += k
  1836  
  1837  	if ensureAllBranchesCouldHappen() && x > maxc+k { // ERROR "Disproved Less64U$"
  1838  		return 42
  1839  	}
  1840  	if ensureAllBranchesCouldHappen() && x <= maxc+k { // ERROR "Proved Leq64U$"
  1841  		return 4242
  1842  	}
  1843  	if ensureAllBranchesCouldHappen() && x < minc+k { // ERROR "Disproved Less64U$"
  1844  		return 424242
  1845  	}
  1846  	if ensureAllBranchesCouldHappen() && x >= minc+k { // ERROR "Proved Leq64U$"
  1847  		return 42424242
  1848  	}
  1849  	return x
  1850  }
  1851  func mathBasedOnPhiLosangeMinUSecondLess(x uint, ensureAllBranchesCouldHappen func() bool) uint {
  1852  	const maxc = 0xf2a
  1853  	const minc = 0xf0a
  1854  	x = maxPhiLess(x, minc)
  1855  	x = minPhiLess(x, maxc)
  1856  
  1857  	const k = 1
  1858  	x += k
  1859  
  1860  	if ensureAllBranchesCouldHappen() && x > maxc+k { // ERROR "Disproved Less64U$"
  1861  		return 42
  1862  	}
  1863  	if ensureAllBranchesCouldHappen() && x <= maxc+k { // ERROR "Proved Leq64U$"
  1864  		return 4242
  1865  	}
  1866  	if ensureAllBranchesCouldHappen() && x < minc+k { // ERROR "Disproved Less64U$"
  1867  		return 424242
  1868  	}
  1869  	if ensureAllBranchesCouldHappen() && x >= minc+k { // ERROR "Proved Leq64U$"
  1870  		return 42424242
  1871  	}
  1872  	return x
  1873  }
  1874  func mathBasedOnPhiLosangeMinFirstLess(x int, ensureAllBranchesCouldHappen func() bool) int {
  1875  	const maxc = 0xf2a
  1876  	const minc = 0xf0a
  1877  	x = minPhiLess(x, maxc)
  1878  	x = maxPhiLess(x, minc)
  1879  
  1880  	const k = 1
  1881  	x += k
  1882  
  1883  	if ensureAllBranchesCouldHappen() && x > maxc+k { // ERROR "Disproved Less64$"
  1884  		return 42
  1885  	}
  1886  	if ensureAllBranchesCouldHappen() && x <= maxc+k { // ERROR "Proved Leq64$"
  1887  		return 4242
  1888  	}
  1889  	if ensureAllBranchesCouldHappen() && x < minc+k { // ERROR "Disproved Less64$"
  1890  		return 424242
  1891  	}
  1892  	if ensureAllBranchesCouldHappen() && x >= minc+k { // ERROR "Proved Leq64$"
  1893  		return 42424242
  1894  	}
  1895  	return x
  1896  }
  1897  func mathBasedOnPhiLosangeMinSecondLess(x int, ensureAllBranchesCouldHappen func() bool) int {
  1898  	const maxc = 0xf2a
  1899  	const minc = 0xf0a
  1900  	x = maxPhiLess(x, minc)
  1901  	x = minPhiLess(x, maxc)
  1902  
  1903  	const k = 1
  1904  	x += k
  1905  
  1906  	if ensureAllBranchesCouldHappen() && x > maxc+k { // ERROR "Disproved Less64$"
  1907  		return 42
  1908  	}
  1909  	if ensureAllBranchesCouldHappen() && x <= maxc+k { // ERROR "Proved Leq64$"
  1910  		return 4242
  1911  	}
  1912  	if ensureAllBranchesCouldHappen() && x < minc+k { // ERROR "Disproved Less64$"
  1913  		return 424242
  1914  	}
  1915  	if ensureAllBranchesCouldHappen() && x >= minc+k { // ERROR "Proved Leq64$"
  1916  		return 42424242
  1917  	}
  1918  	return x
  1919  }
  1920  
  1921  func mathBasedOnPhiBuiltinMinUFirst(x uint, ensureAllBranchesCouldHappen func() bool) uint {
  1922  	const maxc = 0xf2a
  1923  	const minc = 0xf0a
  1924  	x = min(x, maxc)
  1925  	x = max(x, minc)
  1926  
  1927  	const k = 1
  1928  	x += k
  1929  
  1930  	if ensureAllBranchesCouldHappen() && x > maxc+k { // ERROR "Disproved Less64U$"
  1931  		return 42
  1932  	}
  1933  	if ensureAllBranchesCouldHappen() && x <= maxc+k { // ERROR "Proved Leq64U$"
  1934  		return 4242
  1935  	}
  1936  	if ensureAllBranchesCouldHappen() && x < minc+k { // ERROR "Disproved Less64U$"
  1937  		return 424242
  1938  	}
  1939  	if ensureAllBranchesCouldHappen() && x >= minc+k { // ERROR "Proved Leq64U$"
  1940  		return 42424242
  1941  	}
  1942  	return x
  1943  }
  1944  func mathBasedOnPhiBuiltinMinUSecond(x uint, ensureAllBranchesCouldHappen func() bool) uint {
  1945  	const maxc = 0xf2a
  1946  	const minc = 0xf0a
  1947  	x = max(x, minc)
  1948  	x = min(x, maxc)
  1949  
  1950  	const k = 1
  1951  	x += k
  1952  
  1953  	if ensureAllBranchesCouldHappen() && x > maxc+k { // ERROR "Disproved Less64U$"
  1954  		return 42
  1955  	}
  1956  	if ensureAllBranchesCouldHappen() && x <= maxc+k { // ERROR "Proved Leq64U$"
  1957  		return 4242
  1958  	}
  1959  	if ensureAllBranchesCouldHappen() && x < minc+k { // ERROR "Disproved Less64U$"
  1960  		return 424242
  1961  	}
  1962  	if ensureAllBranchesCouldHappen() && x >= minc+k { // ERROR "Proved Leq64U$"
  1963  		return 42424242
  1964  	}
  1965  	return x
  1966  }
  1967  func mathBasedOnPhiBuiltinMinFirst(x int, ensureAllBranchesCouldHappen func() bool) int {
  1968  	const maxc = 0xf2a
  1969  	const minc = 0xf0a
  1970  	x = min(x, maxc)
  1971  	x = max(x, minc)
  1972  
  1973  	const k = 1
  1974  	x += k
  1975  
  1976  	if ensureAllBranchesCouldHappen() && x > maxc+k { // ERROR "Disproved Less64$"
  1977  		return 42
  1978  	}
  1979  	if ensureAllBranchesCouldHappen() && x <= maxc+k { // ERROR "Proved Leq64$"
  1980  		return 4242
  1981  	}
  1982  	if ensureAllBranchesCouldHappen() && x < minc+k { // ERROR "Disproved Less64$"
  1983  		return 424242
  1984  	}
  1985  	if ensureAllBranchesCouldHappen() && x >= minc+k { // ERROR "Proved Leq64$"
  1986  		return 42424242
  1987  	}
  1988  	return x
  1989  }
  1990  func mathBasedOnPhiBuiltinMinSecond(x int, ensureAllBranchesCouldHappen func() bool) int {
  1991  	const maxc = 0xf2a
  1992  	const minc = 0xf0a
  1993  	x = max(x, minc)
  1994  	x = min(x, maxc)
  1995  
  1996  	const k = 1
  1997  	x += k
  1998  
  1999  	if ensureAllBranchesCouldHappen() && x > maxc+k { // ERROR "Disproved Less64$"
  2000  		return 42
  2001  	}
  2002  	if ensureAllBranchesCouldHappen() && x <= maxc+k { // ERROR "Proved Leq64$"
  2003  		return 4242
  2004  	}
  2005  	if ensureAllBranchesCouldHappen() && x < minc+k { // ERROR "Disproved Less64$"
  2006  		return 424242
  2007  	}
  2008  	if ensureAllBranchesCouldHappen() && x >= minc+k { // ERROR "Proved Leq64$"
  2009  		return 42424242
  2010  	}
  2011  	return x
  2012  }
  2013  
  2014  func issue16833(a, b []byte) {
  2015  	n := copy(a, b)
  2016  	_ = a[n:] // ERROR "Proved IsSliceInBounds"
  2017  	_ = b[n:] // ERROR "Proved IsSliceInBounds"
  2018  	_ = a[:n] // ERROR "Proved IsSliceInBounds"
  2019  	_ = b[:n] // ERROR "Proved IsSliceInBounds"
  2020  }
  2021  
  2022  func clampedIdx1(x []int, i int) int {
  2023  	if len(x) == 0 {
  2024  		return 0
  2025  	}
  2026  	return x[min(max(0, i), len(x)-1)] // ERROR "Proved IsInBounds"
  2027  }
  2028  func clampedIdx2(x []int, i int) int {
  2029  	if len(x) == 0 {
  2030  		return 0
  2031  	}
  2032  	return x[max(min(i, len(x)-1), 0)] // TODO: can't get rid of this bounds check yet
  2033  }
  2034  
  2035  func cvtBoolToUint8Disprove(b bool) byte {
  2036  	var c byte
  2037  	if b {
  2038  		c = 1
  2039  	}
  2040  	if c == 2 { // ERROR "Disproved Eq8"
  2041  		c = 3
  2042  	}
  2043  	return c
  2044  }
  2045  func cvtBoolToUint8BCE(b bool, a [2]int64) int64 {
  2046  	c := byte(0)
  2047  	if b {
  2048  		c = 1
  2049  	}
  2050  	return a[c] // ERROR "Proved IsInBounds$"
  2051  }
  2052  
  2053  func transitiveProofsThroughNonOverflowingUnsignedAdd(x, y, z uint64) {
  2054  	x &= 1<<63 - 1
  2055  	y &= 1<<63 - 1
  2056  
  2057  	a := x + y
  2058  	if a > z {
  2059  		return
  2060  	}
  2061  
  2062  	if x > z { // ERROR "Disproved Less64U$"
  2063  		return
  2064  	}
  2065  	if y > z { // ERROR "Disproved Less64U$"
  2066  		return
  2067  	}
  2068  	if a == x {
  2069  		return
  2070  	}
  2071  	if a == y {
  2072  		return
  2073  	}
  2074  
  2075  	x |= 1
  2076  	y |= 1
  2077  	a = x + y
  2078  	if a == x { // ERROR "Disproved Eq64$"
  2079  		return
  2080  	}
  2081  	if a == y { // ERROR "Disproved Eq64$"
  2082  		return
  2083  	}
  2084  }
  2085  
  2086  func transitiveProofsThroughOverflowingUnsignedAdd(x, y, z uint64) {
  2087  	a := x + y
  2088  	if a > z {
  2089  		return
  2090  	}
  2091  
  2092  	if x > z {
  2093  		return
  2094  	}
  2095  	if y > z {
  2096  		return
  2097  	}
  2098  	if a == x {
  2099  		return
  2100  	}
  2101  	if a == y {
  2102  		return
  2103  	}
  2104  
  2105  	x |= 1
  2106  	y |= 1
  2107  	a = x + y
  2108  	if a == x {
  2109  		return
  2110  	}
  2111  	if a == y {
  2112  		return
  2113  	}
  2114  }
  2115  
  2116  func transitiveProofsThroughNonOverflowingSignedAddPositive(x, y, z int64) {
  2117  	x &= 1<<62 - 1
  2118  	y &= 1<<62 - 1
  2119  
  2120  	a := x + y
  2121  	if a > z {
  2122  		return
  2123  	}
  2124  
  2125  	if x > z { // ERROR "Disproved Less64$"
  2126  		return
  2127  	}
  2128  	if y > z { // ERROR "Disproved Less64$"
  2129  		return
  2130  	}
  2131  	if a == x {
  2132  		return
  2133  	}
  2134  	if a == y {
  2135  		return
  2136  	}
  2137  
  2138  	x |= 1
  2139  	y |= 1
  2140  	a = x + y
  2141  	if a == x { // ERROR "Disproved Eq64$"
  2142  		return
  2143  	}
  2144  	if a == y { // ERROR "Disproved Eq64$"
  2145  		return
  2146  	}
  2147  }
  2148  
  2149  func transitiveProofsThroughOverflowingSignedAddPositive(x, y, z int64) {
  2150  	if x < 0 || y < 0 {
  2151  		return
  2152  	}
  2153  
  2154  	a := x + y
  2155  	if a > z {
  2156  		return
  2157  	}
  2158  
  2159  	if x > z {
  2160  		return
  2161  	}
  2162  	if y > z {
  2163  		return
  2164  	}
  2165  	if a == x {
  2166  		return
  2167  	}
  2168  	if a == y {
  2169  		return
  2170  	}
  2171  
  2172  	x |= 1
  2173  	y |= 1
  2174  	a = x + y
  2175  	if a == x { // ERROR "Disproved Eq64$"
  2176  		return
  2177  	}
  2178  	if a == y { // ERROR "Disproved Eq64$"
  2179  		return
  2180  	}
  2181  }
  2182  
  2183  func transitiveProofsThroughNonOverflowingSignedAddNegative(x, y, z int64) {
  2184  	if x < math.MinInt64>>1 || x > 0 ||
  2185  		y < math.MinInt64>>1 || y > 0 {
  2186  		return
  2187  	}
  2188  
  2189  	a := x + y
  2190  	if a < z {
  2191  		return
  2192  	}
  2193  
  2194  	if x < z { // ERROR "Disproved Less64$"
  2195  		return
  2196  	}
  2197  	if y < z { // ERROR "Disproved Less64$"
  2198  		return
  2199  	}
  2200  	if a == x {
  2201  		return
  2202  	}
  2203  	if a == y {
  2204  		return
  2205  	}
  2206  
  2207  	if x == 0 && y == 0 {
  2208  		return
  2209  	}
  2210  	a = x + y
  2211  	if a == x { // ERROR "Disproved Eq64$"
  2212  		return
  2213  	}
  2214  	if a == y { // ERROR "Disproved Eq64$"
  2215  		return
  2216  	}
  2217  }
  2218  
  2219  func transitiveProofsThroughOverflowingSignedAddNegative(x, y, z int64) {
  2220  	if x >= 0 || y >= 0 {
  2221  		return
  2222  	}
  2223  
  2224  	a := x + y
  2225  	if a < z {
  2226  		return
  2227  	}
  2228  
  2229  	if x < z {
  2230  		return
  2231  	}
  2232  	if y < z {
  2233  		return
  2234  	}
  2235  	if a == x {
  2236  		return
  2237  	}
  2238  	if a == y {
  2239  		return
  2240  	}
  2241  
  2242  	x |= 1
  2243  	y |= 1
  2244  	a = x + y
  2245  	if a == x {
  2246  		return
  2247  	}
  2248  	if a == y {
  2249  		return
  2250  	}
  2251  }
  2252  
  2253  func transitiveProofsThroughNonOverflowingUnsignedSub(x, y, z uint64) {
  2254  	x |= 0xfff
  2255  	y &= 0xfff
  2256  
  2257  	a := x - y
  2258  	if a < z {
  2259  		return
  2260  	}
  2261  
  2262  	if x < z { // ERROR "Disproved Less64U$"
  2263  		return
  2264  	}
  2265  	if y < z {
  2266  		return
  2267  	}
  2268  	if a == x {
  2269  		return
  2270  	}
  2271  	if a == y {
  2272  		return
  2273  	}
  2274  
  2275  	y |= 1
  2276  	a = x - y
  2277  	if a == x { // ERROR "Disproved Eq64$"
  2278  		return
  2279  	}
  2280  	if a == y {
  2281  		return
  2282  	}
  2283  }
  2284  
  2285  func transitiveProofsThroughOverflowingUnsignedSub(x, y, z uint64) {
  2286  	a := x - y
  2287  	if a < z {
  2288  		return
  2289  	}
  2290  
  2291  	if x < z {
  2292  		return
  2293  	}
  2294  	if y < z {
  2295  		return
  2296  	}
  2297  	if a == x {
  2298  		return
  2299  	}
  2300  	if a == y {
  2301  		return
  2302  	}
  2303  
  2304  	y |= 1
  2305  	a = x - y
  2306  	if a == x {
  2307  		return
  2308  	}
  2309  	if a == y {
  2310  		return
  2311  	}
  2312  }
  2313  
  2314  func resliceString(s string) byte {
  2315  	if len(s) >= 4 {
  2316  		s = s[2:]   // ERROR "Proved IsSliceInBounds" "Proved slicemask not needed"
  2317  		s = s[1:]   // ERROR "Proved IsSliceInBounds" "Proved slicemask not needed"
  2318  		return s[0] // ERROR "Proved IsInBounds"
  2319  	}
  2320  	return 0
  2321  }
  2322  func resliceBytes(b []byte) byte {
  2323  	if len(b) >= 4 {
  2324  		b = b[2:]   // ERROR "Proved IsSliceInBounds" "Proved slicemask not needed"
  2325  		b = b[1:]   // ERROR "Proved IsSliceInBounds" "Proved slicemask not needed"
  2326  		return b[0] // ERROR "Proved IsInBounds"
  2327  	}
  2328  	return 0
  2329  }
  2330  
  2331  func issue74473(s []uint) {
  2332  	i := 0
  2333  	for {
  2334  		if i >= len(s) { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
  2335  			break
  2336  		}
  2337  		_ = s[i] // ERROR "Proved IsInBounds$"
  2338  		i++
  2339  	}
  2340  }
  2341  
  2342  func setCapMaxBasedOnElementSize(x []uint64) int {
  2343  	c := uintptr(cap(x))
  2344  	max := ^uintptr(0) >> 3
  2345  	if c > max { // ERROR "Disproved Less"
  2346  		return 42
  2347  	}
  2348  	if c <= max { // ERROR "Proved Leq"
  2349  		return 1337
  2350  	}
  2351  	return 0
  2352  }
  2353  
  2354  func issue75144for(a, b []uint64) bool {
  2355  	if len(a) == len(b) {
  2356  		for len(a) > 4 {
  2357  			a = a[4:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2358  			b = b[4:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2359  		}
  2360  		if len(a) == len(b) { // ERROR "Proved Eq64$"
  2361  			return true
  2362  		}
  2363  	}
  2364  	return false
  2365  }
  2366  
  2367  func issue75144if(a, b []uint64) bool {
  2368  	if len(a) == len(b) {
  2369  		if len(a) > 4 {
  2370  			a = a[4:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2371  			b = b[4:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2372  		}
  2373  		if len(a) == len(b) { // ERROR "Proved Eq64$"
  2374  			return true
  2375  		}
  2376  	}
  2377  	return false
  2378  }
  2379  
  2380  func issue75144if2(a, b, c, d []uint64) (r bool) {
  2381  	if len(a) != len(b) || len(c) != len(d) {
  2382  		return
  2383  	}
  2384  	if len(a) <= 4 || len(c) <= 4 {
  2385  		return
  2386  	}
  2387  	if len(a) < len(c) {
  2388  		c = c[4:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2389  		d = d[4:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2390  	} else {
  2391  		a = a[4:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2392  		b = b[4:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2393  	}
  2394  	if len(a) == len(c) {
  2395  		return
  2396  	}
  2397  	if len(a) == len(b) { // ERROR "Proved Eq64$"
  2398  		r = true
  2399  	}
  2400  	if len(c) == len(d) { // ERROR "Proved Eq64$"
  2401  		r = true
  2402  	}
  2403  	return
  2404  }
  2405  
  2406  func issue75144forCannot(a, b []uint64) bool {
  2407  	if len(a) == len(b) {
  2408  		for len(a) > 4 {
  2409  			a = a[4:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2410  			b = b[4:]
  2411  			for len(a) > 2 {
  2412  				a = a[2:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2413  				b = b[2:]
  2414  			}
  2415  		}
  2416  		if len(a) == len(b) {
  2417  			return true
  2418  		}
  2419  	}
  2420  	return false
  2421  }
  2422  
  2423  func issue75144ifCannot(a, b []uint64) bool {
  2424  	if len(a) == len(b) {
  2425  		if len(a) > 4 {
  2426  			a = a[4:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2427  			b = b[4:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2428  			if len(a) > 2 {
  2429  				a = a[2:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2430  				b = b[2:]
  2431  			}
  2432  		}
  2433  		if len(a) == len(b) {
  2434  			return true
  2435  		}
  2436  	}
  2437  	return false
  2438  }
  2439  
  2440  func issue75144ifCannot2(a, b []uint64) bool {
  2441  	if len(a) == len(b) {
  2442  		if len(a) > 4 {
  2443  			a = a[4:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2444  			b = b[4:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2445  		} else if len(a) > 2 {
  2446  			a = a[2:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2447  			b = b[2:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2448  		}
  2449  		if len(a) == len(b) {
  2450  			return true
  2451  		}
  2452  	}
  2453  	return false
  2454  }
  2455  
  2456  func issue75144forNot(a, b []uint64) bool {
  2457  	if len(a) == len(b) {
  2458  		for len(a) > 4 {
  2459  			a = a[4:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2460  			b = b[3:]
  2461  		}
  2462  		if len(a) == len(b) {
  2463  			return true
  2464  		}
  2465  	}
  2466  	return false
  2467  }
  2468  
  2469  func issue75144forNot2(a, b, c []uint64) bool {
  2470  	if len(a) == len(b) {
  2471  		for len(a) > 4 {
  2472  			a = a[4:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2473  			b = c[4:]
  2474  		}
  2475  		if len(a) == len(b) {
  2476  			return true
  2477  		}
  2478  	}
  2479  	return false
  2480  }
  2481  
  2482  func issue75144ifNot(a, b []uint64) bool {
  2483  	if len(a) == len(b) {
  2484  		if len(a) > 4 {
  2485  			a = a[4:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2486  		} else {
  2487  			b = b[4:]
  2488  		}
  2489  		if len(a) == len(b) {
  2490  			return true
  2491  		}
  2492  	}
  2493  	return false
  2494  }
  2495  
  2496  func mulIntoAnd(a, b uint) uint {
  2497  	if a > 1 || b > 1 {
  2498  		return 0
  2499  	}
  2500  	return a * b // ERROR "Rewrote Mul v[0-9]+ into And$"
  2501  }
  2502  
  2503  func mulIntoCondSelect(a, b uint) uint {
  2504  	if a > 1 {
  2505  		return 0
  2506  	}
  2507  	return a * b // ERROR "Rewrote Mul v[0-9]+ into CondSelect"
  2508  }
  2509  
  2510  func div7pos(x int32) bool {
  2511  	if x > 0 {
  2512  		return x%7 == 0 // ERROR "Proved Div32 is unsigned"
  2513  	}
  2514  	return false
  2515  }
  2516  
  2517  func div2pos(x []int) int {
  2518  	return len(x) / 2 // ERROR "Proved Div64 is unsigned"
  2519  }
  2520  
  2521  func div3pos(x []int) int {
  2522  	return len(x) / 3 // ERROR "Proved Div64 is unsigned"
  2523  }
  2524  
  2525  var len200 [200]int
  2526  
  2527  func modbound1(u uint64) int {
  2528  	s := 0
  2529  	for u > 0 {
  2530  		var d uint64
  2531  		u, d = u/100, u%100
  2532  		s += len200[d*2+1] // ERROR "Proved IsInBounds"
  2533  	}
  2534  	return s
  2535  }
  2536  
  2537  func modbound2(p *[10]int, x uint) int {
  2538  	return p[x%9+1] // ERROR "Proved IsInBounds"
  2539  }
  2540  
  2541  func shiftbound(x int) int {
  2542  	return 1 << (x % 11) // ERROR "Proved Lsh(32x32|64x64) bounded" "Proved Div64 does not need fix-up"
  2543  }
  2544  
  2545  func shiftbound2(x int) int {
  2546  	return 1 << (x % 8) // ERROR "Proved Lsh(32x32|64x64) bounded" "Proved Div64 does not need fix-up"
  2547  }
  2548  
  2549  func rangebound1(x []int) int {
  2550  	s := 0
  2551  	for i := range 1000 { // ERROR "Induction variable"
  2552  		if i < len(x) {
  2553  			s += x[i] // ERROR "Proved IsInBounds"
  2554  		}
  2555  	}
  2556  	return s
  2557  }
  2558  
  2559  func rangebound2(x []int) int {
  2560  	s := 0
  2561  	if len(x) > 0 {
  2562  		for i := range 1000 { // ERROR "Induction variable"
  2563  			s += x[i%len(x)] // ERROR "Proved Mod64 is unsigned" "Proved Neq64" "Proved IsInBounds"
  2564  		}
  2565  	}
  2566  	return s
  2567  }
  2568  
  2569  func swapbound(v []int) {
  2570  	for i := 0; i < len(v)/2; i++ { // ERROR "Proved Div64 is unsigned|Induction variable"
  2571  		v[i], // ERROR "Proved IsInBounds"
  2572  			v[len(v)-1-i] = // ERROR "Proved IsInBounds"
  2573  			v[len(v)-1-i],  // ERROR "Proved IsInBounds"
  2574  			v[i] // ERROR "Proved IsInBounds"
  2575  	}
  2576  }
  2577  
  2578  func rightshift(v *[256]int) int {
  2579  	for i := range 1024 { // ERROR "Induction"
  2580  		if v[i/32] == 0 { // ERROR "Proved Div64 is unsigned" "Proved IsInBounds"
  2581  			return i
  2582  		}
  2583  	}
  2584  	for i := range 1024 { // ERROR "Induction"
  2585  		if v[i>>2] == 0 { // ERROR "(Proved IsInBounds|Proved Rsh64x64 is unsigned)"
  2586  			return i
  2587  		}
  2588  	}
  2589  	return -1
  2590  }
  2591  
  2592  func rightShiftBounds(v, s int) {
  2593  	// The ignored "Proved" messages on the shift itself are about whether s >= 0 or s < 32 or 64.
  2594  	// We care about the bounds for x printed on the prove(x) lines.
  2595  
  2596  	if -8 <= v && v <= -2 && 1 <= s && s <= 3 {
  2597  		x := v >> s // ERROR "Proved"
  2598  		prove(x)    // ERROR "Proved sm,SM=-4,-1 "
  2599  	}
  2600  	if -80 <= v && v <= -20 && 1 <= s && s <= 3 {
  2601  		x := v >> s // ERROR "Proved"
  2602  		prove(x)    // ERROR "Proved sm,SM=-40,-3 "
  2603  	}
  2604  	if -8 <= v && v <= 10 && 1 <= s && s <= 3 {
  2605  		x := v >> s // ERROR "Proved"
  2606  		prove(x)    // ERROR "Proved sm,SM=-4,5 "
  2607  	}
  2608  	if 2 <= v && v <= 10 && 1 <= s && s <= 3 {
  2609  		x := v >> s // ERROR "Proved"
  2610  		prove(x)    // ERROR "Proved sm,SM=0,5 "
  2611  	}
  2612  
  2613  	if -8 <= v && v <= -2 && 0 <= s && s <= 3 {
  2614  		x := v >> s // ERROR "Proved"
  2615  		prove(x)    // ERROR "Proved sm,SM=-8,-1 "
  2616  	}
  2617  	if -80 <= v && v <= -20 && 0 <= s && s <= 3 {
  2618  		x := v >> s // ERROR "Proved"
  2619  		prove(x)    // ERROR "Proved sm,SM=-80,-3 "
  2620  	}
  2621  	if -8 <= v && v <= 10 && 0 <= s && s <= 3 {
  2622  		x := v >> s // ERROR "Proved"
  2623  		prove(x)    // ERROR "Proved sm,SM=-8,10 "
  2624  	}
  2625  	if 2 <= v && v <= 10 && 0 <= s && s <= 3 {
  2626  		x := v >> s // ERROR "Proved"
  2627  		prove(x)    // ERROR "Proved sm,SM=0,10 "
  2628  	}
  2629  
  2630  	if -8 <= v && v <= -2 && -1 <= s && s <= 3 {
  2631  		x := v >> s // ERROR "Proved"
  2632  		prove(x)    // ERROR "Proved sm,SM=-8,-1 "
  2633  	}
  2634  	if -80 <= v && v <= -20 && -1 <= s && s <= 3 {
  2635  		x := v >> s // ERROR "Proved"
  2636  		prove(x)    // ERROR "Proved sm,SM=-80,-3 "
  2637  	}
  2638  	if -8 <= v && v <= 10 && -1 <= s && s <= 3 {
  2639  		x := v >> s // ERROR "Proved"
  2640  		prove(x)    // ERROR "Proved sm,SM=-8,10 "
  2641  	}
  2642  	if 2 <= v && v <= 10 && -1 <= s && s <= 3 {
  2643  		x := v >> s // ERROR "Proved"
  2644  		prove(x)    // ERROR "Proved sm,SM=0,10 "
  2645  	}
  2646  }
  2647  
  2648  func unsignedRightShiftBounds(v uint, s int) {
  2649  	if 2 <= v && v <= 10 && -1 <= s && s <= 3 {
  2650  		x := v >> s // ERROR "Proved"
  2651  		proveu(x)   // ERROR "Proved sm,SM=0,10 "
  2652  	}
  2653  	if 2 <= v && v <= 10 && 0 <= s && s <= 3 {
  2654  		x := v >> s // ERROR "Proved"
  2655  		proveu(x)   // ERROR "Proved sm,SM=0,10 "
  2656  	}
  2657  	if 2 <= v && v <= 10 && 1 <= s && s <= 3 {
  2658  		x := v >> s // ERROR "Proved"
  2659  		proveu(x)   // ERROR "Proved sm,SM=0,5 "
  2660  	}
  2661  	if 20 <= v && v <= 100 && 1 <= s && s <= 3 {
  2662  		x := v >> s // ERROR "Proved"
  2663  		proveu(x)   // ERROR "Proved sm,SM=2,50 "
  2664  	}
  2665  }
  2666  
  2667  func subLengths1(b []byte, i int) {
  2668  	if i >= 0 && i <= len(b) {
  2669  		_ = b[len(b)-i:] // ERROR "Proved IsSliceInBounds"
  2670  	}
  2671  }
  2672  
  2673  func subLengths2(b []byte, i int) {
  2674  	if i >= 0 && i <= len(b) {
  2675  		_ = b[:len(b)-i] // ERROR "Proved IsSliceInBounds"
  2676  	}
  2677  }
  2678  
  2679  func issue76355(s []int, i int) int {
  2680  	var a [10]int
  2681  	if i <= len(s)-1 {
  2682  		v := len(s) - i
  2683  		if v < 10 {
  2684  			return a[v]
  2685  		}
  2686  	}
  2687  	return 0
  2688  }
  2689  
  2690  func stringDotDotDot(s string) bool {
  2691  	for i := 0; i < len(s)-2; i++ { // ERROR "Induction variable: limits \[0,[?][)], increment 1"
  2692  		if s[i] == '.' && // ERROR "Proved IsInBounds"
  2693  			s[i+1] == '.' && // ERROR "Proved IsInBounds"
  2694  			s[i+2] == '.' { // ERROR "Proved IsInBounds"
  2695  			return true
  2696  		}
  2697  	}
  2698  	return false
  2699  }
  2700  
  2701  func bytesDotDotDot(s []byte) bool {
  2702  	for i := 0; i < len(s)-2; i++ { // ERROR "Induction variable"
  2703  		if s[i] == '.' && // ERROR "Proved IsInBounds"
  2704  			s[i+1] == '.' && // ERROR "Proved IsInBounds"
  2705  			s[i+2] == '.' { // ERROR "Proved IsInBounds"
  2706  			return true
  2707  		}
  2708  	}
  2709  	return false
  2710  }
  2711  
  2712  // detectSliceLenRelation matches the pattern where
  2713  //  1. v := slicelen - index, OR v := slicecap - index
  2714  //     AND
  2715  //  2. index <= slicelen - K
  2716  //     THEN
  2717  //
  2718  // slicecap - index >= slicelen - index >= K
  2719  func detectSliceLenRelation(s []byte) bool {
  2720  	for i := 0; i <= len(s)-3; i++ { // ERROR "Induction variable"
  2721  		v := len(s) - i
  2722  		if v >= 3 { // ERROR "Proved Leq"
  2723  			return true
  2724  		}
  2725  	}
  2726  	return false
  2727  }
  2728  
  2729  func detectStringLenRelation(s string) bool {
  2730  	for i := 0; i <= len(s)-3; i++ { // ERROR "Induction variable"
  2731  		v := len(s) - i
  2732  		if v >= 3 { // ERROR "Proved Leq"
  2733  			return true
  2734  		}
  2735  	}
  2736  	return false
  2737  }
  2738  
  2739  func issue76688(x, y uint64) uint64 {
  2740  	if x > 1 || y != 1<<63 {
  2741  		return 42
  2742  	}
  2743  	// We do not want to rewrite the multiply to a condselect here since opt can do a better job with a left shift.
  2744  	return x * y
  2745  }
  2746  
  2747  func issue76429(s []byte, k int) byte {
  2748  	if k < 0 || k >= len(s) {
  2749  		return 0
  2750  	}
  2751  	s = s[k:]   // ERROR "Proved IsSliceInBounds" "Proved slicemask not needed"
  2752  	return s[0] // ERROR "Proved IsInBounds"
  2753  }
  2754  
  2755  //go:noinline
  2756  func prove(x int) {
  2757  }
  2758  
  2759  //go:noinline
  2760  func proveu(x uint) {
  2761  }
  2762  
  2763  //go:noinline
  2764  func useInt(a int) {
  2765  }
  2766  
  2767  //go:noinline
  2768  func useSlice(a []int) {
  2769  }
  2770  
  2771  func main() {
  2772  }
  2773  

View as plain text