summaryrefslogtreecommitdiff
path: root/Test/test0/BadLabels0.bpl
blob: ec6ff744afc0daf77fcccda7b273e683d41fc56c (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
// RUN: %boogie -noVerify %s > %t
// RUN: %diff %s.expect %t
procedure Dup(y: int)
{
  X:
  X:  // error: duplicate label
  while (y < 100)
  {
    Y:
  }
  while (y < 1000)
  {
    Y:  // error: duplicate label (labels must be unique in entire procedure body)
  }
}