test/prove.go

   1 // +build amd64
   2 // errorcheck -0 -d=ssa/prove/debug=3
   3
   4 package main
   5
   6 import "math"
   7
   8 func f0(a []int) int {
   9         a[0] = 1
  10         a[0] = 1 // ERROR "Proved boolean IsInBounds$"
  11         a[6] = 1
  12         a[6] = 1 // ERROR "Proved boolean IsInBounds$"
  13         a[5] = 1 // ERROR "Proved IsInBounds$"
  14         a[5] = 1 // ERROR "Proved boolean IsInBounds$"
  15         return 13
  16 }
  17
  18 func f1(a []int) int {
  19         if len(a) <= 5 {
  20                 return 18
  21         }
  22         a[0] = 1 // ERROR "Proved non-negative bounds IsInBounds$"
  23         a[0] = 1 // ERROR "Proved boolean IsInBounds$"
  24         a[6] = 1
  25         a[6] = 1 // ERROR "Proved boolean IsInBounds$"
  26         a[5] = 1 // ERROR "Proved IsInBounds$"
  27         a[5] = 1 // ERROR "Proved boolean IsInBounds$"
  28         return 26
  29 }
  30
  31 func f1b(a []int, i int, j uint) int {
  32         if i >= 0 && i < len(a) { // TODO: handle this case
  33                 return a[i]
  34         }
  35         if j < uint(len(a)) {
  36                 return a[j] // ERROR "Proved IsInBounds"
  37         }
  38         return 0
  39 }
  40
  41 func f2(a []int) int {
  42         for i := range a {
  43                 a[i+1] = i
  44                 a[i+1] = i // ERROR "Proved boolean IsInBounds$"
  45         }
  46         return 34
  47 }
  48
  49 func f3(a []uint) int {
  50         for i := uint(0); i < uint(len(a)); i++ {
  51                 a[i] = i // ERROR "Proved IsInBounds$"
  52         }
  53         return 41
  54 }
  55
  56 func f4a(a, b, c int) int {
  57         if a < b {
  58                 if a == b { // ERROR "Disproved Eq64$"
  59                         return 47
  60                 }
  61                 if a > b { // ERROR "Disproved Greater64$"
  62                         return 50
  63                 }
  64                 if a < b { // ERROR "Proved boolean Less64$"
  65                         return 53
  66                 }
  67                 if a == b { // ERROR "Disproved boolean Eq64$"
  68                         return 56
  69                 }
  70                 if a > b { // ERROR "Disproved boolean Greater64$"
  71                         return 59
  72                 }
  73                 return 61
  74         }
  75         return 63
  76 }
  77
  78 func f4b(a, b, c int) int {
  79         if a <= b {
  80                 if a >= b {
  81                         if a == b { // ERROR "Proved Eq64$"
  82                                 return 70
  83                         }
  84                         return 75
  85                 }
  86                 return 77
  87         }
  88         return 79
  89 }
  90
  91 func f4c(a, b, c int) int {
  92         if a <= b {
  93                 if a >= b {
  94                         if a != b { // ERROR "Disproved Neq64$"
  95                                 return 73
  96                         }
  97                         return 75
  98                 }
  99                 return 77
 100         }
 101         return 79
 102 }
 103
 104 func f4d(a, b, c int) int {
 105         if a < b {
 106                 if a < c {
 107                         if a < b { // ERROR "Proved boolean Less64$"
 108                                 if a < c { // ERROR "Proved boolean Less64$"
 109                                         return 87
 110                                 }
 111                                 return 89
 112                         }
 113                         return 91
 114                 }
 115                 return 93
 116         }
 117         return 95
 118 }
 119
 120 func f4e(a, b, c int) int {
 121         if a < b {
 122                 if b > a { // ERROR "Proved Greater64$"
 123                         return 101
 124                 }
 125                 return 103
 126         }
 127         return 105
 128 }
 129
 130 func f4f(a, b, c int) int {
 131         if a <= b {
 132                 if b > a {
 133                         if b == a { // ERROR "Disproved Eq64$"
 134                                 return 112
 135                         }
 136                         return 114
 137                 }
 138                 if b >= a { // ERROR "Proved Geq64$"
 139                         if b == a { // ERROR "Proved Eq64$"
 140                                 return 118
 141                         }
 142                         return 120
 143                 }
 144                 return 122
 145         }
 146         return 124
 147 }
 148
 149 func f5(a, b uint) int {
 150         if a == b {
 151                 if a <= b { // ERROR "Proved Leq64U$"
 152                         return 130
 153                 }
 154                 return 132
 155         }
 156         return 134
 157 }
 158
 159 // These comparisons are compile time constants.
 160 func f6a(a uint8) int {
 161         if a < a { // ERROR "Disproved Less8U$"
 162                 return 140
 163         }
 164         return 151
 165 }
 166
 167 func f6b(a uint8) int {
 168         if a < a { // ERROR "Disproved Less8U$"
 169                 return 140
 170         }
 171         return 151
 172 }
 173
 174 func f6x(a uint8) int {
 175         if a > a { // ERROR "Disproved Greater8U$"
 176                 return 143
 177         }
 178         return 151
 179 }
 180
 181 func f6d(a uint8) int {
 182         if a <= a { // ERROR "Proved Leq8U$"
 183                 return 146
 184         }
 185         return 151
 186 }
 187
 188 func f6e(a uint8) int {
 189         if a >= a { // ERROR "Proved Geq8U$"
 190                 return 149
 191         }
 192         return 151
 193 }
 194
 195 func f7(a []int, b int) int {
 196         if b < len(a) {
 197                 a[b] = 3
 198                 if b < len(a) { // ERROR "Proved boolean Less64$"
 199                         a[b] = 5 // ERROR "Proved boolean IsInBounds$"
 200                 }
 201         }
 202         return 161
 203 }
 204
 205 func f8(a, b uint) int {
 206         if a == b {
 207                 return 166
 208         }
 209         if a > b {
 210                 return 169
 211         }
 212         if a < b { // ERROR "Proved Less64U$"
 213                 return 172
 214         }
 215         return 174
 216 }
 217
 218 func f9(a, b bool) int {
 219         if a {
 220                 return 1
 221         }
 222         if a || b { // ERROR "Disproved boolean Arg$"
 223                 return 2
 224         }
 225         return 3
 226 }
 227
 228 func f10(a string) int {
 229         n := len(a)
 230         if a[:n>>1] == "aaa" {
 231                 return 0
 232         }
 233         return 1
 234 }
 235
 236 func f11a(a []int, i int) {
 237         useInt(a[i])
 238         useInt(a[i]) // ERROR "Proved boolean IsInBounds$"
 239 }
 240
 241 func f11b(a []int, i int) {
 242         useSlice(a[i:])
 243         useSlice(a[i:]) // ERROR "Proved boolean IsSliceInBounds$"
 244 }
 245
 246 func f11c(a []int, i int) {
 247         useSlice(a[:i])
 248         useSlice(a[:i]) // ERROR "Proved boolean IsSliceInBounds$"
 249 }
 250
 251 func f11d(a []int, i int) {
 252         useInt(a[2*i+7])
 253         useInt(a[2*i+7])
 254 }
 255
 256 func f12(a []int, b int) {
 257         useSlice(a[:b])
 258 }
 259
 260 func f13a(a, b, c int, x bool) int {
 261         if a > 12 {
 262                 if x {
 263                         if a < 12 { // ERROR "Disproved Less64$"
 264                                 return 1
 265                         }
 266                 }
 267                 if x {
 268                         if a <= 12 { // ERROR "Disproved Leq64$"
 269                                 return 2
 270                         }
 271                 }
 272                 if x {
 273                         if a == 12 { // ERROR "Disproved Eq64$"
 274                                 return 3
 275                         }
 276                 }
 277                 if x {
 278                         if a >= 12 { // ERROR "Proved Geq64$"
 279                                 return 4
 280                         }
 281                 }
 282                 if x {
 283                         if a > 12 { // ERROR "Proved boolean Greater64$"
 284                                 return 5
 285                         }
 286                 }
 287                 return 6
 288         }
 289         return 0
 290 }
 291
 292 func f13b(a int, x bool) int {
 293         if a == -9 {
 294                 if x {
 295                         if a < -9 { // ERROR "Disproved Less64$"
 296                                 return 7
 297                         }
 298                 }
 299                 if x {
 300                         if a <= -9 { // ERROR "Proved Leq64$"
 301                                 return 8
 302                         }
 303                 }
 304                 if x {
 305                         if a == -9 { // ERROR "Proved boolean Eq64$"
 306                                 return 9
 307                         }
 308                 }
 309                 if x {
 310                         if a >= -9 { // ERROR "Proved Geq64$"
 311                                 return 10
 312                         }
 313                 }
 314                 if x {
 315                         if a > -9 { // ERROR "Disproved Greater64$"
 316                                 return 11
 317                         }
 318                 }
 319                 return 12
 320         }
 321         return 0
 322 }
 323
 324 func f13c(a int, x bool) int {
 325         if a < 90 {
 326                 if x {
 327                         if a < 90 { // ERROR "Proved boolean Less64$"
 328                                 return 13
 329                         }
 330                 }
 331                 if x {
 332                         if a <= 90 { // ERROR "Proved Leq64$"
 333                                 return 14
 334                         }
 335                 }
 336                 if x {
 337                         if a == 90 { // ERROR "Disproved Eq64$"
 338                                 return 15
 339                         }
 340                 }
 341                 if x {
 342                         if a >= 90 { // ERROR "Disproved Geq64$"
 343                                 return 16
 344                         }
 345                 }
 346                 if x {
 347                         if a > 90 { // ERROR "Disproved Greater64$"
 348                                 return 17
 349                         }
 350                 }
 351                 return 18
 352         }
 353         return 0
 354 }
 355
 356 func f13d(a int) int {
 357         if a < 5 {
 358                 if a < 9 { // ERROR "Proved Less64$"
 359                         return 1
 360                 }
 361         }
 362         return 0
 363 }
 364
 365 func f13e(a int) int {
 366         if a > 9 {
 367                 if a > 5 { // ERROR "Proved Greater64$"
 368                         return 1
 369                 }
 370         }
 371         return 0
 372 }
 373
 374 func f13f(a int64) int64 {
 375         if a > math.MaxInt64 {
 376                 // Unreachable, but prove doesn't know that.
 377                 if a == 0 {
 378                         return 1
 379                 }
 380         }
 381         return 0
 382 }
 383
 384 func f13g(a int) int {
 385         if a < 3 {
 386                 return 5
 387         }
 388         if a > 3 {
 389                 return 6
 390         }
 391         if a == 3 { // ERROR "Proved Eq64$"
 392                 return 7
 393         }
 394         return 8
 395 }
 396
 397 func f13h(a int) int {
 398         if a < 3 {
 399                 if a > 1 {
 400                         if a == 2 { // ERROR "Proved Eq64$"
 401                                 return 5
 402                         }
 403                 }
 404         }
 405         return 0
 406 }
 407
 408 func f13i(a uint) int {
 409         if a == 0 {
 410                 return 1
 411         }
 412         if a > 0 { // ERROR "Proved Greater64U$"
 413                 return 2
 414         }
 415         return 3
 416 }
 417
 418 //go:noinline
 419 func useInt(a int) {
 420 }
 421
 422 //go:noinline
 423 func useSlice(a []int) {
 424 }
 425
 426 func main() {
 427 }