diff options
| author |  qadeer <unknown> | 2014-02-05 12:31:14 -0800 |
|---|---|---|
| committer | qadeer <unknown> | 2014-02-05 12:31:14 -0800 |
| commit | 9a8cb7e40a8bde05f53e616a9b47f06fe57bcaed (patch) | |
| tree | 16e8d0e71c7fd940e2ac872ecad0f059d7b2204a /Source | |
| parent | 37ddd0bd2f8118948a95bffedbbc8d976adaa7ce (diff) | |
bug fix in error trace printing
added a class for Token elimination (not done yet)
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Concurrency/YieldTypeChecker.cs | 7 | ||||
| -rw-r--r-- | Source/Core/DeadVarElim.cs | 77 |
2 files changed, 82 insertions, 2 deletions
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 |