From 9a8cb7e40a8bde05f53e616a9b47f06fe57bcaed Mon Sep 17 00:00:00 2001
From: qadeer <unknown>
Date: Wed, 5 Feb 2014 12:31:14 -0800
Subject: bug fix in error trace printing added a class for Token elimination
 (not done yet)

---
 Source/Concurrency/YieldTypeChecker.cs |  7 +++-
 Source/Core/DeadVarElim.cs             | 77 ++++++++++++++++++++++++++++++++++
 2 files changed, 82 insertions(+), 2 deletions(-)

(limited to 'Source')

diff --git a/Source/Concurrency/YieldTypeChecker.cs b/Source/Concurrency/YieldTypeChecker.cs
index a848ebeb..086e68fa 100644
--- a/Source/Concurrency/YieldTypeChecker.cs
+++ b/Source/Concurrency/YieldTypeChecker.cs
@@ -63,8 +63,11 @@ namespace Microsoft.Boogie
             String s = "\nBody of " + impl.Proc.Name + " is not yield_type_safe at phase " + currPhaseNum.ToString() + "\n";
             foreach (var move in errorAutomaton.GetMoves())
             {
-                IToken tok = nodeToAbsy[move.SourceState].tok;
-                s += string.Format("{0}({1}, {2})\n", tok.filename, tok.line, tok.col);
+                if (nodeToAbsy.ContainsKey(move.SourceState))
+                {
+                    IToken tok = nodeToAbsy[move.SourceState].tok;
+                    s += string.Format("{0}({1}, {2})\n", tok.filename, tok.line, tok.col);
+                }
             }
             return s;
         }
diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs
index 59f03aac..b89219a9 100644
--- a/Source/Core/DeadVarElim.cs
+++ b/Source/Core/DeadVarElim.cs
@@ -1644,4 +1644,81 @@ b.liveVarsBefore = procICFG[mainImpl.Name].liveVarsAfter[b];
       return ret;
     }
   }
+
+  public class TokenEliminator : StandardVisitor
+  {
+      public int TokenCount = 0;
+      public override Expr VisitExpr(Expr node)
+      {
+          node.tok = Token.NoToken;
+          TokenCount++;
+          return base.VisitExpr(node);
+      }
+      public override Variable VisitVariable(Variable node)
+      {
+          node.tok = Token.NoToken;
+          TokenCount++; 
+          return base.VisitVariable(node);
+      }
+      public override Function VisitFunction(Function node)
+      {
+          node.tok = Token.NoToken;
+          TokenCount++; 
+          return base.VisitFunction(node);
+      }
+      public override Implementation VisitImplementation(Implementation node)
+      {
+          node.tok = Token.NoToken;
+          TokenCount++; 
+          return base.VisitImplementation(node);
+      }
+      public override Procedure VisitProcedure(Procedure node)
+      {
+          node.tok = Token.NoToken;
+          TokenCount++; 
+          return base.VisitProcedure(node);
+      }
+      public override Axiom VisitAxiom(Axiom node)
+      {
+          node.tok = Token.NoToken;
+          TokenCount++; 
+          return base.VisitAxiom(node);
+      }
+      public override Cmd VisitAssignCmd(AssignCmd node)
+      {
+          node.tok = Token.NoToken;
+          TokenCount++; 
+          return base.VisitAssignCmd(node);
+      }
+      public override Cmd VisitAssumeCmd(AssumeCmd node)
+      {
+          node.tok = Token.NoToken;
+          TokenCount++; 
+          return base.VisitAssumeCmd(node);
+      }
+      public override Cmd VisitHavocCmd(HavocCmd node)
+      {
+          node.tok = Token.NoToken;
+          TokenCount++; 
+          return base.VisitHavocCmd(node);
+      }
+      public override Constant VisitConstant(Constant node)
+      {
+          node.tok = Token.NoToken;
+          TokenCount++; 
+          return base.VisitConstant(node);
+      }
+      public override TransferCmd VisitTransferCmd(TransferCmd node)
+      {
+          node.tok = Token.NoToken;
+          TokenCount++; 
+          return base.VisitTransferCmd(node);
+      }
+      public override Block VisitBlock(Block node)
+      {
+          node.tok = Token.NoToken;
+          TokenCount++; 
+          return base.VisitBlock(node);
+      }
+  }
 }
\ No newline at end of file
-- 
cgit v1.2.3