...
Run Format

Source file test/loopbce.go

Documentation: test

     1  // +build amd64
     2  // errorcheck -0 -d=ssa/prove/debug=1
     3  
     4  package main
     5  
     6  func f0a(a []int) int {
     7  	x := 0
     8  	for i := range a { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
     9  		x += a[i] // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
    10  	}
    11  	return x
    12  }
    13  
    14  func f0b(a []int) int {
    15  	x := 0
    16  	for i := range a { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
    17  		b := a[i:] // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
    18  		x += b[0]
    19  	}
    20  	return x
    21  }
    22  
    23  func f0c(a []int) int {
    24  	x := 0
    25  	for i := range a { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
    26  		b := a[:i+1] // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
    27  		x += b[0]
    28  	}
    29  	return x
    30  }
    31  
    32  func f1(a []int) int {
    33  	x := 0
    34  	for _, i := range a { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
    35  		x += i
    36  	}
    37  	return x
    38  }
    39  
    40  func f2(a []int) int {
    41  	x := 0
    42  	for i := 1; i < len(a); i++ { // ERROR "Induction variable: limits \[1,\?\), increment 1$"
    43  		x += a[i] // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
    44  	}
    45  	return x
    46  }
    47  
    48  func f4(a [10]int) int {
    49  	x := 0
    50  	for i := 0; i < len(a); i += 2 { // ERROR "Induction variable: limits \[0,10\), increment 2$"
    51  		x += a[i] // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
    52  	}
    53  	return x
    54  }
    55  
    56  func f5(a [10]int) int {
    57  	x := 0
    58  	for i := -10; i < len(a); i += 2 { // ERROR "Induction variable: limits \[-10,10\), increment 2$"
    59  		x += a[i]
    60  	}
    61  	return x
    62  }
    63  
    64  func f6(a []int) {
    65  	for i := range a { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
    66  		b := a[0:i] // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$" "(\([0-9]+\) )?Proved Geq64$"
    67  		f6(b)
    68  	}
    69  }
    70  
    71  func g0a(a string) int {
    72  	x := 0
    73  	for i := 0; i < len(a); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
    74  		x += int(a[i]) // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
    75  	}
    76  	return x
    77  }
    78  
    79  func g0b(a string) int {
    80  	x := 0
    81  	for i := 0; len(a) > i; i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
    82  		x += int(a[i]) // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
    83  	}
    84  	return x
    85  }
    86  
    87  func g0c(a string) int {
    88  	x := 0
    89  	for i := len(a); i > 0; i-- { // ERROR "Induction variable: limits \(0,\?\], increment 1$"
    90  		x += int(a[i-1]) // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
    91  	}
    92  	return x
    93  }
    94  
    95  func g0d(a string) int {
    96  	x := 0
    97  	for i := len(a); 0 < i; i-- { // ERROR "Induction variable: limits \(0,\?\], increment 1$"
    98  		x += int(a[i-1]) // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
    99  	}
   100  	return x
   101  }
   102  
   103  func g0e(a string) int {
   104  	x := 0
   105  	for i := len(a) - 1; i >= 0; i-- { // ERROR "Induction variable: limits \[0,\?\], increment 1$"
   106  		x += int(a[i]) // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
   107  	}
   108  	return x
   109  }
   110  
   111  func g0f(a string) int {
   112  	x := 0
   113  	for i := len(a) - 1; 0 <= i; i-- { // ERROR "Induction variable: limits \[0,\?\], increment 1$"
   114  		x += int(a[i]) // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
   115  	}
   116  	return x
   117  }
   118  
   119  func g1() int {
   120  	a := "evenlength"
   121  	x := 0
   122  	for i := 0; i < len(a); i += 2 { // ERROR "Induction variable: limits \[0,10\), increment 2$"
   123  		x += int(a[i]) // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
   124  	}
   125  	return x
   126  }
   127  
   128  func g2() int {
   129  	a := "evenlength"
   130  	x := 0
   131  	for i := 0; i < len(a); i += 2 { // ERROR "Induction variable: limits \[0,10\), increment 2$"
   132  		j := i
   133  		if a[i] == 'e' { // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
   134  			j = j + 1
   135  		}
   136  		x += int(a[j])
   137  	}
   138  	return x
   139  }
   140  
   141  func g3a() {
   142  	a := "this string has length 25"
   143  	for i := 0; i < len(a); i += 5 { // ERROR "Induction variable: limits \[0,25\), increment 5$"
   144  		useString(a[i:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   145  		useString(a[:i+3])
   146  	}
   147  }
   148  
   149  func g3b(a string) {
   150  	for i := 0; i < len(a); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
   151  		useString(a[i+1:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   152  	}
   153  }
   154  
   155  func g3c(a string) {
   156  	for i := 0; i < len(a); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
   157  		useString(a[:i+1]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   158  	}
   159  }
   160  
   161  func h1(a []byte) {
   162  	c := a[:128]
   163  	for i := range c { // ERROR "Induction variable: limits \[0,128\), increment 1$"
   164  		c[i] = byte(i) // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
   165  	}
   166  }
   167  
   168  func h2(a []byte) {
   169  	for i := range a[:128] { // ERROR "Induction variable: limits \[0,128\), increment 1$"
   170  		a[i] = byte(i)
   171  	}
   172  }
   173  
   174  func k0(a [100]int) [100]int {
   175  	for i := 10; i < 90; i++ { // ERROR "Induction variable: limits \[10,90\), increment 1$"
   176  		a[i-11] = i
   177  		a[i-10] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
   178  		a[i-5] = i  // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
   179  		a[i] = i    // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
   180  		a[i+5] = i  // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
   181  		a[i+10] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
   182  		a[i+11] = i
   183  	}
   184  	return a
   185  }
   186  
   187  func k1(a [100]int) [100]int {
   188  	for i := 10; i < 90; i++ { // ERROR "Induction variable: limits \[10,90\), increment 1$"
   189  		useSlice(a[:i-11]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   190  		useSlice(a[:i-10]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   191  		useSlice(a[:i-5])  // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   192  		useSlice(a[:i])    // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$" "(\([0-9]+\) )?Proved Geq64$"
   193  		useSlice(a[:i+5])  // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   194  		useSlice(a[:i+10]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   195  		useSlice(a[:i+11]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   196  		useSlice(a[:i+12])
   197  
   198  	}
   199  	return a
   200  }
   201  
   202  func k2(a [100]int) [100]int {
   203  	for i := 10; i < 90; i++ { // ERROR "Induction variable: limits \[10,90\), increment 1$"
   204  		useSlice(a[i-11:])
   205  		useSlice(a[i-10:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   206  		useSlice(a[i-5:])  // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   207  		useSlice(a[i:])    // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   208  		useSlice(a[i+5:])  // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   209  		useSlice(a[i+10:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   210  		useSlice(a[i+11:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   211  		useSlice(a[i+12:])
   212  	}
   213  	return a
   214  }
   215  
   216  func k3(a [100]int) [100]int {
   217  	for i := -10; i < 90; i++ { // ERROR "Induction variable: limits \[-10,90\), increment 1$"
   218  		a[i+9] = i
   219  		a[i+10] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
   220  		a[i+11] = i
   221  	}
   222  	return a
   223  }
   224  
   225  func k3neg(a [100]int) [100]int {
   226  	for i := 89; i > -11; i-- { // ERROR "Induction variable: limits \(-11,89\], increment 1$"
   227  		a[i+9] = i
   228  		a[i+10] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
   229  		a[i+11] = i
   230  	}
   231  	return a
   232  }
   233  
   234  func k3neg2(a [100]int) [100]int {
   235  	for i := 89; i >= -10; i-- { // ERROR "Induction variable: limits \[-10,89\], increment 1$"
   236  		a[i+9] = i
   237  		a[i+10] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
   238  		a[i+11] = i
   239  	}
   240  	return a
   241  }
   242  
   243  func k4(a [100]int) [100]int {
   244  	min := (-1) << 63
   245  	for i := min; i < min+50; i++ { // ERROR "Induction variable: limits \[-9223372036854775808,-9223372036854775758\), increment 1$"
   246  		a[i-min] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
   247  	}
   248  	return a
   249  }
   250  
   251  func k5(a [100]int) [100]int {
   252  	max := (1 << 63) - 1
   253  	for i := max - 50; i < max; i++ { // ERROR "Induction variable: limits \[9223372036854775757,9223372036854775807\), increment 1$"
   254  		a[i-max+50] = i   // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
   255  		a[i-(max-70)] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
   256  	}
   257  	return a
   258  }
   259  
   260  func nobce1() {
   261  	// tests overflow of max-min
   262  	a := int64(9223372036854774057)
   263  	b := int64(-1547)
   264  	z := int64(1337)
   265  
   266  	if a%z == b%z {
   267  		panic("invalid test: modulos should differ")
   268  	}
   269  
   270  	for i := b; i < a; i += z {
   271  		// No induction variable is possible because i will overflow a first iteration.
   272  		useString("foobar")
   273  	}
   274  }
   275  
   276  func nobce2(a string) {
   277  	for i := int64(0); i < int64(len(a)); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
   278  		useString(a[i:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   279  	}
   280  	for i := int64(0); i < int64(len(a))-31337; i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
   281  		useString(a[i:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   282  	}
   283  	for i := int64(0); i < int64(len(a))+int64(-1<<63); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
   284  		useString(a[i:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   285  	}
   286  	j := int64(len(a)) - 123
   287  	for i := int64(0); i < j+123+int64(-1<<63); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
   288  		useString(a[i:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   289  	}
   290  	for i := int64(0); i < j+122+int64(-1<<63); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
   291  		// len(a)-123+122+MinInt overflows when len(a) == 0, so a bound check is needed here
   292  		useString(a[i:])
   293  	}
   294  }
   295  
   296  func nobce3(a [100]int64) [100]int64 {
   297  	min := int64((-1) << 63)
   298  	max := int64((1 << 63) - 1)
   299  	for i := min; i < max; i++ { // ERROR "Induction variable: limits \[-9223372036854775808,9223372036854775807\), increment 1$"
   300  		a[i] = i
   301  	}
   302  	return a
   303  }
   304  
   305  func issue26116a(a []int) {
   306  	// There is no induction variable here. The comparison is in the wrong direction.
   307  	for i := 3; i > 6; i++ {
   308  		a[i] = 0
   309  	}
   310  	for i := 7; i < 3; i-- {
   311  		a[i] = 1
   312  	}
   313  }
   314  
   315  //go:noinline
   316  func useString(a string) {
   317  }
   318  
   319  //go:noinline
   320  func useSlice(a []int) {
   321  }
   322  
   323  func main() {
   324  }
   325  

View as plain text