From 4d11b8d19bab3c4b37914f12226e19ac6d68ffb1 Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Thu, 2 Jul 2015 20:00:11 -0700
Subject: Added command-line option /warnShadowing, which emits warnings if
 variables shadow other variables (Issue #86)

---
 Test/dafny0/Shadows.dfy | 42 ++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 42 insertions(+)
 create mode 100644 Test/dafny0/Shadows.dfy

(limited to 'Test/dafny0/Shadows.dfy')

diff --git a/Test/dafny0/Shadows.dfy b/Test/dafny0/Shadows.dfy
new file mode 100644
index 00000000..da1e74d6
--- /dev/null
+++ b/Test/dafny0/Shadows.dfy
@@ -0,0 +1,42 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /warnShadowing "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+module Module0 {
+  class C<alpha> {
+    method M<beta, beta>(x: beta)  // error: duplicate type parameter
+    method P<alpha>(x: alpha)  // shadowed type parameter
+    function F<beta, beta>(x: beta): int  // error: duplicate type parameter
+    function G<alpha>(x: alpha): int  // shadowed type parameter
+
+    method Q0(x: int) returns (x: int)  // error: duplicate variable name
+  }
+}
+module Module1 {
+  class D {
+    method Q1(x: int) returns (y: int)
+    {
+      var x;  // shadowed
+      var y;  // error: duplicate
+    }
+
+    var f: int
+    method R()
+    {
+      var f;  // okay
+      var f;  // error: duplicate
+    }
+    method S()
+    {
+      var x;
+      {
+        var x;  // shadow
+      }
+    }
+    method T()
+    {
+      var x;
+      ghost var b := forall x :: x < 10;  // shadow
+      ghost var c := forall y :: forall y :: y != y + 1;  // shadow
+    }
+  }
+}
-- 
cgit v1.2.3