From f049d2ec646244bc40964b36d961966fe2a3e4dc Mon Sep 17 00:00:00 2001
From: Valentin Wüstholz <wuestholz@gmail.com>
Date: Mon, 16 Nov 2015 12:04:37 -0600
Subject: Add support for identifying unnecessary assumes.

---
 Source/Core/ResolutionContext.cs | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'Source/Core/ResolutionContext.cs')

diff --git a/Source/Core/ResolutionContext.cs b/Source/Core/ResolutionContext.cs
index 474a91dd..279e00bf 100644
--- a/Source/Core/ResolutionContext.cs
+++ b/Source/Core/ResolutionContext.cs
@@ -339,6 +339,18 @@ namespace Microsoft.Boogie {
       varContext = varContext.ParentContext;
     }
 
+    public readonly ISet<string> StatementIds = new HashSet<string>();
+
+    public void AddStatementId(IToken tok, string name)
+    {
+      if (StatementIds.Contains(name))
+      {
+        Error(tok, "more than one statement with same id: " + name);
+        return;
+      }
+      StatementIds.Add(name);
+    }
+
     public void AddVariable(Variable var, bool global) {
       Contract.Requires(var != null);
       var previous = FindVariable(cce.NonNull(var.Name), !global);
-- 
cgit v1.2.3