summaryrefslogtreecommitdiff
path: root/Test/test0/BadLabels0.bpl
diff options
context:
space:
mode:
Diffstat (limited to 'Test/test0/BadLabels0.bpl')
-rw-r--r--Test/test0/BadLabels0.bpl30
1 files changed, 15 insertions, 15 deletions
diff --git a/Test/test0/BadLabels0.bpl b/Test/test0/BadLabels0.bpl
index b3f6f896..6b02a2d1 100644
--- a/Test/test0/BadLabels0.bpl
+++ b/Test/test0/BadLabels0.bpl
@@ -1,15 +1,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)
- }
-}
+// 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)
+ }
+}