summaryrefslogtreecommitdiff
path: root/Test/test0/BadLabels0.bpl
blob: b3f6f89601e7060e9d8e82d889b4847e1a60f4f3 (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)
  }
}