summaryrefslogtreecommitdiff
path: root/Source/Core/ResolutionContext.cs
diff options
context:
space:
mode:
authorGravatar Valentin Wüstholz <wuestholz@gmail.com>2015-11-16 12:04:37 -0600
committerGravatar Valentin Wüstholz <wuestholz@gmail.com>2015-11-16 12:04:37 -0600
commitf049d2ec646244bc40964b36d961966fe2a3e4dc (patch)
tree31dd22334b5cb314eb018fd1deee810836ffa486 /Source/Core/ResolutionContext.cs
parent74765d1b66730a612ce3eaf404883c09ab8f0153 (diff)
Add support for identifying unnecessary assumes.
Diffstat (limited to 'Source/Core/ResolutionContext.cs')
-rw-r--r--Source/Core/ResolutionContext.cs12
1 files changed, 12 insertions, 0 deletions
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);