Requires/EnsuresSeq replaced by List<Requires/Ensures>

3 files changed, 6 insertions, 6 deletions

diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs
index 157571f3..2ff5975e 100644
--- a/Source/Houdini/AbstractHoudini.cs
+++ b/Source/Houdini/AbstractHoudini.cs
@@ -2238,7 +2238,7 @@ namespace Microsoft.Boogie.Houdini {
 

             foreach (var proc in program.TopLevelDeclarations.OfType<Procedure>())

             {

-                var nensures = new EnsuresSeq();

+                var nensures = new List<Ensures>();

                 proc.Ensures.OfType<Ensures>()

                 .Where(ens => !QKeyValue.FindBoolAttribute(ens.Attributes, "ah") &&

                     !QKeyValue.FindBoolAttribute(ens.Attributes, "pre") &&

@@ -3147,7 +3147,7 @@ namespace Microsoft.Boogie.Houdini {
                 PosPrePreds[impl.Name].UnionWith(posPreT);

 

                 // Pick up per-procedure pre-post

-                var nens = new EnsuresSeq();

+                var nens = new List<Ensures>();

                 foreach (var ens in impl.Proc.Ensures.OfType<Ensures>())

                 {

                     string s = null;

diff --git a/Source/Houdini/CandidateDependenceAnalyser.cs b/Source/Houdini/CandidateDependenceAnalyser.cs
index 9a2eb404..0f725ccf 100644
--- a/Source/Houdini/CandidateDependenceAnalyser.cs
+++ b/Source/Houdini/CandidateDependenceAnalyser.cs
@@ -437,7 +437,7 @@ namespace Microsoft.Boogie.Houdini {
         {

 

           #region Handle the preconditions

-          RequiresSeq newRequires = new RequiresSeq();

+          List<Requires> newRequires = new List<Requires>();

           foreach(Requires r in p.Requires) {

             string c;

             if (Houdini.MatchCandidate(r.Condition, candidates, out c)) {

@@ -457,7 +457,7 @@ namespace Microsoft.Boogie.Houdini {
           #endregion

 

           #region Handle the postconditions

-          EnsuresSeq newEnsures = new EnsuresSeq();

+          List<Ensures> newEnsures = new List<Ensures>();

           foreach(Ensures e in p.Ensures) {

             string c;

             if (Houdini.MatchCandidate(e.Condition, candidates, out c)) {

diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index 06d606ff..5078d5a5 100644
--- a/Source/Houdini/Houdini.cs
+++ b/Source/Houdini/Houdini.cs
@@ -1165,7 +1165,7 @@ namespace Microsoft.Boogie.Houdini {
       }

 

       foreach (var proc in prog.TopLevelDeclarations.OfType<Procedure>()) {

-        RequiresSeq newRequires = new RequiresSeq();

+        List<Requires> newRequires = new List<Requires>();

         foreach (Requires r in proc.Requires) {

           string c;

           if (MatchCandidate(r.Condition, out c)) {

@@ -1185,7 +1185,7 @@ namespace Microsoft.Boogie.Houdini {
         }

         proc.Requires = newRequires;

 

-        EnsuresSeq newEnsures = new EnsuresSeq();

+        List<Ensures> newEnsures = new List<Ensures>();

         foreach (Ensures e in proc.Ensures) {

           string c;

           if (MatchCandidate(e.Condition, out c)) {