diff options
| author |  wuestholz <unknown> | 2014-09-23 11:32:04 +0200 |
|---|---|---|
| committer | wuestholz <unknown> | 2014-09-23 11:32:04 +0200 |
| commit | fb226b8b4b9315a0ad2df1fcd1b4a7f12e118791 (patch) | |
| tree | 9245479972ed887b26b013ba4fb6c05862767846 /Source/Core/DeadVarElim.cs | |
| parent | 2031fb15596b2a114f7b3e0bb85ff838507051a0 (diff) | |
Did some refactoring.
Diffstat (limited to 'Source/Core/DeadVarElim.cs')
| -rw-r--r-- | Source/Core/DeadVarElim.cs | 40 |
1 files changed, 16 insertions, 24 deletions
diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs index b54a45c1..e6cf3e9d 100644 --- a/Source/Core/DeadVarElim.cs +++ b/Source/Core/DeadVarElim.cs @@ -73,32 +73,24 @@ namespace Microsoft.Boogie { }
HashSet<Procedure/*!*/> implementedProcs = new HashSet<Procedure/*!*/>();
- foreach (Declaration/*!*/ decl in program.TopLevelDeclarations) {
- Contract.Assert(decl != null);
- if (decl is Implementation) {
- Implementation impl = (Implementation)decl;
- if (impl.Proc != null)
- implementedProcs.Add(impl.Proc);
- }
+ foreach (var impl in program.Implementations) {
+ if (impl.Proc != null)
+ implementedProcs.Add(impl.Proc);
}
- foreach (Declaration/*!*/ decl in program.TopLevelDeclarations) {
- Contract.Assert(decl != null);
- if (decl is Procedure)
+ foreach (var proc in program.Procedures) {
+ if (!implementedProcs.Contains(proc))
{
- if (!implementedProcs.Contains(cce.NonNull((Procedure)decl)))
+ enclosingProc = proc;
+ foreach (var expr in proc.Modifies)
{
- enclosingProc = (Procedure)decl;
- foreach (IdentifierExpr/*!*/ expr in enclosingProc.Modifies)
- {
- Contract.Assert(expr != null);
- ProcessVariable(expr.Decl);
- }
- enclosingProc = null;
- }
- else
- {
- modSets.Add(decl as Procedure, new HashSet<Variable>());
+ Contract.Assert(expr != null);
+ ProcessVariable(expr.Decl);
}
+ enclosingProc = null;
+ }
+ else
+ {
+ modSets.Add(proc, new HashSet<Variable>());
}
}
@@ -917,7 +909,7 @@ namespace Microsoft.Boogie { varsLiveAtEntry.Clear();
varsLiveSummary.Clear();
- foreach (Declaration/*!*/ decl in program.TopLevelDeclarations) {
+ foreach (var decl in program.TopLevelDeclarations) {
Contract.Assert(decl != null);
if (decl is Implementation) {
Implementation/*!*/ imp = (Implementation/*!*/)cce.NonNull(decl);
@@ -1490,7 +1482,7 @@ b.liveVarsBefore = procICFG[mainImpl.Name].liveVarsAfter[b]; if (predicateCmd.Expr is LiteralExpr && prog != null && impl != null) {
LiteralExpr le = (LiteralExpr)predicateCmd.Expr;
if (le.IsFalse) {
- List<GlobalVariable/*!*/>/*!*/ globals = prog.GlobalVariables();
+ var globals = prog.GlobalVariables();
Contract.Assert(cce.NonNullElements(globals));
foreach (Variable/*!*/ v in globals) {
Contract.Assert(v != null);
|