Eliminated dependencies on SpecSharp and CCI from Boogie.sln and Dafny.sln

8 files changed, 136 insertions, 123 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 8f70766f..64b15be7 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -9,8 +9,8 @@
 namespace Microsoft.Boogie.AbstractInterpretation {

   using System.Diagnostics;

   using System.Diagnostics.Contracts;

-  using CCI = System.Compiler;

   using System.Collections;

+  using System.Collections.Generic;

   using AI = Microsoft.AbstractInterpretationFramework;

 

   public class CallSite {

@@ -45,7 +45,7 @@ namespace Microsoft.Boogie.AbstractInterpretation {
     public AI.Lattice/*!*/ Lattice;

     public AI.Lattice.Element/*!*/ OnEntry;

     public AI.Lattice.Element/*!*/ OnExit;

-    public CCI.IMutableSet/*<CallSite>*//*!*/ ReturnPoints; // whenever OnExit changes, we start analysis again at all the ReturnPoints

+    public HashSet<CallSite>/*!*/ ReturnPoints; // whenever OnExit changes, we start analysis again at all the ReturnPoints

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(Lattice != null);

@@ -61,7 +61,7 @@ namespace Microsoft.Boogie.AbstractInterpretation {
       this.Lattice = lattice;

       this.OnEntry = onEntry;

       this.OnExit = lattice.Bottom;

-      this.ReturnPoints = new CCI.HashSet();

+      this.ReturnPoints = new HashSet<CallSite>();

       // base();

     }

 

@@ -407,7 +407,7 @@ namespace Microsoft.Boogie {
         Hashtable substMap = new Hashtable(); // Variable -> IdentifierExpr

 

         VariableSeq/*!*/ targets = new VariableSeq();

-        Set<Variable> footprint = new Set<Variable>();

+        HashSet<Variable> footprint = new HashSet<Variable>();

 

         foreach (Block/*!*/ b in g.BackEdgeNodes(header))

         {

@@ -422,7 +422,7 @@ namespace Microsoft.Boogie {
 

                     VariableCollector c = new VariableCollector();

                     c.Visit(cmd);

-                    footprint.AddRange(c.usedVars);

+                    footprint.UnionWith(c.usedVars);

                 }

             }

         }

@@ -531,7 +531,7 @@ namespace Microsoft.Boogie {
         Contract.Assert(header != null);

         LoopProcedure loopProc = loopHeaderToLoopProc[header];

         Dictionary<Block, Block> blockMap = new Dictionary<Block, Block>();

-        Set<string> dummyBlocks = new Set<string>();

+        HashSet<string> dummyBlocks = new HashSet<string>();

 

         CodeCopier codeCopier = new CodeCopier(loopHeaderToSubstMap[header]);  // fix me

         VariableSeq inputs = loopHeaderToInputs[header];

@@ -696,7 +696,7 @@ namespace Microsoft.Boogie {
     {

         // Do a BFS to find all reachable blocks

         List<Block> reachableBlocks = new List<Block>();

-        Set<string> visited = new Set<string>();

+        HashSet<string> visited = new HashSet<string>();

         List<Block> worklist = new List<Block>();

 

         visited.Add(impl.Blocks[0].Label);

@@ -2806,7 +2806,7 @@ namespace Microsoft.Boogie {
     public void PruneUnreachableBlocks() {

       ArrayList /*Block!*/ visitNext = new ArrayList /*Block!*/ ();

       List<Block/*!*/> reachableBlocks = new List<Block/*!*/>();

-      System.Compiler.IMutableSet /*Block!*/ reachable = new System.Compiler.HashSet /*Block!*/ ();  // the set of elements in "reachableBlocks"

+      HashSet<Block> reachable = new HashSet<Block>();  // the set of elements in "reachableBlocks"

 

       visitNext.Add(this.Blocks[0]);

       while (visitNext.Count != 0) {

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index 35929311..afd171b9 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -78,7 +78,7 @@ namespace Microsoft.Boogie {
     public readonly IToken/*!*/ EndCurly;

     public StmtList ParentContext;

     public BigBlock ParentBigBlock;

-    public Set<string/*!*/>/*!*/ Labels = new Set<string/*!*/>();

+    public HashSet<string/*!*/>/*!*/ Labels = new HashSet<string/*!*/>();

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(EndCurly != null);

@@ -233,7 +233,7 @@ namespace Microsoft.Boogie {
     List<Block/*!*/> blocks;

     string/*!*/ prefix = "anon";

     int anon = 0;

-    Set<string/*!*/> allLabels = new Set<string/*!*/>();

+    HashSet<string/*!*/> allLabels = new HashSet<string/*!*/>();

     Errors/*!*/ errorHandler;

     [ContractInvariantMethod]

     void ObjectInvariant() {

@@ -784,7 +784,7 @@ namespace Microsoft.Boogie {
     // VC generation and SCC computation

     public BlockSeq/*!*/ Predecessors;

 

-    public Set<Variable/*!*/> liveVarsBefore;

+    public HashSet<Variable/*!*/> liveVarsBefore;

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(Label != null);

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index b63b82cc..42bd1406 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -10,7 +10,6 @@ using System.Collections.Specialized;
 using System.IO;

 using System.Diagnostics;

 using System.Diagnostics.Contracts;

-using Cci = System.Compiler;

 

 namespace Microsoft.Boogie {

   public class CommandLineOptions {

@@ -1543,6 +1542,7 @@ namespace Microsoft.Boogie {
       return Contract.Exists(procsToCheck, s => 0 <= methodFullname.IndexOf(s));

     }

 

+#if CCI

     public bool UserWantsToTranslateRoutine(Cci.Method method, string methodFullname) {

       Contract.Requires(methodFullname != null);

       Contract.Requires(method != null);

@@ -1674,6 +1674,7 @@ namespace Microsoft.Boogie {
       }

       return null;

     }

+#endif

 

     class CommandLineParseState {

       public string s;

diff --git a/Source/Core/Core.csproj b/Source/Core/Core.csproj
index ab4857dc..6cea383c 100644
--- a/Source/Core/Core.csproj
+++ b/Source/Core/Core.csproj
@@ -103,19 +103,7 @@
       <SpecificVersion>False</SpecificVersion>

       <HintPath>..\..\Binaries\FSharp.Core.dll</HintPath>

     </Reference>

-    <Reference Include="Microsoft.SpecSharp.Runtime, Version=1.0.21126.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

-      <HintPath>..\..\Binaries\Microsoft.SpecSharp.Runtime.dll</HintPath>

-    </Reference>

     <Reference Include="System" />

-    <Reference Include="System.Compiler, Version=1.0.21126.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

-      <HintPath>..\..\Binaries\System.Compiler.dll</HintPath>

-    </Reference>

-    <Reference Include="System.Compiler.Framework, Version=1.0.21126.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

-      <HintPath>..\..\Binaries\System.Compiler.Framework.dll</HintPath>

-    </Reference>

     <Reference Include="System.Xml" />

   </ItemGroup>

   <ItemGroup>

diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs
index 694ddc00..40be3798 100644
--- a/Source/Core/DeadVarElim.cs
+++ b/Source/Core/DeadVarElim.cs
@@ -41,7 +41,7 @@ namespace Microsoft.Boogie {
 

   public class ModSetCollector : StandardVisitor {

     static Procedure proc;

-    static Dictionary<Procedure/*!*/, Set<Variable/*!*/>/*!*/>/*!*/ modSets;

+    static Dictionary<Procedure/*!*/, HashSet<Variable/*!*/>/*!*/>/*!*/ modSets;

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(cce.NonNullElements(modSets));

@@ -60,9 +60,9 @@ namespace Microsoft.Boogie {
       }

       Console.WriteLine("Number of procedures = {0}", procCount);

 

-      modSets = new Dictionary<Procedure/*!*/, Set<Variable/*!*/>/*!*/>();

+      modSets = new Dictionary<Procedure/*!*/, HashSet<Variable/*!*/>/*!*/>();

 

-      Set<Procedure/*!*/> implementedProcs = new Set<Procedure/*!*/>();

+      HashSet<Procedure/*!*/> implementedProcs = new HashSet<Procedure/*!*/>();

       foreach (Declaration/*!*/ decl in program.TopLevelDeclarations) {

         Contract.Assert(decl != null);

         if (decl is Implementation) {

@@ -155,7 +155,7 @@ namespace Microsoft.Boogie {
       if (var.Name == "alloc")

         return;

       if (!modSets.ContainsKey(localProc)) {

-        modSets[localProc] = new Set<Variable/*!*/>();

+        modSets[localProc] = new HashSet<Variable/*!*/>();

       }

       if (modSets[localProc].Contains(var))

         return;

@@ -165,8 +165,8 @@ namespace Microsoft.Boogie {
   }

 

   public class VariableCollector : StandardVisitor {

-    public System.Collections.Generic.Set<Variable/*!*/>/*!*/ usedVars;

-    public System.Collections.Generic.Set<Variable/*!*/>/*!*/ oldVarsUsed;

+    public HashSet<Variable/*!*/>/*!*/ usedVars;

+    public HashSet<Variable/*!*/>/*!*/ oldVarsUsed;

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(cce.NonNullElements(usedVars));

@@ -176,8 +176,8 @@ namespace Microsoft.Boogie {
     int insideOldExpr;

 

     public VariableCollector() {

-      usedVars = new System.Collections.Generic.Set<Variable/*!*/>();

-      oldVarsUsed = new System.Collections.Generic.Set<Variable/*!*/>();

+      usedVars = new System.Collections.Generic.HashSet<Variable/*!*/>();

+      oldVarsUsed = new System.Collections.Generic.HashSet<Variable/*!*/>();

       insideOldExpr = 0;

     }

 

@@ -210,11 +210,11 @@ namespace Microsoft.Boogie {
       blockCoalescer.Visit(program);

     }

 

-    private static Set<Block/*!*/>/*!*/ ComputeMultiPredecessorBlocks(Implementation/*!*/ impl) {

+    private static HashSet<Block/*!*/>/*!*/ ComputeMultiPredecessorBlocks(Implementation/*!*/ impl) {

       Contract.Requires(impl != null);

-      Contract.Ensures(cce.NonNullElements(Contract.Result<Set<Block>>()));

-      Set<Block/*!*/> visitedBlocks = new Set<Block/*!*/>();

-      Set<Block/*!*/> multiPredBlocks = new Set<Block/*!*/>();

+      Contract.Ensures(cce.NonNullElements(Contract.Result<HashSet<Block>>()));

+      HashSet<Block/*!*/> visitedBlocks = new HashSet<Block/*!*/>();

+      HashSet<Block/*!*/> multiPredBlocks = new HashSet<Block/*!*/>();

       Stack<Block/*!*/> dfsStack = new Stack<Block/*!*/>();

       dfsStack.Push(impl.Blocks[0]);

       while (dfsStack.Count > 0) {

@@ -247,10 +247,10 @@ namespace Microsoft.Boogie {
       //Console.WriteLine("Procedure {0}", impl.Name);

       //Console.WriteLine("Initial number of blocks = {0}", impl.Blocks.Count);

 

-      Set<Block/*!*/> multiPredBlocks = ComputeMultiPredecessorBlocks(impl);

+      HashSet<Block/*!*/> multiPredBlocks = ComputeMultiPredecessorBlocks(impl);

       Contract.Assert(cce.NonNullElements(multiPredBlocks));

-      Set<Block/*!*/> visitedBlocks = new Set<Block/*!*/>();

-      Set<Block/*!*/> removedBlocks = new Set<Block/*!*/>();

+      HashSet<Block/*!*/> visitedBlocks = new HashSet<Block/*!*/>();

+      HashSet<Block/*!*/> removedBlocks = new HashSet<Block/*!*/>();

       Stack<Block/*!*/> dfsStack = new Stack<Block/*!*/>();

       dfsStack.Push(impl.Blocks[0]);

       while (dfsStack.Count > 0) {

@@ -333,14 +333,14 @@ namespace Microsoft.Boogie {
       IEnumerable<Block> sortedNodes = dag.TopologicalSort();

       foreach (Block/*!*/ block in sortedNodes) {

         Contract.Assert(block != null);

-        Set<Variable/*!*/>/*!*/ liveVarsAfter = new Set<Variable/*!*/>();

+        HashSet<Variable/*!*/>/*!*/ liveVarsAfter = new HashSet<Variable/*!*/>();

         if (block.TransferCmd is GotoCmd) {

           GotoCmd gotoCmd = (GotoCmd)block.TransferCmd;

           if (gotoCmd.labelTargets != null) {

             foreach (Block/*!*/ succ in gotoCmd.labelTargets) {

               Contract.Assert(succ != null);

               Contract.Assert(succ.liveVarsBefore != null);

-              liveVarsAfter.AddRange(succ.liveVarsBefore);

+              liveVarsAfter.UnionWith(succ.liveVarsBefore);

             }

           }

         }

@@ -365,7 +365,7 @@ namespace Microsoft.Boogie {
     }

 

     // perform in place update of liveSet

-    public static void Propagate(Cmd cmd, Set<Variable/*!*/>/*!*/ liveSet) {

+    public static void Propagate(Cmd cmd, HashSet<Variable/*!*/>/*!*/ liveSet) {

       Contract.Requires(cmd != null);

       Contract.Requires(cce.NonNullElements(liveSet));

       if (cmd is AssignCmd) {

@@ -373,7 +373,7 @@ namespace Microsoft.Boogie {
         // I must first iterate over all the targets and remove the live ones.

         // After the removals are done, I must add the variables referred on 

         // the right side of the removed targets

-        Set<int> indexSet = new Set<int>();

+        HashSet<int> indexSet = new HashSet<int>();

         int index = 0;

         foreach (AssignLhs/*!*/ lhs in assignCmd.Lhss) {

           Contract.Assert(lhs != null);

@@ -394,7 +394,7 @@ namespace Microsoft.Boogie {
           if (indexSet.Contains(index)) {

             VariableCollector/*!*/ collector = new VariableCollector();

             collector.Visit(expr);

-            liveSet.AddRange(collector.usedVars);

+            liveSet.UnionWith(collector.usedVars);

             AssignLhs lhs = assignCmd.Lhss[index];

             if (lhs is MapAssignLhs) {

               // If the target is a map, then all indices are also read

@@ -402,7 +402,7 @@ namespace Microsoft.Boogie {
               foreach (Expr e in malhs.Indexes) {

                 VariableCollector/*!*/ c = new VariableCollector();

                 c.Visit(e);

-                liveSet.AddRange(c.usedVars);

+                liveSet.UnionWith(c.usedVars);

               }

             }

           }

@@ -427,7 +427,7 @@ namespace Microsoft.Boogie {
         } else {

           VariableCollector/*!*/ collector = new VariableCollector();

           collector.Visit(predicateCmd.Expr);

-          liveSet.AddRange(collector.usedVars);

+          liveSet.UnionWith(collector.usedVars);

         }

       } else if (cmd is CommentCmd) {

         // comments are just for debugging and don't affect verification

@@ -470,8 +470,8 @@ namespace Microsoft.Boogie {
 

   public class GenKillWeight {

     // lambda S. (S - kill) union gen

-    Set<Variable/*!*/>/*!*/ gen;

-    Set<Variable/*!*/>/*!*/ kill;

+    HashSet<Variable/*!*/>/*!*/ gen;

+    HashSet<Variable/*!*/>/*!*/ kill;

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(cce.NonNullElements(gen));

@@ -482,17 +482,17 @@ namespace Microsoft.Boogie {
 

     bool isZero;

 

-    public static GenKillWeight/*!*/ oneWeight = new GenKillWeight(new Set<Variable/*!*/>(), new Set<Variable/*!*/>());

+    public static GenKillWeight/*!*/ oneWeight = new GenKillWeight(new HashSet<Variable/*!*/>(), new HashSet<Variable/*!*/>());

     public static GenKillWeight/*!*/ zeroWeight = new GenKillWeight();

 

     // initializes to zero

     public GenKillWeight() {

       this.isZero = true;

-      this.gen = new Set<Variable/*!*/>();

-      this.kill = new Set<Variable/*!*/>();

+      this.gen = new HashSet<Variable/*!*/>();

+      this.kill = new HashSet<Variable/*!*/>();

     }

 

-    public GenKillWeight(Set<Variable/*!*/> gen, Set<Variable/*!*/> kill) {

+    public GenKillWeight(HashSet<Variable/*!*/> gen, HashSet<Variable/*!*/> kill) {

       Contract.Requires(cce.NonNullElements(gen));

       Contract.Requires(cce.NonNullElements(kill));

       Contract.Assert(gen != null);

@@ -519,7 +519,14 @@ namespace Microsoft.Boogie {
       if (w1.isZero || w2.isZero)

         return zero();

 

-      return new GenKillWeight(w1.gen.Union(w2.gen.Difference(w1.kill)), w1.kill.Union(w2.kill));

+      HashSet<Variable> t = new HashSet<Variable>(w2.gen);

+      t.ExceptWith(w1.kill);

+      HashSet<Variable> g = new HashSet<Variable>(w1.gen);

+      g.UnionWith(t);

+      HashSet<Variable> k = new HashSet<Variable>(w1.kill);

+      k.UnionWith(w2.kill);

+      return new GenKillWeight(g, k);

+      //return new GenKillWeight(w1.gen.Union(w2.gen.Difference(w1.kill)), w1.kill.Union(w2.kill));

     }

 

     public static GenKillWeight combine(GenKillWeight w1, GenKillWeight w2) {

@@ -531,16 +538,29 @@ namespace Microsoft.Boogie {
       if (w2.isZero)

         return w1;

 

-      return new GenKillWeight(w1.gen.Union(w2.gen), w1.kill.Intersection(w2.kill));

+      HashSet<Variable> g = new HashSet<Variable>(w1.gen);

+      g.UnionWith(w2.gen);

+      HashSet<Variable> k = new HashSet<Variable>(w1.kill);

+      k.IntersectWith(w2.kill);

+      return new GenKillWeight(g, k);

+      //return new GenKillWeight(w1.gen.Union(w2.gen), w1.kill.Intersection(w2.kill));

     }

 

     public static GenKillWeight projectLocals(GenKillWeight w) {

       Contract.Requires(w != null);

       Contract.Ensures(Contract.Result<GenKillWeight>() != null);

-      Set<Variable/*!*/> gen = w.gen.FindAll(isGlobal);

-      Contract.Assert(cce.NonNullElements(gen));

-      Set<Variable/*!*/> kill = w.kill.FindAll(isGlobal);

-      Contract.Assert(cce.NonNullElements(kill));

+      HashSet<Variable/*!*/> gen = new HashSet<Variable>();

+      foreach (Variable v in w.gen)

+      {

+          if (isGlobal(v))

+              gen.Add(v);

+      }

+      HashSet<Variable/*!*/> kill = new HashSet<Variable>();

+      foreach (Variable v in w.kill)

+      {

+          if (isGlobal(v))

+              kill.Add(v);

+      }

 

       return new GenKillWeight(gen, kill);

     }

@@ -567,16 +587,18 @@ namespace Microsoft.Boogie {
       return string.Format("({0},{1})", gen.ToString(), kill.ToString());

     }

 

-    public Set<Variable/*!*/>/*!*/ getLiveVars() {

-      Contract.Ensures(cce.NonNullElements(Contract.Result<Set<Variable>>()));

+    public HashSet<Variable/*!*/>/*!*/ getLiveVars() {

+      Contract.Ensures(cce.NonNullElements(Contract.Result<HashSet<Variable>>()));

       return gen;

     }

 

-    public Set<Variable/*!*/>/*!*/ getLiveVars(Set<Variable/*!*/>/*!*/ lv) {

+    public HashSet<Variable/*!*/>/*!*/ getLiveVars(HashSet<Variable/*!*/>/*!*/ lv) {

       Contract.Requires(cce.NonNullElements(lv));

-      Contract.Ensures(cce.NonNullElements(Contract.Result<Set<Variable>>()));

-      Set<Variable/*!*/>/*!*/ temp = cce.NonNull(lv.Difference(kill));

-      return cce.NonNull(temp.Union(gen));

+      Contract.Ensures(cce.NonNullElements(Contract.Result<HashSet<Variable>>()));

+      HashSet<Variable> temp = new HashSet<Variable>(lv);

+      temp.ExceptWith(kill);

+      temp.UnionWith(gen);

+      return temp;

     }

 

   }

@@ -585,18 +607,18 @@ namespace Microsoft.Boogie {
     public Graph<Block/*!*/>/*!*/ graph;

     // Map from procedure to the list of blocks that call that procedure

     public Dictionary<string/*!*/, List<Block/*!*/>/*!*/>/*!*/ procsCalled;

-    public Set<Block/*!*/>/*!*/ nodes;

-    public Dictionary<Block/*!*/, Set<Block/*!*/>/*!*/>/*!*/ succEdges;

-    public Dictionary<Block/*!*/, Set<Block/*!*/>/*!*/>/*!*/ predEdges;

+    public HashSet<Block/*!*/>/*!*/ nodes;

+    public Dictionary<Block/*!*/, HashSet<Block/*!*/>/*!*/>/*!*/ succEdges;

+    public Dictionary<Block/*!*/, HashSet<Block/*!*/>/*!*/>/*!*/ predEdges;

     private Dictionary<Block/*!*/, int>/*!*/ priority;

 

-    public Set<Block/*!*/>/*!*/ srcNodes;

-    public Set<Block/*!*/>/*!*/ exitNodes;

+    public HashSet<Block/*!*/>/*!*/ srcNodes;

+    public HashSet<Block/*!*/>/*!*/ exitNodes;

 

     public Dictionary<Block/*!*/, GenKillWeight/*!*/>/*!*/ weightBefore;

     public Dictionary<Block/*!*/, GenKillWeight/*!*/>/*!*/ weightAfter;

-    public Dictionary<Block/*!*/, Set<Variable/*!*/>/*!*/>/*!*/ liveVarsAfter;

-    public Dictionary<Block/*!*/, Set<Variable/*!*/>/*!*/>/*!*/ liveVarsBefore;

+    public Dictionary<Block/*!*/, HashSet<Variable/*!*/>/*!*/>/*!*/ liveVarsAfter;

+    public Dictionary<Block/*!*/, HashSet<Variable/*!*/>/*!*/>/*!*/ liveVarsBefore;

 

     public GenKillWeight/*!*/ summary;

     public Implementation/*!*/ impl;

@@ -624,19 +646,19 @@ namespace Microsoft.Boogie {
       Contract.Requires(impl != null);

       this.graph = new Graph<Block/*!*/>();

       this.procsCalled = new Dictionary<string/*!*/, List<Block/*!*/>/*!*/>();

-      this.nodes = new Set<Block/*!*/>();

-      this.succEdges = new Dictionary<Block/*!*/, Set<Block/*!*/>/*!*/>();

-      this.predEdges = new Dictionary<Block/*!*/, Set<Block/*!*/>/*!*/>();

+      this.nodes = new HashSet<Block/*!*/>();

+      this.succEdges = new Dictionary<Block/*!*/, HashSet<Block/*!*/>/*!*/>();

+      this.predEdges = new Dictionary<Block/*!*/, HashSet<Block/*!*/>/*!*/>();

 

       this.priority = new Dictionary<Block/*!*/, int>();

 

-      this.srcNodes = new Set<Block/*!*/>();

-      this.exitNodes = new Set<Block/*!*/>();

+      this.srcNodes = new HashSet<Block/*!*/>();

+      this.exitNodes = new HashSet<Block/*!*/>();

 

       this.weightBefore = new Dictionary<Block/*!*/, GenKillWeight/*!*/>();

       this.weightAfter = new Dictionary<Block/*!*/, GenKillWeight/*!*/>();

-      this.liveVarsAfter = new Dictionary<Block/*!*/, Set<Variable/*!*/>/*!*/>();

-      this.liveVarsBefore = new Dictionary<Block/*!*/, Set<Variable/*!*/>/*!*/>();

+      this.liveVarsAfter = new Dictionary<Block/*!*/, HashSet<Variable/*!*/>/*!*/>();

+      this.liveVarsBefore = new Dictionary<Block/*!*/, HashSet<Variable/*!*/>/*!*/>();

 

       summary = GenKillWeight.zero();

       this.impl = impl;

@@ -725,11 +747,11 @@ namespace Microsoft.Boogie {
     private void registerNode(Block b) {

       Contract.Requires(b != null);

       if (!succEdges.ContainsKey(b)) {

-        succEdges.Add(b, new Set<Block/*!*/>());

+        succEdges.Add(b, new HashSet<Block/*!*/>());

       }

 

       if (!predEdges.ContainsKey(b)) {

-        predEdges.Add(b, new Set<Block/*!*/>());

+        predEdges.Add(b, new HashSet<Block/*!*/>());

       }

 

       nodes.Add(b);

@@ -762,8 +784,8 @@ namespace Microsoft.Boogie {
 

     Implementation/*!*/ mainImpl;

 

-    static Dictionary<string/*!*/, Set<Variable/*!*/>/*!*/>/*!*/ varsLiveAtExit = new Dictionary<string/*!*/, Set<Variable/*!*/>/*!*/>();

-    static Dictionary<string/*!*/, Set<Variable/*!*/>/*!*/>/*!*/ varsLiveAtEntry = new Dictionary<string/*!*/, Set<Variable/*!*/>/*!*/>();

+    static Dictionary<string/*!*/, HashSet<Variable/*!*/>/*!*/>/*!*/ varsLiveAtExit = new Dictionary<string/*!*/, HashSet<Variable/*!*/>/*!*/>();

+    static Dictionary<string/*!*/, HashSet<Variable/*!*/>/*!*/>/*!*/ varsLiveAtEntry = new Dictionary<string/*!*/, HashSet<Variable/*!*/>/*!*/>();

     static Dictionary<string/*!*/, GenKillWeight/*!*/>/*!*/ varsLiveSummary = new Dictionary<string/*!*/, GenKillWeight/*!*/>();

     [ContractInvariantMethod]

     void ObjectInvariant() {

@@ -875,15 +897,15 @@ namespace Microsoft.Boogie {
 

     }

 

-    public static Set<Variable/*!*/>/*!*/ GetVarsLiveAtExit(Implementation impl, Program prog) {

+    public static HashSet<Variable/*!*/>/*!*/ GetVarsLiveAtExit(Implementation impl, Program prog) {

       Contract.Requires(prog != null);

       Contract.Requires(impl != null);

-      Contract.Ensures(cce.NonNullElements(Contract.Result<Set<Variable>>()));

+      Contract.Ensures(cce.NonNullElements(Contract.Result<HashSet<Variable>>()));

       if (varsLiveAtExit.ContainsKey(impl.Name)) {

         return varsLiveAtExit[impl.Name];

       }

       // Return default: all globals and out params

-      Set<Variable/*!*/>/*!*/ lv = new Set<Variable/*!*/>();

+      HashSet<Variable/*!*/>/*!*/ lv = new HashSet<Variable/*!*/>();

       foreach (Variable/*!*/ v in prog.GlobalVariables()) {

         Contract.Assert(v != null);

         lv.Add(v);

@@ -895,15 +917,15 @@ namespace Microsoft.Boogie {
       return lv;

     }

 

-    public static Set<Variable/*!*/>/*!*/ GetVarsLiveAtEntry(Implementation impl, Program prog) {

+    public static HashSet<Variable/*!*/>/*!*/ GetVarsLiveAtEntry(Implementation impl, Program prog) {

       Contract.Requires(prog != null);

       Contract.Requires(impl != null);

-      Contract.Ensures(cce.NonNullElements(Contract.Result<Set<Variable>>()));

+      Contract.Ensures(cce.NonNullElements(Contract.Result<HashSet<Variable>>()));

       if (varsLiveAtEntry.ContainsKey(impl.Name)) {

         return varsLiveAtEntry[impl.Name];

       }

       // Return default: all globals and in params

-      Set<Variable/*!*/>/*!*/ lv = new Set<Variable/*!*/>();

+      HashSet<Variable/*!*/>/*!*/ lv = new HashSet<Variable/*!*/>();

       foreach (Variable/*!*/ v in prog.GlobalVariables()) {

         Contract.Assert(v != null);

         lv.Add(v);

@@ -920,10 +942,10 @@ namespace Microsoft.Boogie {
       return varsLiveSummary.ContainsKey(name);

     }

 

-    public static Set<Variable/*!*/>/*!*/ PropagateLiveVarsAcrossCall(CallCmd cmd, Set<Variable/*!*/>/*!*/ lvAfter) {

+    public static HashSet<Variable/*!*/>/*!*/ PropagateLiveVarsAcrossCall(CallCmd cmd, HashSet<Variable/*!*/>/*!*/ lvAfter) {

       Contract.Requires(cmd != null);

       Contract.Requires(cce.NonNullElements(lvAfter));

-      Contract.Ensures(cce.NonNullElements(Contract.Result<Set<Variable>>()));

+      Contract.Ensures(cce.NonNullElements(Contract.Result<HashSet<Variable>>()));

       Procedure/*!*/ proc = cce.NonNull(cmd.Proc);

       if (varsLiveSummary.ContainsKey(proc.Name)) {

         GenKillWeight/*!*/ w1 = getWeightBeforeCall(cmd);

@@ -936,8 +958,8 @@ namespace Microsoft.Boogie {
         Contract.Assert(w != null);

         return w.getLiveVars(lvAfter);

       }

-      Set<Variable/*!*/>/*!*/ ret = new Set<Variable/*!*/>();

-      ret.AddRange(lvAfter);

+      HashSet<Variable/*!*/>/*!*/ ret = new HashSet<Variable/*!*/>();

+      ret.UnionWith(lvAfter);

       LiveVariableAnalysis.Propagate(cmd, ret);

       return ret;

     }

@@ -1014,7 +1036,7 @@ namespace Microsoft.Boogie {
 

     class WorkList {

       SortedList<int, int>/*!*/ priorities;

-      Set<string/*!*/>/*!*/ labels;

+      HashSet<string/*!*/>/*!*/ labels;

 

       Dictionary<int, List<WorkItem/*!*/>/*!*/>/*!*/ workList;

       [ContractInvariantMethod]

@@ -1027,7 +1049,7 @@ namespace Microsoft.Boogie {
 

 

       public WorkList() {

-        labels = new Set<string/*!*/>();

+        labels = new HashSet<string/*!*/>();

         priorities = new SortedList<int, int>();

         workList = new Dictionary<int, List<WorkItem/*!*/>/*!*/>();

       }

@@ -1127,8 +1149,8 @@ namespace Microsoft.Boogie {
         Contract.Assert(cfg != null);

         foreach (Block/*!*/ b in cfg.nodes) {

           Contract.Assert(b != null);

-          cfg.liveVarsAfter.Add(b, new Set<Variable/*!*/>());

-          cfg.liveVarsBefore.Add(b, new Set<Variable/*!*/>());

+          cfg.liveVarsAfter.Add(b, new HashSet<Variable/*!*/>());

+          cfg.liveVarsBefore.Add(b, new HashSet<Variable/*!*/>());

         }

       }

 

@@ -1150,16 +1172,16 @@ namespace Microsoft.Boogie {
       // Set live variable info

       foreach (ICFG/*!*/ cfg in procICFG.Values) {

         Contract.Assert(cfg != null);

-        Set<Variable/*!*/>/*!*/ lv = new Set<Variable/*!*/>();

+        HashSet<Variable/*!*/>/*!*/ lv = new HashSet<Variable/*!*/>();

         foreach (Block/*!*/ eb in cfg.exitNodes) {

           Contract.Assert(eb != null);

-          lv.AddRange(cfg.liveVarsAfter[eb]);

+          lv.UnionWith(cfg.liveVarsAfter[eb]);

         }

         varsLiveAtExit.Add(cfg.impl.Name, lv);

-        lv = new Set<Variable/*!*/>();

+        lv = new HashSet<Variable/*!*/>();

         foreach (Block/*!*/ eb in cfg.srcNodes) {

           Contract.Assert(eb != null);

-          lv.AddRange(cfg.liveVarsBefore[eb]);

+          lv.UnionWith(cfg.liveVarsBefore[eb]);

         }

         varsLiveAtEntry.Add(cfg.impl.Name, lv);

         varsLiveSummary.Add(cfg.impl.Name, cfg.summary);

@@ -1186,11 +1208,11 @@ b.liveVarsBefore = procICFG[mainImpl.Name].liveVarsAfter[b];
       Contract.Assert(cfg != null);

       Block/*!*/ block = wi.block;

       Contract.Assert(block != null);

-      Set<Variable/*!*/>/*!*/ lv = cfg.liveVarsAfter[block];

+      HashSet<Variable/*!*/>/*!*/ lv = cfg.liveVarsAfter[block];

       Contract.Assert(cce.NonNullElements(lv));

       // Propagate backwards in the block

-      Set<Variable/*!*/>/*!*/ prop = new Set<Variable/*!*/>();

-      prop.AddRange(lv);

+      HashSet<Variable/*!*/>/*!*/ prop = new HashSet<Variable/*!*/>();

+      prop.UnionWith(lv);

       for (int i = block.Cmds.Length - 1; i >= 0; i--) {

         Cmd/*!*/ cmd = block.Cmds[i];

         Contract.Assert(cmd != null);

@@ -1202,7 +1224,7 @@ b.liveVarsBefore = procICFG[mainImpl.Name].liveVarsAfter[b];
             Contract.Assert(callee != null);

             // Inter propagation

             // Remove local variables; add return variables

-            Set<Variable/*!*/>/*!*/ elv = new Set<Variable/*!*/>();

+            HashSet<Variable/*!*/>/*!*/ elv = new HashSet<Variable/*!*/>();

             foreach (Variable/*!*/ v in prop) {

               Contract.Assert(v != null);

               if (v is GlobalVariable)

@@ -1215,7 +1237,7 @@ b.liveVarsBefore = procICFG[mainImpl.Name].liveVarsAfter[b];
 

             foreach (Block/*!*/ eb in callee.exitNodes) {

               Contract.Assert(eb != null);

-              callee.liveVarsAfter[eb].AddRange(elv);

+              callee.liveVarsAfter[eb].UnionWith(elv);

               // TODO: check if modified before inserting

               AddToWorkListReverse(new WorkItem(callee, eb));

             }

@@ -1231,13 +1253,14 @@ b.liveVarsBefore = procICFG[mainImpl.Name].liveVarsAfter[b];
         }

       }

 

-      cfg.liveVarsBefore[block].AddRange(prop);

+      cfg.liveVarsBefore[block].UnionWith(prop);

 

       foreach (Block/*!*/ b in cfg.predEdges[block]) {

         Contract.Assert(b != null);

-        Set<Variable/*!*/>/*!*/ prev = cfg.liveVarsAfter[b];

+        HashSet<Variable/*!*/>/*!*/ prev = cfg.liveVarsAfter[b];

         Contract.Assert(cce.NonNullElements(prev));

-        Set<Variable/*!*/>/*!*/ curr = cce.NonNull(prev.Union(cfg.liveVarsBefore[block]));

+        HashSet<Variable/*!*/>/*!*/ curr = new HashSet<Variable>(prev);

+        curr.UnionWith(cfg.liveVarsBefore[block]);

         Contract.Assert(cce.NonNullElements(curr));

         if (curr.Count != prev.Count) {

           cfg.liveVarsAfter[b] = curr;

@@ -1323,8 +1346,8 @@ b.liveVarsBefore = procICFG[mainImpl.Name].liveVarsAfter[b];
       if (weightCache.ContainsKey(cmd))

         return weightCache[cmd];

 

-      Set<Variable/*!*/>/*!*/ gen = new Set<Variable/*!*/>();

-      Set<Variable/*!*/>/*!*/ kill = new Set<Variable/*!*/>();

+      HashSet<Variable/*!*/>/*!*/ gen = new HashSet<Variable/*!*/>();

+      HashSet<Variable/*!*/>/*!*/ kill = new HashSet<Variable/*!*/>();

       GenKillWeight/*!*/ ret;

 

       if (cmd is AssignCmd) {

@@ -1349,7 +1372,7 @@ b.liveVarsBefore = procICFG[mainImpl.Name].liveVarsAfter[b];
           Contract.Assert(expr != null);

           VariableCollector/*!*/ collector = new VariableCollector();

           collector.Visit(expr);

-          gen.AddRange(collector.usedVars);

+          gen.UnionWith(collector.usedVars);

           AssignLhs lhs = assignCmd.Lhss[index];

           if (lhs is MapAssignLhs) {

             // If the target is a map, then all indices are also read

@@ -1357,7 +1380,7 @@ b.liveVarsBefore = procICFG[mainImpl.Name].liveVarsAfter[b];
             foreach (Expr e in malhs.Indexes) {

               VariableCollector/*!*/ c = new VariableCollector();

               c.Visit(e);

-              gen.AddRange(c.usedVars);

+              gen.UnionWith(c.usedVars);

             }

           }

           index++;

@@ -1396,7 +1419,7 @@ b.liveVarsBefore = procICFG[mainImpl.Name].liveVarsAfter[b];
         } else {

           VariableCollector/*!*/ collector = new VariableCollector();

           collector.Visit(predicateCmd.Expr);

-          gen.AddRange(collector.usedVars);

+          gen.UnionWith(collector.usedVars);

         }

         ret = new GenKillWeight(gen, kill);

       } else if (cmd is CommentCmd) {

@@ -1444,8 +1467,8 @@ b.liveVarsBefore = procICFG[mainImpl.Name].liveVarsAfter[b];
       if (weightCacheAfterCall.ContainsKey(cmd))

         return weightCacheAfterCall[cmd];

 

-      Set<Variable/*!*/>/*!*/ gen = new Set<Variable/*!*/>();

-      Set<Variable/*!*/>/*!*/ kill = new Set<Variable/*!*/>();

+      HashSet<Variable/*!*/>/*!*/ gen = new HashSet<Variable/*!*/>();

+      HashSet<Variable/*!*/>/*!*/ kill = new HashSet<Variable/*!*/>();

 

       Contract.Assert(cmd is CallCmd);

       CallCmd/*!*/ ccmd = cce.NonNull((CallCmd)cmd);

@@ -1482,15 +1505,15 @@ b.liveVarsBefore = procICFG[mainImpl.Name].liveVarsAfter[b];
       if (weightCacheBeforeCall.ContainsKey(cmd))

         return weightCacheBeforeCall[cmd];

 

-      Set<Variable/*!*/>/*!*/ gen = new Set<Variable/*!*/>();

-      Set<Variable/*!*/>/*!*/ kill = new Set<Variable/*!*/>();

+      HashSet<Variable/*!*/>/*!*/ gen = new HashSet<Variable/*!*/>();

+      HashSet<Variable/*!*/>/*!*/ kill = new HashSet<Variable/*!*/>();

       CallCmd/*!*/ ccmd = cce.NonNull((CallCmd/*!*/)cmd);

 

       foreach (Expr/*!*/ expr in ccmd.Ins) {

         Contract.Assert(expr != null);

         VariableCollector/*!*/ collector = new VariableCollector();

         collector.Visit(expr);

-        gen.AddRange(collector.usedVars);

+        gen.UnionWith(collector.usedVars);

       }

 

       Contract.Assert(ccmd.Proc != null);

diff --git a/Source/Core/LoopUnroll.cs b/Source/Core/LoopUnroll.cs
index cfadd2b2..6976e281 100644
--- a/Source/Core/LoopUnroll.cs
+++ b/Source/Core/LoopUnroll.cs
@@ -5,7 +5,6 @@
 //-----------------------------------------------------------------------------

 using System.Diagnostics.Contracts;

 using System.Collections.Generic;

-using Cci = System.Compiler;

 using Bpl = Microsoft.Boogie;

 

 namespace Microsoft.Boogie {

@@ -16,7 +15,7 @@ namespace Microsoft.Boogie {
       Contract.Requires(0 <= unrollMaxDepth);

       Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>()));

       Dictionary<Block, GraphNode/*!*/> gd = new Dictionary<Block, GraphNode/*!*/>();

-      Cci.HashSet/*Block*//*!*/ beingVisited = new Cci.HashSet/*Block*/();

+      HashSet<Block> beingVisited = new HashSet<Block>();

       GraphNode gStart = GraphNode.ComputeGraphInfo(null, start, gd, beingVisited);

 

       // Compute SCCs

@@ -106,7 +105,7 @@ namespace Microsoft.Boogie {
         return cmds;

       }

 

-      public static GraphNode ComputeGraphInfo(GraphNode from, Block b, Dictionary<Block/*!*/, GraphNode/*!*/>/*!*/ gd, Cci.HashSet/*Block*/ beingVisited) {

+      public static GraphNode ComputeGraphInfo(GraphNode from, Block b, Dictionary<Block/*!*/, GraphNode/*!*/>/*!*/ gd, HashSet<Block> beingVisited) {

         Contract.Requires(beingVisited != null);

         Contract.Requires(b != null);

         Contract.Requires(cce.NonNullElements(gd));

diff --git a/Source/Core/ResolutionContext.cs b/Source/Core/ResolutionContext.cs
index 93018097..d4b353ef 100644
--- a/Source/Core/ResolutionContext.cs
+++ b/Source/Core/ResolutionContext.cs
@@ -7,7 +7,6 @@ namespace Microsoft.Boogie {
   using System.Collections;

   using System.Collections.Generic;

   using System;

-  using Microsoft.SpecSharp.Collections;

   using System.Diagnostics.Contracts;

 

   [ContractClass(typeof(IErrorSinkContracts))]

diff --git a/Source/Core/Xml.cs b/Source/Core/Xml.cs
index 8fca82f8..e0b909fe 100644
--- a/Source/Core/Xml.cs
+++ b/Source/Core/Xml.cs
@@ -8,7 +8,6 @@ using System.IO;
 using System.Xml;

 using System.Collections.Generic;

 using System.Diagnostics.Contracts;

-using Cci = System.Compiler;

 namespace Microsoft.Boogie {

 

   public class XmlSink {

@@ -143,6 +142,7 @@ namespace Microsoft.Boogie {
       cce.EndExpose();

     }

 

+#if CCI

     public void WriteError(string message, Cci.Node offendingNode, BlockSeq trace) {

       Contract.Requires(offendingNode != null);

       Contract.Requires(message != null);

@@ -177,6 +177,7 @@ namespace Microsoft.Boogie {
       }

       cce.EndExpose();

     }

+#endif

 

     [Inside]

     private void WriteTokenAttributes(IToken tok) {

@@ -189,6 +190,7 @@ namespace Microsoft.Boogie {
       }

     }

 

+#if CCI

     [Inside]

     private void WriteTokenAttributes(Cci.Node node) {

       Contract.Requires(node != null);

@@ -201,6 +203,7 @@ namespace Microsoft.Boogie {
         wr.WriteAttributeString("column", node.SourceContext.StartColumn.ToString());

       }

     }

+#endif

 

     public void WriteStartInference(string inferenceName) {

       Contract.Requires(inferenceName != null);