Make set iteration order deterministic

Make the set class generic

8 files changed, 26 insertions, 20 deletions

diff --git a/Source/AIFramework/Lattice.cs b/Source/AIFramework/Lattice.cs
index 005c9b17..ab10be9a 100644
--- a/Source/AIFramework/Lattice.cs
+++ b/Source/AIFramework/Lattice.cs
@@ -11,11 +11,12 @@ namespace Microsoft.AbstractInterpretationFramework {
   using System.Diagnostics;

   using Microsoft.AbstractInterpretationFramework.Collections;

   using Microsoft.Boogie;

-  using IMutableSet = Microsoft.Boogie.Set;

-  using ISet = Microsoft.Boogie.Set;

-  using HashSet = Microsoft.Boogie.Set;

-  using ArraySet = Microsoft.Boogie.Set;

 

+  using ArraySet = Microsoft.Boogie.GSet<object>;
+  using IMutableSet = Microsoft.Boogie.GSet<object>; 

+  using HashSet = Microsoft.Boogie.GSet<object>;

+  using ISet = Microsoft.Boogie.GSet<object>;

+  using Set = Microsoft.Boogie.GSet<object>;

 

 

   /// <summary>

diff --git a/Source/AIFramework/MultiLattice.cs b/Source/AIFramework/MultiLattice.cs
index 9071bd4c..ba9aa752 100644
--- a/Source/AIFramework/MultiLattice.cs
+++ b/Source/AIFramework/MultiLattice.cs
@@ -11,7 +11,9 @@ namespace Microsoft.AbstractInterpretationFramework {
   using Microsoft.AbstractInterpretationFramework.Collections;

 

   using Microsoft.Boogie;

-  using ISet = Microsoft.Boogie.Set;

+

+  using ISet = Microsoft.Boogie.GSet<object>;

+  using Set = Microsoft.Boogie.GSet<object>;

 

 

   /// <summary>

diff --git a/Source/AIFramework/Mutable.cs b/Source/AIFramework/Mutable.cs
index 232909e4..7592aa6a 100644
--- a/Source/AIFramework/Mutable.cs
+++ b/Source/AIFramework/Mutable.cs
@@ -11,7 +11,7 @@ namespace Microsoft.AbstractInterpretationFramework.Collections {
   /// <summary>

   ///  Extend sets for using as a IWorkList.

   /// </summary>

-  public class WorkSet : Microsoft.Boogie.Set, Microsoft.Boogie.IWorkList {

+  public class WorkSet : Microsoft.Boogie.GSet<object>, Microsoft.Boogie.IWorkList {

 

     // See Bug #148 for an explanation of why this is here.

     // Without it, the contract inheritance rules will complain since it

diff --git a/Source/AIFramework/Polyhedra/LinearConstraint.cs b/Source/AIFramework/Polyhedra/LinearConstraint.cs
index 5d1cabd5..ab5e14f8 100644
--- a/Source/AIFramework/Polyhedra/LinearConstraint.cs
+++ b/Source/AIFramework/Polyhedra/LinearConstraint.cs
@@ -9,9 +9,10 @@ namespace Microsoft.AbstractInterpretationFramework {
   //using System.Compiler;

   using System.Collections;

   using Microsoft.Basetypes;

-  using IMutableSet = Microsoft.Boogie.Set;

-  using HashSet = Microsoft.Boogie.Set;

-  using ISet = Microsoft.Boogie.Set;

+  using Set = Microsoft.Boogie.GSet<object>;
+  using IMutableSet = Microsoft.Boogie.GSet<object>; 

+  using HashSet = Microsoft.Boogie.GSet<object>;

+  using ISet = Microsoft.Boogie.GSet<object>;

 

 

   /// <summary>

diff --git a/Source/AIFramework/Polyhedra/LinearConstraintSystem.cs b/Source/AIFramework/Polyhedra/LinearConstraintSystem.cs
index 299d49cf..74e36eae 100644
--- a/Source/AIFramework/Polyhedra/LinearConstraintSystem.cs
+++ b/Source/AIFramework/Polyhedra/LinearConstraintSystem.cs
@@ -11,9 +11,10 @@ namespace Microsoft.AbstractInterpretationFramework {
   //using Microsoft.SpecSharp.Collections;

   using System.Diagnostics.Contracts;

   using Microsoft.Basetypes;

-  using IMutableSet = Microsoft.Boogie.Set;

-  using HashSet = Microsoft.Boogie.Set;

-  using ISet = Microsoft.Boogie.Set;

+

+  using IMutableSet = Microsoft.Boogie.GSet<object>;

+  using ISet = Microsoft.Boogie.GSet<object>;

+  using HashSet = Microsoft.Boogie.GSet<object>;

 

   /// <summary>

   /// Represents a system of linear constraints (constraint/frame representations).

diff --git a/Source/AIFramework/Polyhedra/PolyhedraAbstraction.cs b/Source/AIFramework/Polyhedra/PolyhedraAbstraction.cs
index 44abfed6..06c0f483 100644
--- a/Source/AIFramework/Polyhedra/PolyhedraAbstraction.cs
+++ b/Source/AIFramework/Polyhedra/PolyhedraAbstraction.cs
@@ -11,9 +11,8 @@ namespace Microsoft.AbstractInterpretationFramework {
   using System.Diagnostics.Contracts;

   using Microsoft.Basetypes;

 

-  using ISet = Microsoft.Boogie.Set;

-  using HashSet = Microsoft.Boogie.Set;

-

+  using ISet = Microsoft.Boogie.GSet<object>;

+  using HashSet = Microsoft.Boogie.GSet<object>;

 

   /// <summary>

   /// Represents an invariant over linear variable constraints, represented by a polyhedron.

diff --git a/Source/AIFramework/Polyhedra/SimplexTableau.cs b/Source/AIFramework/Polyhedra/SimplexTableau.cs
index 4c37e980..4d734c27 100644
--- a/Source/AIFramework/Polyhedra/SimplexTableau.cs
+++ b/Source/AIFramework/Polyhedra/SimplexTableau.cs
@@ -8,8 +8,8 @@ namespace Microsoft.AbstractInterpretationFramework {
   using System;

   using System.Diagnostics.Contracts;

   using Microsoft.Basetypes;

-  using IMutableSet = Microsoft.Boogie.Set;

-  using HashSet = Microsoft.Boogie.Set;

+  using IMutableSet = Microsoft.Boogie.GSet<object>;

+  using HashSet = Microsoft.Boogie.GSet<object>;

 

 

   /// <summary>

diff --git a/Source/AIFramework/VariableMap/VariableMapLattice.cs b/Source/AIFramework/VariableMap/VariableMapLattice.cs
index b60d318b..172cef01 100644
--- a/Source/AIFramework/VariableMap/VariableMapLattice.cs
+++ b/Source/AIFramework/VariableMap/VariableMapLattice.cs
@@ -13,9 +13,11 @@ namespace Microsoft.AbstractInterpretationFramework {
   using Microsoft.AbstractInterpretationFramework.Collections;

 

   using Microsoft.Boogie;

-  using IMutableSet = Microsoft.Boogie.Set;

-  using HashSet = Microsoft.Boogie.Set;

-  using ISet = Microsoft.Boogie.Set;

+

+  using IMutableSet = Microsoft.Boogie.GSet<object>;

+  using ISet = Microsoft.Boogie.GSet<object>;

+  using Set = Microsoft.Boogie.GSet<object>;

+  using HashSet = Microsoft.Boogie.GSet<object>;

 

   /// <summary>

   ///  Creates a lattice that works for several variables given a MicroLattice.  Assumes