diff options
author | qunyanm <unknown> | 2016-02-26 16:50:38 -0800 |
---|---|---|
committer | qunyanm <unknown> | 2016-02-26 16:50:38 -0800 |
commit | c558eecdcd6444919c0314043c0f328c85ca3b22 (patch) | |
tree | 2c11ac97b45b26e4e6ccf8e4f9f6d5068f999ff4 | |
parent | 0531b8772f4174d807caecc356ecaa41adca8c8c (diff) |
Fix issue 139. Allow bound variables in nested case patterns to shadow variables
declared outside the enclosing match.
-rw-r--r-- | Source/Dafny/Resolver.cs | 12 | ||||
-rw-r--r-- | Test/dafny4/Bug139.dfy | 25 | ||||
-rw-r--r-- | Test/dafny4/Bug139.dfy.expect | 2 |
3 files changed, 38 insertions, 1 deletions
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 5a63b4e3..d3b59b51 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -6376,7 +6376,12 @@ namespace Microsoft.Dafny if (topLevel) {
ScopePushAndReport(scope, v, "parameter");
} else {
- if (scope.Find(v.Name) != null) {
+ // For cons(a, const(b, c)):
+ // this handles check to see if 'b' or 'c' is duplicate with 'a',
+ // the duplication check between 'b' and 'c' is handled in the desugared
+ // form (to avoid reporting the same error twice), that is why we don't
+ // push 'b' and 'c' onto the scope, only find.
+ if (scope.FindInCurrentScope(v.Name) != null) {
reporter.Error(MessageSource.Resolver, v, "Duplicate parameter name: {0}", v.Name);
}
}
@@ -11069,6 +11074,11 @@ namespace Microsoft.Dafny return Find(name, false);
}
+ public Thing FindInCurrentScope(string name) {
+ Contract.Requires(name != null);
+ return Find(name, true);
+ }
+
public bool ContainsDecl(Thing t) {
return things.Exists(thing => thing == t);
}
diff --git a/Test/dafny4/Bug139.dfy b/Test/dafny4/Bug139.dfy new file mode 100644 index 00000000..bd4ded73 --- /dev/null +++ b/Test/dafny4/Bug139.dfy @@ -0,0 +1,25 @@ +// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+datatype List = Nil | Cons(int, List)
+
+method R(xs: List)
+{
+ var a: int;
+ var b: int;
+ match xs
+ case Nil =>
+ case Cons(a, Nil()) => // this 'a' is allowed
+ case Cons(x, Cons(b, tail)) => // this 'b' (which is in a nested position) generates an error
+}
+
+function F(xs: List): int
+{
+ var a := 4;
+ var b := 7;
+ match xs
+ case Nil => 0
+ case Cons(a, Nil()) => 1
+ case Cons(x, Cons(b, tail)) => 2
+}
+
diff --git a/Test/dafny4/Bug139.dfy.expect b/Test/dafny4/Bug139.dfy.expect new file mode 100644 index 00000000..52595bf9 --- /dev/null +++ b/Test/dafny4/Bug139.dfy.expect @@ -0,0 +1,2 @@ +
+Dafny program verifier finished with 3 verified, 0 errors
|