Did some refactoring.

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
parent: 2031fb15596b2a114f7b3e0bb85ff838507051a0 (diff)
25 files changed, 254 insertions, 328 deletions
diff --git a/Source/AbsInt/NativeLattice.cs b/Source/AbsInt/NativeLattice.cs
index 8bb44385..30014643 100644
--- a/Source/AbsInt/NativeLattice.cs
+++ b/Source/AbsInt/NativeLattice.cs
@@ -120,8 +120,7 @@ namespace Microsoft.Boogie.AbstractInterpretation
       // procedures.
 
       return program
-            .TopLevelDeclarations
-            .Where(d => d is Implementation).Select(i => (Implementation)i)
+            .Implementations
             .GroupBy(i => i.Proc).Select(g => g.ToArray()).ToDictionary(a => a[0].Proc);
     }
 
@@ -137,17 +136,13 @@ namespace Microsoft.Boogie.AbstractInterpretation
       // Differently stated, it is the \alpha from axioms (i.e. first order formulae) to the underlyng abstract domain
       var initialElement = lattice.Top;
       Contract.Assert(initialElement != null);
-      foreach (var decl in program.TopLevelDeclarations) {
-        var ax = decl as Axiom;
-        if (ax != null) {
-          initialElement = lattice.Constrain(initialElement, ax.Expr);
-        }
+      foreach (var ax in program.Axioms) {
+        initialElement = lattice.Constrain(initialElement, ax.Expr);
       }
 
       // analyze each procedure
-      foreach (var decl in program.TopLevelDeclarations) {
-        var proc = decl as Procedure;
-        if (proc != null && procedureImplementations.ContainsKey(proc)) {
+      foreach (var proc in program.Procedures) {
+        if (procedureImplementations.ContainsKey(proc)) {
           // analyze each implementation of the procedure
           foreach (var impl in procedureImplementations[proc]) {
             // add the precondition to the axioms
diff --git a/Source/AbsInt/Traverse.cs b/Source/AbsInt/Traverse.cs
index 633ad86e..184a4071 100644
--- a/Source/AbsInt/Traverse.cs
+++ b/Source/AbsInt/Traverse.cs
@@ -24,25 +24,22 @@ namespace Microsoft.Boogie {
       Contract.Requires(program != null);
       cce.BeginExpose(program);
 
-      foreach (Declaration m in program.TopLevelDeclarations) {
-        Implementation impl = m as Implementation;
-        if (impl != null) {
-          if (impl.Blocks != null && impl.Blocks.Count > 0) {
-            Contract.Assume(cce.IsConsistent(impl));
-            cce.BeginExpose(impl);
-            Block start = impl.Blocks[0];
-            Contract.Assume(start != null);
-            Contract.Assume(cce.IsConsistent(start));
-            Visit(start);
-
-            // We reset the state...
-            foreach (Block b in impl.Blocks) {
-              cce.BeginExpose(b);
-              b.TraversingStatus = Block.VisitState.ToVisit;
-              cce.EndExpose();
-            }
+      foreach (var impl in program.Implementations) {
+        if (impl.Blocks != null && impl.Blocks.Count > 0) {
+          Contract.Assume(cce.IsConsistent(impl));
+          cce.BeginExpose(impl);
+          Block start = impl.Blocks[0];
+          Contract.Assume(start != null);
+          Contract.Assume(cce.IsConsistent(start));
+          Visit(start);
+
+          // We reset the state...
+          foreach (Block b in impl.Blocks) {
+            cce.BeginExpose(b);
+            b.TraversingStatus = Block.VisitState.ToVisit;
             cce.EndExpose();
           }
+          cce.EndExpose();
         }
       }
       cce.EndExpose();
diff --git a/Source/Concurrency/LinearSets.cs b/Source/Concurrency/LinearSets.cs
index f9a791bc..b6e23e38 100644
--- a/Source/Concurrency/LinearSets.cs
+++ b/Source/Concurrency/LinearSets.cs
@@ -634,10 +634,8 @@ namespace Microsoft.Boogie
 
         public void Transform()
         {
-            foreach (var decl in program.TopLevelDeclarations)
+            foreach (var impl in program.Implementations)
             {
-                Implementation impl = decl as Implementation;
-                if (impl == null) continue;
                 Dictionary<string, Variable> domainNameToInputVar = new Dictionary<string, Variable>();
                 foreach (string domainName in linearDomains.Keys)
                 {
@@ -739,11 +737,8 @@ namespace Microsoft.Boogie
                 }
             }
 
-            foreach (var decl in program.TopLevelDeclarations)
+            foreach (var proc in program.Procedures)
             {
-                Procedure proc = decl as Procedure;
-                if (proc == null) continue;
-
                 Dictionary<string, HashSet<Variable>> domainNameToInputScope = new Dictionary<string, HashSet<Variable>>();
                 Dictionary<string, HashSet<Variable>> domainNameToOutputScope = new Dictionary<string, HashSet<Variable>>();
                 foreach (var domainName in linearDomains.Keys)
diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs
index 23c8945b..baea905a 100644
--- a/Source/Concurrency/OwickiGries.cs
+++ b/Source/Concurrency/OwickiGries.cs
@@ -1182,19 +1182,17 @@ namespace Microsoft.Boogie
                 if (CommandLineOptions.Clo.TrustPhasesDownto <= phaseNum || phaseNum <= CommandLineOptions.Clo.TrustPhasesUpto) continue;
 
                 MyDuplicator duplicator = new MyDuplicator(moverTypeChecker, phaseNum);
-                foreach (var decl in program.TopLevelDeclarations)
+                foreach (var proc in program.Procedures)
                 {
-                    Procedure proc = decl as Procedure;
-                    if (proc == null || !moverTypeChecker.procToActionInfo.ContainsKey(proc)) continue;
+                    if (!moverTypeChecker.procToActionInfo.ContainsKey(proc)) continue;
                     Procedure duplicateProc = duplicator.VisitProcedure(proc);
                     decls.Add(duplicateProc);
                 }
                 decls.AddRange(duplicator.impls);
                 OwickiGries ogTransform = new OwickiGries(linearTypeChecker, moverTypeChecker, duplicator);
-                foreach (var decl in program.TopLevelDeclarations)
+                foreach (var impl in program.Implementations)
                 {
-                    Implementation impl = decl as Implementation;
-                    if (impl == null || !moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc) || moverTypeChecker.procToActionInfo[impl.Proc].phaseNum < phaseNum)
+                    if (!moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc) || moverTypeChecker.procToActionInfo[impl.Proc].phaseNum < phaseNum)
                         continue;
                     Implementation duplicateImpl = duplicator.VisitImplementation(impl);
                     ogTransform.TransformImpl(duplicateImpl);
diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs
index 5fd67978..cd636946 100644
--- a/Source/Concurrency/TypeCheck.cs
+++ b/Source/Concurrency/TypeCheck.cs
@@ -269,10 +269,9 @@ namespace Microsoft.Boogie
 
         public void TypeCheck()
         {
-            foreach (Declaration decl in program.TopLevelDeclarations)
+            foreach (var proc in program.Procedures)
             {
-                Procedure proc = decl as Procedure;
-                if (proc == null || !QKeyValue.FindBoolAttribute(proc.Attributes, "yields")) continue;
+                if (!QKeyValue.FindBoolAttribute(proc.Attributes, "yields")) continue;
 
                 int phaseNum = int.MaxValue;
                 int availableUptoPhaseNum = int.MaxValue;
diff --git a/Source/Concurrency/YieldTypeChecker.cs b/Source/Concurrency/YieldTypeChecker.cs
index 98657706..7a037f93 100644
--- a/Source/Concurrency/YieldTypeChecker.cs
+++ b/Source/Concurrency/YieldTypeChecker.cs
@@ -134,10 +134,9 @@ namespace Microsoft.Boogie
         
         public static void PerformYieldSafeCheck(MoverTypeChecker moverTypeChecker)
         {
-            foreach (var decl in moverTypeChecker.program.TopLevelDeclarations)
+            foreach (var impl in moverTypeChecker.program.Implementations)
             {
-                Implementation impl = decl as Implementation;
-                if (impl == null || !moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc) || moverTypeChecker.procToActionInfo[impl.Proc].phaseNum == 0) continue;
+                if (!moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc) || moverTypeChecker.procToActionInfo[impl.Proc].phaseNum == 0) continue;
                 impl.PruneUnreachableBlocks();
                 Graph<Block> implGraph = Program.GraphFromImpl(impl);
                 implGraph.ComputeLoops();
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index b48ddd3b..baefd09a 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -361,20 +361,19 @@ namespace Microsoft.Boogie {
       //Contract.Requires(rc != null);
       Helpers.ExtraTraceInformation("Starting resolution");
 
-      foreach (Declaration d in TopLevelDeclarations) {
+      foreach (var d in TopLevelDeclarations) {
         d.Register(rc);
       }
 
       ResolveTypes(rc);
 
       var prunedTopLevelDecls = new List<Declaration/*!*/>();
-      foreach (Declaration d in TopLevelDeclarations) {
+      foreach (var d in TopLevelDeclarations) {
         if (QKeyValue.FindBoolAttribute(d.Attributes, "ignore")) {
           continue;
         }
         // resolve all the non-type-declarations
-        if (d is TypeCtorDecl || d is TypeSynonymDecl) {
-        } else {
+        if (!(d is TypeCtorDecl || d is TypeSynonymDecl)) {
           int e = rc.ErrorCount;
           d.Resolve(rc);
           if (CommandLineOptions.Clo.OverlookBoogieTypeErrors && rc.ErrorCount != e && d is Implementation) {
@@ -388,27 +387,24 @@ namespace Microsoft.Boogie {
       }
       TopLevelDeclarations = prunedTopLevelDecls;
 
-      foreach (Declaration d in TopLevelDeclarations) {
-        Variable v = d as Variable;
-        if (v != null) {
-          v.ResolveWhere(rc);
-        }
+      foreach (var v in Variables) {
+        v.ResolveWhere(rc);
       }
     }
 
     private void ResolveTypes(ResolutionContext rc) {
       Contract.Requires(rc != null);
       // first resolve type constructors
-      foreach (Declaration d in TopLevelDeclarations) {
-        if (d is TypeCtorDecl && !QKeyValue.FindBoolAttribute(d.Attributes, "ignore"))
+      foreach (var d in TopLevelDeclarations.OfType<TypeCtorDecl>()) {
+        if (!QKeyValue.FindBoolAttribute(d.Attributes, "ignore"))
           d.Resolve(rc);
       }
 
       // collect type synonym declarations
       List<TypeSynonymDecl/*!*/>/*!*/ synonymDecls = new List<TypeSynonymDecl/*!*/>();
-      foreach (Declaration d in TopLevelDeclarations) {
+      foreach (var d in TopLevelDeclarations.OfType<TypeSynonymDecl>()) {
         Contract.Assert(d != null);
-        if (d is TypeSynonymDecl && !QKeyValue.FindBoolAttribute(d.Attributes, "ignore"))
+        if (!QKeyValue.FindBoolAttribute(d.Attributes, "ignore"))
           synonymDecls.Add((TypeSynonymDecl)d);
       }
 
@@ -432,31 +428,74 @@ namespace Microsoft.Boogie {
       Helpers.ExtraTraceInformation("Starting typechecking");
 
       int oldErrorCount = tc.ErrorCount;
-      foreach (Declaration d in TopLevelDeclarations) {
+      foreach (var d in TopLevelDeclarations) {
         d.Typecheck(tc);
       }
 
       if (oldErrorCount == tc.ErrorCount) {
         // check whether any type proxies have remained uninstantiated
         TypeAmbiguitySeeker/*!*/ seeker = new TypeAmbiguitySeeker(tc);
-        foreach (Declaration d in TopLevelDeclarations) {
+        foreach (var d in TopLevelDeclarations) {
           seeker.Visit(d);
         }
       }
     }
 
-    public IEnumerable<Implementation> Implementations()
+    public IEnumerable<Implementation> Implementations
+    {
+      get
+      {
+        return TopLevelDeclarations.OfType<Implementation>();
+      }
+    }
+
+    public IEnumerable<Axiom> Axioms
+    {
+      get
+      {
+        return TopLevelDeclarations.OfType<Axiom>();
+      }
+    }
+
+    public IEnumerable<Procedure> Procedures
+    {
+      get
+      {
+        return TopLevelDeclarations.OfType<Procedure>();
+      }
+    }
+
+    public IEnumerable<Function> Functions
+    {
+      get
+      {
+        return TopLevelDeclarations.OfType<Function>();
+      }
+    }
+    
+    public IEnumerable<Variable> Variables
+    {
+      get
+      {
+        return TopLevelDeclarations.OfType<Variable>();
+      }
+    }
+
+    public IEnumerable<Constant> Constants
     {
-      return TopLevelDeclarations.OfType<Implementation>();
+      get
+      {
+        return TopLevelDeclarations.OfType<Constant>();
+      }
     }
 
     public IEnumerable<Block> Blocks()
     {
-      return Implementations().Select(Item => Item.Blocks).SelectMany(Item => Item);
+      return Implementations.Select(Item => Item.Blocks).SelectMany(Item => Item);
     }
 
     public void ComputeStronglyConnectedComponents() {
-      foreach (Declaration d in this.TopLevelDeclarations) {
+      foreach (var d in this.TopLevelDeclarations) {
         d.ComputeStronglyConnectedComponents();
       }
     }
@@ -465,14 +504,14 @@ namespace Microsoft.Boogie {
     /// Reset the abstract stated computed before
     /// </summary>
     public void ResetAbstractInterpretationState() {
-      foreach (Declaration d in this.TopLevelDeclarations) {
+      foreach (var d in this.TopLevelDeclarations) {
         d.ResetAbstractInterpretationState();
       }
     }
 
     public void UnrollLoops(int n, bool uc) {
       Contract.Requires(0 <= n);
-      foreach (var impl in Implementations()) {
+      foreach (var impl in Implementations) {
         if (impl.Blocks != null && impl.Blocks.Count > 0) {
           cce.BeginExpose(impl);
           {
@@ -874,20 +913,16 @@ namespace Microsoft.Boogie {
     public static Graph<Implementation> BuildCallGraph(Program program) {
       Graph<Implementation> callGraph = new Graph<Implementation>();
       Dictionary<Procedure, HashSet<Implementation>> procToImpls = new Dictionary<Procedure, HashSet<Implementation>>();
-      foreach (Declaration decl in program.TopLevelDeclarations) {
-        Procedure proc = decl as Procedure;
-        if (proc == null) continue;
+      foreach (var proc in program.Procedures) {
         procToImpls[proc] = new HashSet<Implementation>();
       }
-      foreach (Declaration decl in program.TopLevelDeclarations) {
-        Implementation impl = decl as Implementation;
-        if (impl == null || impl.SkipVerification) continue;
+      foreach (var impl in program.Implementations) {
+        if (impl.SkipVerification) continue;
         callGraph.AddSource(impl);
         procToImpls[impl.Proc].Add(impl);
       }
-      foreach (Declaration decl in program.TopLevelDeclarations) {
-        Implementation impl = decl as Implementation;
-        if (impl == null || impl.SkipVerification) continue;
+      foreach (var impl in program.Implementations) {
+        if (impl.SkipVerification) continue;
         foreach (Block b in impl.Blocks) {
           foreach (Cmd c in b.Cmds) {
             CallCmd cc = c as CallCmd;
@@ -984,10 +1019,9 @@ namespace Microsoft.Boogie {
         procsWithIrreducibleLoops = new HashSet<string>();
         List<Implementation/*!*/>/*!*/ loopImpls = new List<Implementation/*!*/>();
         Dictionary<string, Dictionary<string, Block>> fullMap = new Dictionary<string, Dictionary<string, Block>>();
-        foreach (Declaration d in this.TopLevelDeclarations)
+        foreach (var impl in this.Implementations)
         {
-            Implementation impl = d as Implementation;
-            if (impl != null && impl.Blocks != null && impl.Blocks.Count > 0)
+            if (impl.Blocks != null && impl.Blocks.Count > 0)
             {
                 try
                 {
@@ -1046,15 +1080,13 @@ namespace Microsoft.Boogie {
     }
 
     private List<GlobalVariable/*!*/> globals = null;
-    public List<GlobalVariable/*!*/>/*!*/ GlobalVariables() {
+    public IEnumerable<GlobalVariable/*!*/>/*!*/ GlobalVariables() {
       Contract.Ensures(cce.NonNullElements(Contract.Result<List<GlobalVariable>>()));
       if (globals != null)
         return globals;
       globals = new List<GlobalVariable/*!*/>();
-      foreach (Declaration d in TopLevelDeclarations) {
-        GlobalVariable gvar = d as GlobalVariable;
-        if (gvar != null)
-          globals.Add(gvar);
+      foreach (var gvar in TopLevelDeclarations.OfType<GlobalVariable>()) {
+        globals.Add(gvar);
       }
       return globals;
     }
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);
diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs
index 86311d18..6dd030e8 100644
--- a/Source/Core/Duplicator.cs
+++ b/Source/Core/Duplicator.cs
@@ -641,7 +641,7 @@ namespace Microsoft.Boogie {
           if (funCall != null)
           {
             // TODO(wuestholz): Maybe we should speed up this lookup.
-            funCall.Func = Program.TopLevelDeclarations.OfType<Function>().FirstOrDefault(f => f.Name == funCall.FunctionName);
+            funCall.Func = Program.Functions.FirstOrDefault(f => f.Name == funCall.FunctionName);
           }
         }
         return result;
diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs
index 4738d855..fc2608b7 100644
--- a/Source/Core/Inline.cs
+++ b/Source/Core/Inline.cs
@@ -202,7 +202,7 @@ namespace Microsoft.Boogie {
       Contract.Ensures(impl.Proc != null);
       ResolutionContext rc = new ResolutionContext(new DummyErrorSink());
 
-      foreach (Declaration decl in program.TopLevelDeclarations) {
+      foreach (var decl in program.TopLevelDeclarations) {
         decl.Register(rc);
       }
 
@@ -675,9 +675,8 @@ namespace Microsoft.Boogie {
 
     protected static Implementation FindProcImpl(Program program, Procedure proc) {
       Contract.Requires(program != null);
-      foreach (Declaration decl in program.TopLevelDeclarations) {
-        Implementation impl = decl as Implementation;
-        if (impl != null && impl.Proc == proc) {
+      foreach (var impl in program.Implementations) {
+        if (impl.Proc == proc) {
           return impl;
         }
       }
diff --git a/Source/Core/InterProceduralReachabilityGraph.cs b/Source/Core/InterProceduralReachabilityGraph.cs
index ccf4b153..b477e7de 100644
--- a/Source/Core/InterProceduralReachabilityGraph.cs
+++ b/Source/Core/InterProceduralReachabilityGraph.cs
@@ -63,7 +63,7 @@ namespace Microsoft.Boogie
 
     private IEnumerable<Block> OriginalProgramBlocks()
     {
-      return prog.TopLevelDeclarations.OfType<Implementation>().Select(Item => Item.Blocks).SelectMany(Item => Item);
+      return prog.Implementations.Select(Item => Item.Blocks).SelectMany(Item => Item);
     }
 
     private void AddCallAndReturnEdges()
@@ -118,7 +118,7 @@ namespace Microsoft.Boogie
     private void ProcessBodilessProcedures()
     {
       #region Add single node CFG for procedures with no body
-      foreach (var proc in prog.TopLevelDeclarations.OfType<Procedure>())
+      foreach (var proc in prog.Procedures)
       {
         if (!newProcedureEntryNodes.ContainsKey(proc.Name))
         {
@@ -134,7 +134,7 @@ namespace Microsoft.Boogie
     private void ProcessImplementations()
     {
       #region Transform implementation CFGs so that every call is in its own basic block
-      foreach (var impl in prog.TopLevelDeclarations.OfType<Implementation>())
+      foreach (var impl in prog.Implementations)
       {
         string exitLabel = "__" + impl.Name + "_newExit";
         Block newExit = new Block(Token.NoToken, exitLabel, new List<Cmd>(), new GotoCmd(Token.NoToken, new List<Block>()));
diff --git a/Source/Core/VariableDependenceAnalyser.cs b/Source/Core/VariableDependenceAnalyser.cs
index 476f1cac..c429e199 100644
--- a/Source/Core/VariableDependenceAnalyser.cs
+++ b/Source/Core/VariableDependenceAnalyser.cs
@@ -135,7 +135,7 @@ namespace Microsoft.Boogie {
 
     private void Initialise() {
       foreach (var descriptor in
-        prog.TopLevelDeclarations.OfType<Variable>().Where(Item => VariableRelevantToAnalysis(Item, null)).
+        prog.Variables.Where(Item => VariableRelevantToAnalysis(Item, null)).
           Select(Variable => Variable.Name).
           Select(Name => new GlobalDescriptor(Name))) {
         dependsOnNonTransitive.AddEdge(descriptor, descriptor);
@@ -164,12 +164,12 @@ namespace Microsoft.Boogie {
     }
 
     private IEnumerable<Procedure> NonInlinedProcedures() {
-      return prog.TopLevelDeclarations.OfType<Procedure>().
+      return prog.Procedures.
         Where(Item => QKeyValue.FindIntAttribute(Item.Attributes, "inline", -1) == -1);
     }
 
     private IEnumerable<Implementation> NonInlinedImplementations() {
-      return prog.TopLevelDeclarations.OfType<Implementation>().
+      return prog.Implementations.
         Where(Item => QKeyValue.FindIntAttribute(Item.Proc.Attributes, "inline", -1) == -1);
     }
 
@@ -439,7 +439,7 @@ namespace Microsoft.Boogie {
       Dictionary<Implementation, Dictionary<Block, HashSet<Block>>> LocalCtrlDeps = new Dictionary<Implementation, Dictionary<Block, HashSet<Block>>>();
 
       // Work out and union together local control dependences
-      foreach (var Impl in prog.TopLevelDeclarations.OfType<Implementation>()) {
+      foreach (var Impl in prog.Implementations) {
         Graph<Block> blockGraph = prog.ProcessLoops(Impl);
         LocalCtrlDeps[Impl] = blockGraph.ControlDependence();
         foreach (var KeyValue in LocalCtrlDeps[Impl]) {
@@ -450,7 +450,7 @@ namespace Microsoft.Boogie {
       Graph<Implementation> callGraph = Program.BuildCallGraph(prog);
 
       // Add inter-procedural control dependence nodes based on calls
-      foreach (var Impl in prog.TopLevelDeclarations.OfType<Implementation>()) {
+      foreach (var Impl in prog.Implementations) {
         foreach (var b in Impl.Blocks) {
           foreach (var cmd in b.Cmds.OfType<CallCmd>()) {
             var DirectCallee = GetImplementation(cmd.callee);
@@ -513,7 +513,7 @@ namespace Microsoft.Boogie {
     }
 
     private Implementation GetImplementation(string proc) {
-      foreach (var Impl in prog.TopLevelDeclarations.OfType<Implementation>()) {
+      foreach (var Impl in prog.Implementations) {
         if (Impl.Name.Equals(proc)) {
           return Impl;
         }
diff --git a/Source/Doomed/VCDoomed.cs b/Source/Doomed/VCDoomed.cs
index 6dd3b5ca..4fd574a4 100644
--- a/Source/Doomed/VCDoomed.cs
+++ b/Source/Doomed/VCDoomed.cs
@@ -594,9 +594,8 @@ namespace VC {
       {
         List<Cmd> cc = new List<Cmd>();
         // where clauses of global variables
-        foreach (Declaration d in program.TopLevelDeclarations) {
-          GlobalVariable gvar = d as GlobalVariable;
-          if (gvar != null && gvar.TypedIdent.WhereExpr != null) {
+        foreach (var gvar in program.GlobalVariables()) {
+          if (gvar.TypedIdent.WhereExpr != null) {
             Cmd c = new AssumeCmd(gvar.tok, gvar.TypedIdent.WhereExpr);
             cc.Add(c);
           }
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index a9220a4c..093f1d90 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -467,7 +467,7 @@ namespace Microsoft.Boogie
 
         if (CommandLineOptions.Clo.PrintCFGPrefix != null)
         {
-          foreach (var impl in program.TopLevelDeclarations.OfType<Implementation>())
+          foreach (var impl in program.Implementations)
           {
             using (StreamWriter sw = new StreamWriter(CommandLineOptions.Clo.PrintCFGPrefix + "." + impl.Name + ".dot"))
             {
@@ -868,7 +868,7 @@ namespace Microsoft.Boogie
 
       #region Select and prioritize implementations that should be verified
 
-      var impls = program.TopLevelDeclarations.OfType<Implementation>().Where(
+      var impls = program.Implementations.Where(
         impl => impl != null && CommandLineOptions.Clo.UserWantsToCheckRoutine(cce.NonNull(impl.Name)) && !impl.SkipVerification);
 
       // operate on a stable copy, in case it gets updated while we're running
@@ -876,7 +876,7 @@ namespace Microsoft.Boogie
       if (0 < CommandLineOptions.Clo.VerifySnapshots)
       {
         // TODO(wuestholz): Maybe we should speed up this lookup.
-        OtherDefinitionAxiomsCollector.Collect(program.TopLevelDeclarations.OfType<Axiom>());
+        OtherDefinitionAxiomsCollector.Collect(program.Axioms);
         DependencyCollector.Collect(program);
         stablePrioritizedImpls = impls.OrderByDescending(
           impl => impl.Priority != 1 ? impl.Priority : Cache.VerificationPriority(impl)).ToArray();
@@ -1084,10 +1084,9 @@ namespace Microsoft.Boogie
               var svcgen = vcgen as VC.StratifiedVCGen;
               Contract.Assert(svcgen != null);
               var ss = new HashSet<string>();
-              foreach (var tdecl in program.TopLevelDeclarations)
+              foreach (var c in program.Constants)
               {
-                var c = tdecl as Constant;
-                if (c == null || !c.Name.StartsWith(CommandLineOptions.Clo.inferLeastForUnsat)) continue;
+                if (!c.Name.StartsWith(CommandLineOptions.Clo.inferLeastForUnsat)) continue;
                 ss.Add(c.Name);
               }
               verificationResult.Outcome = svcgen.FindLeastToVerify(impl, ref ss);
diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs
index 55c6ba85..93ca9cb7 100644
--- a/Source/ExecutionEngine/VerificationResultCache.cs
+++ b/Source/ExecutionEngine/VerificationResultCache.cs
@@ -194,7 +194,7 @@ namespace Microsoft.Boogie
     private static void SetAssertionChecksums(Implementation implementation, Program program)
     {
       // TODO(wuestholz): Maybe we should speed up this lookup.
-      var implPrevSnap = program.Implementations().FirstOrDefault(i => i.Id == implementation.Id);
+      var implPrevSnap = program.Implementations.FirstOrDefault(i => i.Id == implementation.Id);
       if (implPrevSnap != null)
       {
         implementation.AssertionChecksums = implPrevSnap.AssertionChecksums;
@@ -204,7 +204,7 @@ namespace Microsoft.Boogie
     private static void SetAssertionChecksumsInPreviousSnapshot(Implementation implementation, Program program)
     {
       // TODO(wuestholz): Maybe we should speed up this lookup.
-      var implPrevSnap = program.Implementations().FirstOrDefault(i => i.Id == implementation.Id);
+      var implPrevSnap = program.Implementations.FirstOrDefault(i => i.Id == implementation.Id);
       if (implPrevSnap != null)
       {
         implementation.AssertionChecksumsInPreviousSnapshot = implPrevSnap.AssertionChecksums;
@@ -216,7 +216,7 @@ namespace Microsoft.Boogie
       var result = base.VisitCallCmd(node);
 
       // TODO(wuestholz): Maybe we should speed up this lookup.
-      var oldProc = programInCachedSnapshot.TopLevelDeclarations.OfType<Procedure>().FirstOrDefault(p => p.Name == node.Proc.Name);
+      var oldProc = programInCachedSnapshot.Procedures.FirstOrDefault(p => p.Name == node.Proc.Name);
       if (oldProc != null
           && oldProc.DependencyChecksum != node.Proc.DependencyChecksum
           && node.AssignedAssumptionVariable == null)
@@ -327,7 +327,7 @@ namespace Microsoft.Boogie
       Contract.Requires(oldProc != null && newProg != null);
 
       // TODO(wuestholz): Maybe we should speed up this lookup.
-      var funcs = newProg.TopLevelDeclarations.OfType<Function>();
+      var funcs = newProg.Functions;
       return oldProc.DependenciesCollected
              && (oldProc.FunctionDependencies == null || oldProc.FunctionDependencies.All(dep => funcs.Any(f => f.Name == dep.Name && f.DependencyChecksum == dep.DependencyChecksum)));
     }
diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs
index c73758d8..e268a8d7 100644
--- a/Source/Houdini/AbstractHoudini.cs
+++ b/Source/Houdini/AbstractHoudini.cs
@@ -58,7 +58,7 @@ namespace Microsoft.Boogie.Houdini {
             this.constant2FuncCall = new Dictionary<string, NAryExpr>();
 
             // Find the existential functions
-            foreach (var func in program.TopLevelDeclarations.OfType<Function>()
+            foreach (var func in program.Functions
                 .Where(f => QKeyValue.FindBoolAttribute(f.Attributes, "existential")))
                 existentialFunctions.Add(func.Name, func);
 
@@ -104,7 +104,7 @@ namespace Microsoft.Boogie.Houdini {
             this.proverTime = TimeSpan.Zero;
             this.numProverQueries = 0;
 
-            program.TopLevelDeclarations.OfType<Implementation>()
+            program.Implementations
                 .Where(impl => !impl.SkipVerification)
                 .Iter(impl => name2Impl.Add(impl.Name, impl));
 
@@ -753,23 +753,19 @@ namespace Microsoft.Boogie.Houdini {
         {
             Graph<Implementation> callGraph = new Graph<Implementation>();
             Dictionary<Procedure, HashSet<Implementation>> procToImpls = new Dictionary<Procedure, HashSet<Implementation>>();
-            foreach (Declaration decl in program.TopLevelDeclarations)
+            foreach (var proc in program.Procedures)
             {
-                Procedure proc = decl as Procedure;
-                if (proc == null) continue;
                 procToImpls[proc] = new HashSet<Implementation>();
             }
-            foreach (Declaration decl in program.TopLevelDeclarations)
+            foreach (var impl in program.Implementations)
             {
-                Implementation impl = decl as Implementation;
-                if (impl == null || impl.SkipVerification) continue;
+                if (impl.SkipVerification) continue;
                 callGraph.AddSource(impl);
                 procToImpls[impl.Proc].Add(impl);
             }
-            foreach (Declaration decl in program.TopLevelDeclarations)
+            foreach (var impl in program.Implementations)
             {
-                Implementation impl = decl as Implementation;
-                if (impl == null || impl.SkipVerification) continue;
+                if (impl.SkipVerification) continue;
                 foreach (Block b in impl.Blocks)
                 {
                     foreach (Cmd c in b.Cmds)
@@ -2139,8 +2135,7 @@ namespace Microsoft.Boogie.Houdini {
               });
 
             domains.Iter(tup => AbstractDomainFactory.Register(tup.Item1, tup.Item2));
-            program.TopLevelDeclarations.OfType<Function>()
-                .Iter(RegisterFunction);
+            program.Functions.Iter(RegisterFunction);
         }
 
         private static void RegisterFunction(Function func)
@@ -2227,8 +2222,7 @@ namespace Microsoft.Boogie.Houdini {
 
             name2Impl.Values.Iter(attachEnsures);
 
-            program.TopLevelDeclarations
-                .OfType<Implementation>()
+            program.Implementations
                 .Iter(impl => impl2Summary.Add(impl.Name, summaryClass.GetFlaseSummary(program, impl)));
 
             // Build call graph
@@ -2237,7 +2231,7 @@ namespace Microsoft.Boogie.Houdini {
             name2Impl.Values.Iter(impl => Succ.Add(impl, new HashSet<Implementation>()));
             name2Impl.Values.Iter(impl => Pred.Add(impl, new HashSet<Implementation>()));
 
-            foreach (var impl in program.TopLevelDeclarations.OfType<Implementation>())
+            foreach (var impl in program.Implementations)
             {
                 foreach (var blk in impl.Blocks)
                 {
@@ -2276,7 +2270,7 @@ namespace Microsoft.Boogie.Houdini {
             var copy = new Dictionary<string, Implementation>();
             if (WitnessFile != null)
             {
-                foreach (var impl in program.TopLevelDeclarations.OfType<Implementation>())
+                foreach (var impl in program.Implementations)
                 {
                     var nimpl = new Implementation(Token.NoToken, impl.Name, impl.TypeParameters,
                         impl.InParams, impl.OutParams, new List<Variable>(impl.LocVars), new List<Block>());
@@ -2365,7 +2359,7 @@ namespace Microsoft.Boogie.Houdini {
                 return Expr.True;
 
             var vars = new Dictionary<string, Expr>();
-            foreach (var g in program.TopLevelDeclarations.OfType<GlobalVariable>())
+            foreach (var g in program.GlobalVariables())
                 vars.Add(g.Name, Expr.Ident(g));
             foreach (var v in proc.InParams.OfType<Variable>())
                 vars.Add(v.Name, Expr.Ident(v));
@@ -2389,7 +2383,7 @@ namespace Microsoft.Boogie.Houdini {
             if (WitnessFile == null)
                 return;
 
-            foreach (var proc in program.TopLevelDeclarations.OfType<Procedure>())
+            foreach (var proc in program.Procedures)
             {
                 var nensures = new List<Ensures>();
                 proc.Ensures.OfType<Ensures>()
@@ -2411,7 +2405,7 @@ namespace Microsoft.Boogie.Houdini {
                 .Iter(decl => decls.Add(decl));
             program.TopLevelDeclarations = decls;
             var name2Proc = new Dictionary<string, Procedure>();
-            foreach (var proc in program.TopLevelDeclarations.OfType<Procedure>())
+            foreach (var proc in program.Procedures)
             {
                 name2Proc.Add(proc.Name, proc);
                 if (impl2Summary.ContainsKey(proc.Name))
@@ -2430,7 +2424,7 @@ namespace Microsoft.Boogie.Houdini {
             }
 
             // Replace SummaryPreds with their definition
-            foreach (var impl in program.TopLevelDeclarations.OfType<Implementation>())
+            foreach (var impl in program.Implementations)
             {
                 foreach (var blk in impl.Blocks)
                 {
@@ -2448,7 +2442,7 @@ namespace Microsoft.Boogie.Houdini {
                         var forold = new Dictionary<string, Expr>();
                         var always = new Dictionary<string, Expr>();
                         int i = 0;
-                        foreach (var g in program.TopLevelDeclarations.OfType<GlobalVariable>())
+                        foreach (var g in program.GlobalVariables())
                         {
                             forold.Add(g.Name, expr.Args[i]);
                             always.Add(g.Name, expr.Args[i]);
@@ -2556,23 +2550,19 @@ namespace Microsoft.Boogie.Houdini {
         {
             Graph<Implementation> callGraph = new Graph<Implementation>();
             Dictionary<Procedure, HashSet<Implementation>> procToImpls = new Dictionary<Procedure, HashSet<Implementation>>();
-            foreach (Declaration decl in program.TopLevelDeclarations)
+            foreach (var proc in program.Procedures)
             {
-                Procedure proc = decl as Procedure;
-                if (proc == null) continue;
                 procToImpls[proc] = new HashSet<Implementation>();
             }
-            foreach (Declaration decl in program.TopLevelDeclarations)
+            foreach (var impl in program.Implementations)
             {
-                Implementation impl = decl as Implementation;
-                if (impl == null || impl.SkipVerification) continue;
+                if (impl.SkipVerification) continue;
                 callGraph.AddSource(impl);
                 procToImpls[impl.Proc].Add(impl);
             }
-            foreach (Declaration decl in program.TopLevelDeclarations)
+            foreach (var impl in program.Implementations)
             {
-                Implementation impl = decl as Implementation;
-                if (impl == null || impl.SkipVerification) continue;
+                if (impl.SkipVerification) continue;
                 foreach (Block b in impl.Blocks)
                 {
                     foreach (Cmd c in b.Cmds)
@@ -2753,7 +2743,7 @@ namespace Microsoft.Boogie.Houdini {
             var ret = new Dictionary<string, VCExpr>();
 
             var cnt = 0;
-            foreach (var g in program.TopLevelDeclarations.OfType<GlobalVariable>())
+            foreach (var g in program.GlobalVariables())
             {
                 ret.Add(string.Format("old({0})", g.Name), summaryPred[cnt]);
                 cnt++;
@@ -2768,7 +2758,7 @@ namespace Microsoft.Boogie.Houdini {
 
             // Fill up values of globals that are not modified
             cnt = 0;
-            foreach (var g in program.TopLevelDeclarations.OfType<GlobalVariable>())
+            foreach (var g in program.GlobalVariables())
             {
                 if (ret.ContainsKey(g.Name)) { cnt++; continue; }
 
@@ -2777,7 +2767,7 @@ namespace Microsoft.Boogie.Houdini {
             }
 
             // Constants
-            foreach (var c in program.TopLevelDeclarations.OfType<Constant>())
+            foreach (var c in program.Constants)
             {
                 var value = prover.Context.BoogieExprTranslator.Translate(Expr.Ident(c));
                 ret.Add(string.Format("{0}", c.Name), value);
@@ -2795,7 +2785,7 @@ namespace Microsoft.Boogie.Houdini {
             var implVars = impl2EndStateVars[impl.Name];
 
             var cnt = 0;
-            foreach (var g in program.TopLevelDeclarations.OfType<GlobalVariable>())
+            foreach (var g in program.GlobalVariables())
             {
                 ret.Add(string.Format("old({0})", g.Name), getValue(implVars[cnt], model));
                 cnt++;
@@ -2810,7 +2800,7 @@ namespace Microsoft.Boogie.Houdini {
 
             // Fill up values of globals that are not modified
             cnt = 0;
-            foreach (var g in program.TopLevelDeclarations.OfType<GlobalVariable>())
+            foreach (var g in program.GlobalVariables())
             {
                 if (ret.ContainsKey(g.Name)) { cnt++; continue; }
 
@@ -2819,7 +2809,7 @@ namespace Microsoft.Boogie.Houdini {
             }
 
             // Constants
-            foreach (var c in program.TopLevelDeclarations.OfType<Constant>())
+            foreach (var c in program.Constants)
             {
                 try
                 {
@@ -3231,7 +3221,7 @@ namespace Microsoft.Boogie.Houdini {
             boolConstants = new HashSet<string>();
             UpperCandidates = new Dictionary<Tuple<string, int>, List<PredicateAbsDisjunct>>();
 
-            program.TopLevelDeclarations.OfType<Constant>()
+            program.Constants
                 .Where(c => c.TypedIdent.Type.IsBool)
                 .Iter(c => boolConstants.Add(c.Name));
 
@@ -3241,7 +3231,7 @@ namespace Microsoft.Boogie.Houdini {
             var posPreT = new HashSet<int>();
             var tempP = new HashSet<Procedure>();
             foreach (var proc in
-                program.TopLevelDeclarations.OfType<Procedure>()
+                program.Procedures
                 .Where(proc => QKeyValue.FindBoolAttribute(proc.Attributes, "template")))
             {
                 tempP.Add(proc);
@@ -3274,7 +3264,7 @@ namespace Microsoft.Boogie.Houdini {
             program.TopLevelDeclarations.RemoveAll(decl => tempP.Contains(decl));
             var upperPreds = new Dictionary<string, List<Expr>>();
 
-            foreach (var impl in program.TopLevelDeclarations.OfType<Implementation>())
+            foreach (var impl in program.Implementations)
             {
                 PrePreds.Add(impl.Name, new List<NamedExpr>());
                 PostPreds.Add(impl.Name, new List<NamedExpr>());
@@ -3876,7 +3866,7 @@ namespace Microsoft.Boogie.Houdini {
             Simplify();
 
             // Find the free expressions
-            var proc = program.TopLevelDeclarations.OfType<Procedure>().FirstOrDefault(p => p.Name == procName);
+            var proc = program.Procedures.FirstOrDefault(p => p.Name == procName);
             Contract.Assert(proc != null);
             Expr freeSummary = Expr.True;
             foreach (var req in proc.Requires.OfType<Requires>().Where(req => req.Free))
@@ -4598,13 +4588,9 @@ namespace Microsoft.Boogie.Houdini {
         public static Dictionary<string, Implementation> nameImplMapping(Program p)
         {
             var m = new Dictionary<string, Implementation>();
-            foreach (Declaration d in p.TopLevelDeclarations)
+            foreach (var impl in p.Implementations)
             {
-                if (d is Implementation)
-                {
-                    Implementation impl = d as Implementation;
-                    m.Add(impl.Name, impl);
-                }
+                m.Add(impl.Name, impl);
             }
 
             return m;
diff --git a/Source/Houdini/CandidateDependenceAnalyser.cs b/Source/Houdini/CandidateDependenceAnalyser.cs
index ea891dd6..9ff333dc 100644
--- a/Source/Houdini/CandidateDependenceAnalyser.cs
+++ b/Source/Houdini/CandidateDependenceAnalyser.cs
@@ -185,7 +185,7 @@ namespace Microsoft.Boogie.Houdini {
 
     private IEnumerable<CandidateInstance> CandidateInstances()
     {
-      foreach (var impl in prog.TopLevelDeclarations.OfType<Implementation>())
+      foreach (var impl in prog.Implementations)
       {
         foreach (var b in impl.Blocks) {
           foreach (Cmd cmd in b.Cmds)
@@ -202,7 +202,7 @@ namespace Microsoft.Boogie.Houdini {
         }
       }
 
-      foreach (var proc in prog.TopLevelDeclarations.OfType<Procedure>())
+      foreach (var proc in prog.Procedures)
       {
         foreach (Requires r in proc.Requires)
         {
@@ -351,7 +351,7 @@ namespace Microsoft.Boogie.Houdini {
     }
 
     private IEnumerable<string> GetCandidates() {
-      return prog.TopLevelDeclarations.OfType<Variable>().Where(Item =>
+      return prog.Variables.Where(Item =>
         QKeyValue.FindBoolAttribute(Item.Attributes, "existential")).Select(Item => Item.Name);
     }
 
@@ -409,7 +409,7 @@ namespace Microsoft.Boogie.Houdini {
         #endregion
 
         #region Adapt candidate assertions to take account of stages
-        foreach (var b in prog.TopLevelDeclarations.OfType<Implementation>().Select(Item => Item.Blocks).SelectMany(Item => Item))
+        foreach (var b in prog.Implementations.Select(Item => Item.Blocks).SelectMany(Item => Item))
         {
             List<Cmd> newCmds = new List<Cmd>();
             foreach (var cmd in b.Cmds)
@@ -433,7 +433,7 @@ namespace Microsoft.Boogie.Houdini {
         #endregion
 
         #region Adapt candidate pre/postconditions to take account of stages
-        foreach (var p in prog.TopLevelDeclarations.OfType<Procedure>())
+        foreach (var p in prog.Procedures)
         {
 
           #region Handle the preconditions
@@ -633,7 +633,7 @@ namespace Microsoft.Boogie.Houdini {
       this.candidateToOccurences = new Dictionary<string,HashSet<object>>();
 
       // Add all candidate occurrences in blocks
-      foreach(Block b in prog.TopLevelDeclarations.OfType<Implementation>().Select(Item => Item.Blocks).SelectMany(Item => Item)) {
+      foreach(Block b in prog.Implementations.Select(Item => Item.Blocks).SelectMany(Item => Item)) {
         foreach(Cmd cmd in b.Cmds) {
           AssertCmd assertCmd = cmd as AssertCmd;
           if(assertCmd != null) {
@@ -646,7 +646,7 @@ namespace Microsoft.Boogie.Houdini {
       }
 
       // Add all candidate occurrences in preconditions
-      foreach(var proc in prog.TopLevelDeclarations.OfType<Procedure>()) {
+      foreach(var proc in prog.Procedures) {
         foreach(Requires r in proc.Requires) {
           string c;
           if(Houdini.MatchCandidate(r.Condition, candidates, out c)) {
@@ -656,7 +656,7 @@ namespace Microsoft.Boogie.Houdini {
       }
 
       // Add all candidate occurrences in preconditions
-      foreach(var proc in prog.TopLevelDeclarations.OfType<Procedure>()) {
+      foreach(var proc in prog.Procedures) {
         foreach(Ensures e in proc.Ensures) {
           string c;
           if(Houdini.MatchCandidate(e.Condition, candidates, out c)) {
diff --git a/Source/Houdini/ConcurrentHoudini.cs b/Source/Houdini/ConcurrentHoudini.cs
index bfc96258..5c0f217f 100644
--- a/Source/Houdini/ConcurrentHoudini.cs
+++ b/Source/Houdini/ConcurrentHoudini.cs
@@ -46,7 +46,7 @@ namespace Microsoft.Boogie.Houdini
           RefutedAnnotation ra = null;
           Implementation refutationSite = null;
 
-          foreach (var r in program.TopLevelDeclarations.OfType<Implementation>()) {
+          foreach (var r in program.Implementations) {
             if (r.Name.Equals(refutedSharedAnnotations[key].RefutationSite.Name)) {
               refutationSite = r;
               break;
@@ -56,7 +56,7 @@ namespace Microsoft.Boogie.Houdini
 
           if (refutedSharedAnnotations[key].Kind == RefutedAnnotationKind.REQUIRES) {
             Procedure proc = null;
-            foreach (var p in program.TopLevelDeclarations.OfType<Procedure>()) {
+            foreach (var p in program.Procedures) {
               if (p.Name.Equals(refutedSharedAnnotations[key].CalleeProc.Name)) {
                 proc = p;
                 break;
diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index e91d0528..6b1f2c39 100644
--- a/Source/Houdini/Houdini.cs
+++ b/Source/Houdini/Houdini.cs
@@ -399,14 +399,11 @@ namespace Microsoft.Boogie.Houdini {
 
     protected HashSet<Variable> CollectExistentialConstants() {
       HashSet<Variable> existentialConstants = new HashSet<Variable>();
-      foreach (Declaration decl in program.TopLevelDeclarations) {
-        Constant constant = decl as Constant;
-        if (constant != null) {
-          bool result = false;
-          if (constant.CheckBooleanAttribute("existential", ref result)) {
-            if (result == true)
-              existentialConstants.Add(constant);
-          }
+      foreach (var constant in program.Constants) {
+        bool result = false;
+        if (constant.CheckBooleanAttribute("existential", ref result)) {
+          if (result == true)
+            existentialConstants.Add(constant);
         }
       }
       return existentialConstants;
@@ -898,7 +895,7 @@ namespace Microsoft.Boogie.Houdini {
     private int NumberOfStages()
     {
       int result = 1;
-      foreach(var c in program.TopLevelDeclarations.OfType<Constant>()) {
+      foreach(var c in program.Constants) {
         result = Math.Max(result, 1 + QKeyValue.FindIntAttribute(c.Attributes, "stage_active", -1));
       }
       return result;
@@ -1103,7 +1100,7 @@ namespace Microsoft.Boogie.Houdini {
     protected Dictionary<Variable, bool> GetAssignmentWithStages(int currentStage, IEnumerable<int> completedStages)
     {
       Dictionary<Variable, bool> result = new Dictionary<Variable, bool>(currentHoudiniState.Assignment);
-      foreach (var c in program.TopLevelDeclarations.OfType<Constant>())
+      foreach (var c in program.Constants)
       {
         int stageActive = QKeyValue.FindIntAttribute(c.Attributes, "stage_active", -1);
         if (stageActive != -1)
@@ -1181,7 +1178,7 @@ namespace Microsoft.Boogie.Houdini {
 
       // Treat all assertions
       // TODO: do we need to also consider assumptions?
-      foreach (Block block in prog.TopLevelDeclarations.OfType<Implementation>().Select(item => item.Blocks).SelectMany(item => item)) {
+      foreach (Block block in prog.Implementations.Select(item => item.Blocks).SelectMany(item => item)) {
         List<Cmd> newCmds = new List<Cmd>();
         foreach (Cmd cmd in block.Cmds) {
           string c;
@@ -1190,7 +1187,7 @@ namespace Microsoft.Boogie.Houdini {
             var cVar = currentHoudiniState.Assignment.Keys.Where(item => item.Name.Equals(c)).ToList()[0];
             if (currentHoudiniState.Assignment[cVar]) {
               Dictionary<Variable, Expr> cToTrue = new Dictionary<Variable, Expr>();
-              Variable cVarProg = prog.TopLevelDeclarations.OfType<Variable>().Where(item => item.Name.Equals(c)).ToList()[0];
+              Variable cVarProg = prog.Variables.Where(item => item.Name.Equals(c)).ToList()[0];
               cToTrue[cVarProg] = Expr.True;
               newCmds.Add(new AssumeCmd(assertCmd.tok,
                 Substituter.Apply(Substituter.SubstitutionFromHashtable(cToTrue), assertCmd.Expr),
@@ -1204,14 +1201,14 @@ namespace Microsoft.Boogie.Houdini {
         block.Cmds = newCmds;
       }
 
-      foreach (var proc in prog.TopLevelDeclarations.OfType<Procedure>()) {
+      foreach (var proc in prog.Procedures) {
         List<Requires> newRequires = new List<Requires>();
         foreach (Requires r in proc.Requires) {
           string c;
           if (MatchCandidate(r.Condition, out c)) {
             var cVar = currentHoudiniState.Assignment.Keys.Where(item => item.Name.Equals(c)).ToList()[0];
             if (currentHoudiniState.Assignment[cVar]) {
-              Variable cVarProg = prog.TopLevelDeclarations.OfType<Variable>().Where(item => item.Name.Equals(c)).ToList()[0];
+              Variable cVarProg = prog.Variables.Where(item => item.Name.Equals(c)).ToList()[0];
               Dictionary<Variable, Expr> subst = new Dictionary<Variable, Expr>();
               subst[cVarProg] = Expr.True;
               newRequires.Add(new Requires(Token.NoToken, true,
@@ -1231,7 +1228,7 @@ namespace Microsoft.Boogie.Houdini {
           if (MatchCandidate(e.Condition, out c)) {
             var cVar = currentHoudiniState.Assignment.Keys.Where(item => item.Name.Equals(c)).ToList()[0];
             if (currentHoudiniState.Assignment[cVar]) {
-              Variable cVarProg = prog.TopLevelDeclarations.OfType<Variable>().Where(item => item.Name.Equals(c)).ToList()[0];
+              Variable cVarProg = prog.Variables.Where(item => item.Name.Equals(c)).ToList()[0];
               Dictionary<Variable, Expr> subst = new Dictionary<Variable, Expr>();
               subst[cVarProg] = Expr.True;
               newEnsures.Add(new Ensures(Token.NoToken, true,
diff --git a/Source/Predication/UniformityAnalyser.cs b/Source/Predication/UniformityAnalyser.cs
index 3d6b7b18..ff298942 100644
--- a/Source/Predication/UniformityAnalyser.cs
+++ b/Source/Predication/UniformityAnalyser.cs
@@ -84,7 +84,7 @@ namespace Microsoft.Boogie
 
         public void Analyse()
         {
-            var impls = prog.TopLevelDeclarations.OfType<Implementation>();
+            var impls = prog.Implementations;
 
             foreach (var Impl in impls)
             {
@@ -143,7 +143,7 @@ namespace Microsoft.Boogie
                 ProcedureChanged = true;
             }
 
-            var procs = prog.TopLevelDeclarations.OfType<Procedure>();
+            var procs = prog.Procedures;
 
             foreach (var Proc in procs) {
 
@@ -268,11 +268,11 @@ namespace Microsoft.Boogie
 
         private Procedure GetProcedure(string procedureName)
         {
-            foreach (Declaration D in prog.TopLevelDeclarations)
+            foreach (var p in prog.Procedures)
             {
-                if (D is Procedure && ((D as Procedure).Name == procedureName))
+                if (p.Name == procedureName)
                 {
-                    return D as Procedure;
+                    return p;
                 }
             }
             Debug.Assert(false);
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index 9fc301da..bb34c8f8 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -429,12 +429,8 @@ namespace Microsoft.Boogie {
           }
         }
       }
-      foreach (Declaration decl in prog.TopLevelDeclarations) {
-        Contract.Assert(decl != null);
-        Axiom ax = decl as Axiom;
-        if (ax != null) {
-          ctx.AddAxiom(ax, null);
-        }
+      foreach (var ax in prog.Axioms) {
+        ctx.AddAxiom(ax, null);
       }
       foreach (Declaration decl in prog.TopLevelDeclarations) {
         Contract.Assert(decl != null);
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 50a717f9..e74e0bbf 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -1831,7 +1831,7 @@ namespace VC {
       // global variables
       lock (program.TopLevelDeclarations)
       {
-        foreach (Variable v in program.TopLevelDeclarations.OfType<Variable>())
+        foreach (var v in program.Variables)
         {
           if (!(v is Constant))
           {
diff --git a/Source/VCGeneration/FixedpointVC.cs b/Source/VCGeneration/FixedpointVC.cs
index 9f39e46c..04b976ea 100644
--- a/Source/VCGeneration/FixedpointVC.cs
+++ b/Source/VCGeneration/FixedpointVC.cs
@@ -392,56 +392,42 @@ namespace Microsoft.Boogie
 
         void MarkAllFunctionImplementationsInline()
         {
-            foreach (var d in program.TopLevelDeclarations)
+            foreach (var func in program.Functions)
             {
-                var impl = d as Function;
-                if (impl != null)
+                if (func.Body == null && func.DefinitionAxiom != null)
                 {
-                    if (impl.Body == null && impl.DefinitionAxiom != null)
-                    {
-                        var def = impl.DefinitionAxiom.Expr as QuantifierExpr;
-                        var bod = def.Body as NAryExpr;
-                        impl.Body = bod.Args[1];
-                        impl.DefinitionAxiom = null;
-                    }
-                    if (impl.Body != null)
-                        if (impl.FindExprAttribute("inline") == null)
-                            impl.AddAttribute("inline", Expr.Literal(100));
+                    var def = func.DefinitionAxiom.Expr as QuantifierExpr;
+                    var bod = def.Body as NAryExpr;
+                    func.Body = bod.Args[1];
+                    func.DefinitionAxiom = null;
                 }
+                if (func.Body != null)
+                    if (func.FindExprAttribute("inline") == null)
+                        func.AddAttribute("inline", Expr.Literal(100));
             }
         }
 
         void InlineAll()
         {
-            foreach (var d in program.TopLevelDeclarations)
+            foreach (var impl in program.Implementations)
             {
-                var impl = d as Implementation;
-                if (impl != null)
-                {
-                    impl.OriginalBlocks = impl.Blocks;
-                    impl.OriginalLocVars = impl.LocVars;
-                    if(impl.Name != main_proc_name)
-                      if(impl.FindExprAttribute("inline") == null)
-                        impl.AddAttribute("inline", Expr.Literal(100));
-                }
+                impl.OriginalBlocks = impl.Blocks;
+                impl.OriginalLocVars = impl.LocVars;
+                if(impl.Name != main_proc_name)
+                  if(impl.FindExprAttribute("inline") == null)
+                    impl.AddAttribute("inline", Expr.Literal(100));
             }
-            var decls = program.TopLevelDeclarations;
-            foreach (var d in decls)
+            foreach (var impl in program.Implementations)
             {
-                var impl = d as Implementation;
-                if (impl != null && !impl.SkipVerification)
+                if (!impl.SkipVerification)
                 {
                     Inliner.ProcessImplementation(program, impl);
                 }
             }
-            foreach (var d in program.TopLevelDeclarations)
+            foreach (var impl in program.Implementations)
             {
-                var impl = d as Implementation;
-                if (impl != null)
-                {
-                    impl.OriginalBlocks = null;
-                    impl.OriginalLocVars = null;
-                }
+                impl.OriginalBlocks = null;
+                impl.OriginalLocVars = null;
             }
         }
 
@@ -650,12 +636,8 @@ namespace Microsoft.Boogie
         public void GenerateVCsForStratifiedInlining()
         {
             Contract.Requires(program != null);
-            foreach (Declaration decl in program.TopLevelDeclarations)
+            foreach (var impl in program.Implementations)
             {
-                Contract.Assert(decl != null);
-                Implementation impl = decl as Implementation;
-                if (impl == null)
-                    continue;
                 Contract.Assert(!impl.Name.StartsWith(recordProcName), "Not allowed to have an implementation for this guy");
 
                 Procedure proc = cce.NonNull(impl.Proc);
@@ -713,10 +695,8 @@ namespace Microsoft.Boogie
 
             if (mode == Mode.Boogie) return;
 
-            foreach (var decl in program.TopLevelDeclarations)
+            foreach (var proc in program.Procedures)
             {
-                var proc = decl as Procedure;
-                if (proc == null) continue;
                 if (!proc.Name.StartsWith(recordProcName)) continue;
                 Contract.Assert(proc.InParams.Count == 1);
 
@@ -754,12 +734,8 @@ namespace Microsoft.Boogie
 			foreach (var node in rpfp.nodes)
 				pmap.Add ((node.Name as VCExprBoogieFunctionOp).Func.Name, node);
 			
-			foreach (Declaration decl in program.TopLevelDeclarations)
+			foreach (var impl in program.Implementations)
             {
-                Contract.Assert(decl != null);
-                Implementation impl = decl as Implementation;
-                if (impl == null)
-                    continue;
                 Contract.Assert(!impl.Name.StartsWith(recordProcName), "Not allowed to have an implementation for this guy");
 
                 Procedure proc = cce.NonNull(impl.Proc);
@@ -1400,25 +1376,17 @@ namespace Microsoft.Boogie
 
                 // find the name of the main procedure
                 main_proc_name = null; // default in case no entry point defined
-                foreach (var d in program.TopLevelDeclarations)
+                foreach (var impl in program.Implementations)
                 {
-                    var impl = d as Implementation;
-                    if (impl != null)
-                    {
-                        if (QKeyValue.FindBoolAttribute(impl.Attributes, "entrypoint"))
-                            main_proc_name = impl.Proc.Name;
-                    }
+                    if (QKeyValue.FindBoolAttribute(impl.Attributes, "entrypoint"))
+                        main_proc_name = impl.Proc.Name;
                 }
                 if (main_proc_name == null)
                 {
-                    foreach (var d in program.TopLevelDeclarations)
+                    foreach (var impl in program.Implementations)
                     {
-                        var impl = d as Implementation;
-                        if (impl != null)
-                        {
-                            if (impl.Proc.Name == "main" || impl.Proc.Name.EndsWith(".main"))
-                                main_proc_name = impl.Proc.Name;
-                        }
+                        if (impl.Proc.Name == "main" || impl.Proc.Name.EndsWith(".main"))
+                            main_proc_name = impl.Proc.Name;
                     }
                 }
                 if (main_proc_name == null)
@@ -1428,10 +1396,9 @@ namespace Microsoft.Boogie
                 {
                     InlineAll();
                     Microsoft.Boogie.BlockCoalescer.CoalesceBlocks(program);
-                    foreach (var d in program.TopLevelDeclarations)
+                    foreach (var impl in program.Implementations)
                     {
-                        var impl = d as Implementation;
-                        if (impl != null && main_proc_name == impl.Proc.Name)
+                        if (main_proc_name == impl.Proc.Name)
                         {
                             Microsoft.Boogie.LiveVariableAnalysis.ClearLiveVariables(impl);
                             CyclicLiveVariableAnalysis.ComputeLiveVariables(impl);
@@ -1444,15 +1411,11 @@ namespace Microsoft.Boogie
 
                     if (style == AnnotationStyle.Procedure || style == AnnotationStyle.Call)
                     {
-                        foreach (var proc in program.TopLevelDeclarations)
+                        foreach (var impl in program.Implementations)
                         {
-                            var impl = proc as Implementation;
-                            if (impl != null)
-                            {
-                                if (!QKeyValue.FindBoolAttribute(impl.Attributes, "entrypoint"))
-                                    AnnotateProcRequires(impl.Proc, impl, boogieContext);
-                                AnnotateProcEnsures(impl.Proc, impl, boogieContext);
-                            }
+                            if (!QKeyValue.FindBoolAttribute(impl.Attributes, "entrypoint"))
+                                AnnotateProcRequires(impl.Proc, impl, boogieContext);
+                            AnnotateProcEnsures(impl.Proc, impl, boogieContext);
                         }
                         if (style == AnnotationStyle.Call)
                         {
@@ -1463,40 +1426,30 @@ namespace Microsoft.Boogie
                     // must do this after annotating procedures, else calls
                     // will be prematurely desugared
                     
-                    foreach (var d in program.TopLevelDeclarations)
+                    foreach (var impl in program.Implementations)
                     {
-                        var impl = d as Implementation;
-                        if (impl != null)
-                        {
-                            Microsoft.Boogie.LiveVariableAnalysis.ClearLiveVariables(impl);
-                            CyclicLiveVariableAnalysis.ComputeLiveVariables(impl);
-                        }
+                        Microsoft.Boogie.LiveVariableAnalysis.ClearLiveVariables(impl);
+                        CyclicLiveVariableAnalysis.ComputeLiveVariables(impl);
                     }
 
 
                     if (style == AnnotationStyle.Flat || style == AnnotationStyle.Call)
                     {
-                        foreach (var proc in program.TopLevelDeclarations)
+                        foreach (var impl in program.Implementations)
                         {
-                            var impl = proc as Implementation;
-                            if (impl != null)
-                                AnnotateLoops(impl, boogieContext);
+                            AnnotateLoops(impl, boogieContext);
                         }
                     }
                     if (style == AnnotationStyle.Call)
                     {
                         Dictionary<string, bool> impls = new Dictionary<string, bool>();
-                        foreach (var proc in program.TopLevelDeclarations)
+                        foreach (var impl in program.Implementations)
                         {
-                            var impl = proc as Implementation;
-                            if (impl != null)
-                                impls.Add(impl.Proc.Name, true);
+                            impls.Add(impl.Proc.Name, true);
                         }
-                        foreach (var proc in program.TopLevelDeclarations)
+                        foreach (var impl in program.Implementations)
                         {
-                            var impl = proc as Implementation;
-                            if (impl != null)
-                                AnnotateCallSites(impl, boogieContext, impls);
+                            AnnotateCallSites(impl, boogieContext, impls);
                         }
                     }
                     if (style == AnnotationStyle.Flat)
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index fe40618e..5eed14fd 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -333,18 +333,14 @@ namespace VC {
       : base(program, logFilePath, appendLogFile, checkers) {
       implName2StratifiedInliningInfo = new Dictionary<string, StratifiedInliningInfo>();
       prover = ProverInterface.CreateProver(program, logFilePath, appendLogFile, CommandLineOptions.Clo.ProverKillTime);
-      foreach (Declaration decl in program.TopLevelDeclarations) {
-        Implementation impl = decl as Implementation;
-        if (impl == null) continue;
+      foreach (var impl in program.Implementations) {
         implName2StratifiedInliningInfo[impl.Name] = new StratifiedInliningInfo(impl, this);
       }
       GenerateRecordFunctions();
     }
 
     private void GenerateRecordFunctions() {
-      foreach (var decl in program.TopLevelDeclarations) {
-        var proc = decl as Procedure;
-        if (proc == null) continue;
+      foreach (var proc in program.Procedures) {
         if (!proc.Name.StartsWith(recordProcName)) continue;
         Contract.Assert(proc.InParams.Count == 1);
 
@@ -901,9 +897,7 @@ namespace VC {
 
       // Find all the boolean constants
       var allConsts = new HashSet<VCExprVar>();
-      foreach (var decl in program.TopLevelDeclarations) {
-        var constant = decl as Constant;
-        if (constant == null) continue;
+      foreach (var constant in program.Constants) {
         if (!allBoolVars.Contains(constant.Name)) continue;
         var v = prover.Context.BoogieExprTranslator.LookupVariable(constant);
         allConsts.Add(v);
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 3735388c..758430bd 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -2600,7 +2600,7 @@ namespace VC {
         // where clauses of global variables
         lock (program.TopLevelDeclarations)
         {
-          foreach (var gvar in program.TopLevelDeclarations.OfType<GlobalVariable>())
+          foreach (var gvar in program.GlobalVariables())
           {
             if (gvar != null && gvar.TypedIdent.WhereExpr != null)
             {
@@ -2755,15 +2755,11 @@ namespace VC {
     {
         // Construct the set of inlined procs in the original program
         var inlinedProcs = new HashSet<string>();
-        foreach (var decl in program.TopLevelDeclarations)
+        foreach (var proc in program.Procedures)
         {
-            if (decl is Procedure)
-            {  
-                if (!(decl is LoopProcedure))
-                {
-                    var p = decl as Procedure;
-                    inlinedProcs.Add(p.Name);
-                }
+            if (!(proc is LoopProcedure))
+            {
+                inlinedProcs.Add(proc.Name);
             }
         }
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
parent	2031fb15596b2a114f7b3e0bb85ff838507051a0 (diff)