summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Rustan Leino <unknown>2016-03-01 15:38:18 -0800
committerGravatar Rustan Leino <unknown>2016-03-01 15:38:18 -0800
commit2144154dc66b8d83792dd4395d3059c97d044e01 (patch)
tree2b6a64475391309a24fecf839c77379b06fea023
parent1f38d2d252aaac3d55191e6c3dad46ecffdfee2c (diff)
parent45e7bb72d4a8676796cb71cd8d11787dd6f91e17 (diff)
Merge
-rw-r--r--Source/Dafny/Resolver.cs12
-rw-r--r--Source/DafnyExtension/ResolverTagger.cs38
-rw-r--r--Test/dafny4/Bug139.dfy25
-rw-r--r--Test/dafny4/Bug139.dfy.expect2
4 files changed, 43 insertions, 34 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/Source/DafnyExtension/ResolverTagger.cs b/Source/DafnyExtension/ResolverTagger.cs
index b711c276..4a50a4e8 100644
--- a/Source/DafnyExtension/ResolverTagger.cs
+++ b/Source/DafnyExtension/ResolverTagger.cs
@@ -15,7 +15,6 @@ using System.Linq;
using System.Text.RegularExpressions;
using System.Windows.Shapes;
using Microsoft.VisualStudio;
-using System.Windows.Threading;
using Microsoft.VisualStudio.Shell;
using Microsoft.VisualStudio.Shell.Interop;
using Microsoft.VisualStudio.Text;
@@ -130,8 +129,6 @@ namespace DafnyLanguage
ErrorListProvider _errorProvider;
private bool m_disposed;
- readonly DispatcherTimer timer;
-
// The 'Snapshot' and 'Program' fields should be updated and read together, so they are protected by "this"
public ITextSnapshot Snapshot; // may be null
public Dafny.Program Program; // non-null only if the snapshot contains a Dafny program that type checks
@@ -230,13 +227,7 @@ namespace DafnyLanguage
Snapshot = null; // this makes sure the next snapshot will look different
_errorProvider = new ErrorListProvider(serviceProvider);
- BufferIdleEventUtil.AddBufferIdleEventListener(_buffer, UponIdle);
-
- // keep track idle time after BufferIdleEvent has been handled.
- timer = new DispatcherTimer(DispatcherPriority.ApplicationIdle);
- timer.Interval = TimeSpan.FromMilliseconds(5000);
- timer.Tick += new EventHandler(ResolveBuffer);
- buffer.Changed += BufferChanged;
+ BufferIdleEventUtil.AddBufferIdleEventListener(_buffer, ResolveBuffer);
}
public void Dispose()
@@ -266,9 +257,7 @@ namespace DafnyLanguage
_errorProvider.Dispose();
_errorProvider = null;
}
- BufferIdleEventUtil.RemoveBufferIdleEventListener(_buffer, UponIdle);
- timer.Tick -= ResolveBuffer;
- _buffer.Changed -= BufferChanged;
+ BufferIdleEventUtil.RemoveBufferIdleEventListener(_buffer, ResolveBuffer);
if (_document != null && _document.TextBuffer != null)
{
ResolverTaggers.Remove(_document.TextBuffer);
@@ -328,21 +317,9 @@ namespace DafnyLanguage
/// <summary>
/// Calls the Dafny parser/resolver/type checker on the contents of the buffer, updates the Error List accordingly.
/// </summary>
- void ResolveBuffer(object sender, EventArgs args)
- {
- timer.Stop();
- ParseAndResolveBuffer(sender, args, true);
- }
-
- void UponIdle(object sender, EventArgs args) {
- timer.Stop();
- ParseAndResolveBuffer(sender, args, false);
- timer.Start();
- }
-
- void ParseAndResolveBuffer(object sender, EventArgs args, bool runResolver) {
+ void ResolveBuffer(object sender, EventArgs args) {
ITextSnapshot snapshot = _buffer.CurrentSnapshot;
- if (snapshot == Snapshot && !runResolver)
+ if (snapshot == Snapshot)
return; // we've already done this snapshot
string filename = _document != null ? _document.FilePath : "<program>";
@@ -351,7 +328,7 @@ namespace DafnyLanguage
Dafny.Program program;
try
{
- program = driver.ProcessResolution(runResolver);
+ program = driver.ProcessResolution(true);
newErrors = driver.Errors;
}
catch (Exception e)
@@ -380,11 +357,6 @@ namespace DafnyLanguage
UpdateErrorList(snapshot);
}
- void BufferChanged(object sender, TextContentChangedEventArgs e) {
- timer.Stop();
- timer.Start();
- }
-
public void UpdateErrorList(ITextSnapshot snapshot)
{
if (_errorProvider != null && !m_disposed)
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