Requires/EnsuresSeq replaced by List<Requires/Ensures>

7 files changed, 30 insertions, 42 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 5f6ecc26..0e9909cb 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -2359,9 +2359,9 @@ namespace Microsoft.Boogie {
   }

 

   public class Procedure : DeclWithFormals {

-    public RequiresSeq/*!*/ Requires;

+    public List<Requires>/*!*/ Requires;

     public IdentifierExprSeq/*!*/ Modifies;

-    public EnsuresSeq/*!*/ Ensures;

+    public List<Ensures>/*!*/ Ensures;

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(Requires != null);

@@ -2376,7 +2376,7 @@ namespace Microsoft.Boogie {
     public readonly ProcedureSummary/*!*/ Summary;

 

     public Procedure(IToken/*!*/ tok, string/*!*/ name, TypeVariableSeq/*!*/ typeParams, VariableSeq/*!*/ inParams, VariableSeq/*!*/ outParams,

-      RequiresSeq/*!*/ requires, IdentifierExprSeq/*!*/ modifies, EnsuresSeq/*!*/ ensures)

+      List<Requires>/*!*/ requires, IdentifierExprSeq/*!*/ modifies, List<Ensures>/*!*/ ensures)

       : this(tok, name, typeParams, inParams, outParams, requires, modifies, ensures, null) {

       Contract.Requires(tok != null);

       Contract.Requires(name != null);

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

 

     public Procedure(IToken/*!*/ tok, string/*!*/ name, TypeVariableSeq/*!*/ typeParams, VariableSeq/*!*/ inParams, VariableSeq/*!*/ outParams,

-      RequiresSeq/*!*/ @requires, IdentifierExprSeq/*!*/ @modifies, EnsuresSeq/*!*/ @ensures, QKeyValue kv

+      List<Requires>/*!*/ @requires, IdentifierExprSeq/*!*/ @modifies, List<Ensures>/*!*/ @ensures, QKeyValue kv

       )

       : base(tok, name, typeParams, inParams, outParams) {

       Contract.Requires(tok != null);

@@ -2531,7 +2531,7 @@ namespace Microsoft.Boogie {
                            VariableSeq inputs, VariableSeq outputs, IdentifierExprSeq globalMods)

           : base(Token.NoToken, impl.Name + "_loop_" + header.ToString(),

                new TypeVariableSeq(), inputs, outputs,

-               new RequiresSeq(), globalMods, new EnsuresSeq())

+               new List<Requires>(), globalMods, new List<Ensures>())

       {

           enclosingImpl = impl;

       }

@@ -3224,18 +3224,6 @@ namespace Microsoft.Boogie {
     }

   }

 

-  public sealed class RequiresSeq : List<Requires> {

-    public int Length {

-      get { return Count; }

-    }

-  }

-

-  public sealed class EnsuresSeq : List<Ensures> {

-    public int Length {

-      get { return Count; }

-    }

-  }

-

   public sealed class VariableSeq : List<Variable> {

     public VariableSeq(params Variable[]/*!*/ args)

       : base(args) {

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index cf6fa9ce..47f5505e 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -2113,7 +2113,7 @@ namespace Microsoft.Boogie {
       Substitution s = Substituter.SubstitutionFromHashtable(substMapBound);

       bool hasWildcard = (wildcardVars.Length != 0);

       Expr preConjunction = null;

-      for (int i = 0; i < this.Proc.Requires.Length; i++) {

+      for (int i = 0; i < this.Proc.Requires.Count; i++) {

         Requires/*!*/ req = cce.NonNull(this.Proc.Requires[i]);

         if (!req.Free && !IsFree) {

           if (hasWildcard) {

@@ -2149,7 +2149,7 @@ namespace Microsoft.Boogie {
       #region assume Pre[ins := cins] with formal paramters

       if (hasWildcard) {

         s = Substituter.SubstitutionFromHashtable(substMap);

-        for (int i = 0; i < this.Proc.Requires.Length; i++) {

+        for (int i = 0; i < this.Proc.Requires.Count; i++) {

           Requires/*!*/ req = cce.NonNull(this.Proc.Requires[i]);

           if (!req.Free) {

             Requires/*!*/ reqCopy = (Requires/*!*/)cce.NonNull(req.Clone());

diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg
index 64ddbb50..9cd7d524 100644
--- a/Source/Core/BoogiePL.atg
+++ b/Source/Core/BoogiePL.atg
@@ -588,9 +588,9 @@ Procedure<out Procedure/*!*/ proc, out /*maybe null*/ Implementation impl>
 = (. Contract.Ensures(Contract.ValueAtReturn(out proc) != null); IToken/*!*/ x;

      TypeVariableSeq/*!*/ typeParams;

      VariableSeq/*!*/ ins, outs;

-     RequiresSeq/*!*/ pre = new RequiresSeq();

+     List<Requires>/*!*/ pre = new List<Requires>();

      IdentifierExprSeq/*!*/ mods = new IdentifierExprSeq();

-     EnsuresSeq/*!*/ post = new EnsuresSeq();

+     List<Ensures>/*!*/ post = new List<Ensures>();

 

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

      StmtList/*!*/ stmtList;

@@ -642,7 +642,7 @@ ProcSignature<bool allowWhereClausesOnFormals, out IToken/*!*/ name, out TypeVar
   .

 

 

-Spec<RequiresSeq/*!*/ pre, IdentifierExprSeq/*!*/ mods, EnsuresSeq/*!*/ post>

+Spec<List<Requires>/*!*/ pre, IdentifierExprSeq/*!*/ mods, List<Ensures>/*!*/ post>

 = (.Contract.Requires(pre != null); Contract.Requires(mods != null); Contract.Requires(post != null); TokenSeq/*!*/ ms; .)

   ( "modifies"

     [ Idents<out ms>        (. foreach(IToken/*!*/ m in ms){

@@ -656,7 +656,7 @@ Spec<RequiresSeq/*!*/ pre, IdentifierExprSeq/*!*/ mods, EnsuresSeq/*!*/ post>
   )

   .

 

-SpecPrePost<bool free, RequiresSeq/*!*/ pre, EnsuresSeq/*!*/ post>

+SpecPrePost<bool free, List<Requires>/*!*/ pre, List<Ensures>/*!*/ post>

 = (. Contract.Requires(pre != null); Contract.Requires(post != null); Expr/*!*/ e; Token tok = null; QKeyValue kv = null; .)

   ( "requires"              (. tok = t; .)

     { Attribute<ref kv> }

diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs
index b7626d99..26d57f68 100644
--- a/Source/Core/Inline.cs
+++ b/Source/Core/Inline.cs
@@ -453,7 +453,7 @@ namespace Microsoft.Boogie {
       }

 

       // inject requires

-      for (int i = 0; i < proc.Requires.Length; i++) {

+      for (int i = 0; i < proc.Requires.Count; i++) {

         Requires/*!*/ req = cce.NonNull(proc.Requires[i]);

         inCmds.Add(InlinedRequires(callCmd, req));

       }

@@ -529,7 +529,7 @@ namespace Microsoft.Boogie {
       CmdSeq outCmds = new CmdSeq();

 

       // inject ensures

-      for (int i = 0; i < proc.Ensures.Length; i++) {

+      for (int i = 0; i < proc.Ensures.Count; i++) {

         Ensures/*!*/ ens = cce.NonNull(proc.Ensures[i]);

         outCmds.Add(InlinedEnsures(callCmd, ens));

       }

diff --git a/Source/Core/OwickiGries.cs b/Source/Core/OwickiGries.cs
index 63f9557f..bd6b1da3 100644
--- a/Source/Core/OwickiGries.cs
+++ b/Source/Core/OwickiGries.cs
@@ -176,7 +176,7 @@ namespace Microsoft.Boogie
                 Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_global_old_{0}", ie.Decl.Name), ie.Decl.TypedIdent.Type), true);

                 inputs.Add(f);

             }

-            yieldProc = new Procedure(Token.NoToken, "og_yield", new TypeVariableSeq(), inputs, new VariableSeq(), new RequiresSeq(), new IdentifierExprSeq(), new EnsuresSeq());

+            yieldProc = new Procedure(Token.NoToken, "og_yield", new TypeVariableSeq(), inputs, new VariableSeq(), new List<Requires>(), new IdentifierExprSeq(), new List<Ensures>());

             yieldProc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));

         }

 

@@ -275,8 +275,8 @@ namespace Microsoft.Boogie
 

             VariableSeq inParams = new VariableSeq();

             VariableSeq outParams = new VariableSeq();

-            RequiresSeq requiresSeq = new RequiresSeq();

-            EnsuresSeq ensuresSeq = new EnsuresSeq();

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

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

             IdentifierExprSeq ieSeq = new IdentifierExprSeq();

             int count = 0;

             while (callCmd != null)

@@ -406,7 +406,7 @@ namespace Microsoft.Boogie
 

             // Create the yield checker procedure

             var yieldCheckerName = string.Format("{0}_YieldChecker_{1}", decl is Procedure ? "Proc" : "Impl", decl.Name);

-            var yieldCheckerProc = new Procedure(Token.NoToken, yieldCheckerName, decl.TypeParameters, inputs, new VariableSeq(), new RequiresSeq(), new IdentifierExprSeq(), new EnsuresSeq());

+            var yieldCheckerProc = new Procedure(Token.NoToken, yieldCheckerName, decl.TypeParameters, inputs, new VariableSeq(), new List<Requires>(), new IdentifierExprSeq(), new List<Ensures>());

             yieldCheckerProc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));

             yieldCheckerProcs.Add(yieldCheckerProc);

 

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

                             if (!asyncAndParallelCallDesugarings.ContainsKey(callCmd.Proc.Name))

                             {

-                                asyncAndParallelCallDesugarings[callCmd.Proc.Name] = new Procedure(Token.NoToken, string.Format("DummyAsyncTarget_{0}", callCmd.Proc.Name), callCmd.Proc.TypeParameters, callCmd.Proc.InParams, callCmd.Proc.OutParams, callCmd.Proc.Requires, new IdentifierExprSeq(), new EnsuresSeq());

+                                asyncAndParallelCallDesugarings[callCmd.Proc.Name] = new Procedure(Token.NoToken, string.Format("DummyAsyncTarget_{0}", callCmd.Proc.Name), callCmd.Proc.TypeParameters, callCmd.Proc.InParams, callCmd.Proc.OutParams, callCmd.Proc.Requires, new IdentifierExprSeq(), new List<Ensures>());

                             }

                             var dummyAsyncTargetProc = asyncAndParallelCallDesugarings[callCmd.Proc.Name];

                             CallCmd dummyCallCmd = new CallCmd(Token.NoToken, dummyAsyncTargetProc.Name, callCmd.Ins, callCmd.Outs);

@@ -639,7 +639,7 @@ namespace Microsoft.Boogie
             // Collect the yield predicates and desugar yields

             List<CmdSeq> yields = new List<CmdSeq>();

             CmdSeq cmds = new CmdSeq();

-            if (proc.Requires.Length > 0)

+            if (proc.Requires.Count > 0)

             {

                 Dictionary<string, HashSet<Variable>> domainNameToScope = new Dictionary<string, HashSet<Variable>>();

                 foreach (var domainName in linearTypechecker.linearDomains.Keys)

@@ -678,7 +678,7 @@ namespace Microsoft.Boogie
                 yields.Add(cmds);

                 cmds = new CmdSeq();

             }

-            if (info.inParallelCall && proc.Ensures.Length > 0)

+            if (info.inParallelCall && proc.Ensures.Count > 0)

             {

                 Dictionary<string, HashSet<Variable>> domainNameToScope = new Dictionary<string, HashSet<Variable>>();

                 foreach (var domainName in linearTypechecker.linearDomains.Keys)

diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index 95c46934..32e439f0 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -470,9 +470,9 @@ private class BvBounds : Expr {
 		Contract.Ensures(Contract.ValueAtReturn(out proc) != null); IToken/*!*/ x;

 		TypeVariableSeq/*!*/ typeParams;

 		VariableSeq/*!*/ ins, outs;

-		RequiresSeq/*!*/ pre = new RequiresSeq();

+		List<Requires>/*!*/ pre = new List<Requires>();

 		IdentifierExprSeq/*!*/ mods = new IdentifierExprSeq();

-		EnsuresSeq/*!*/ post = new EnsuresSeq();

+		List<Ensures>/*!*/ post = new List<Ensures>();

 		

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

 		StmtList/*!*/ stmtList;

@@ -867,7 +867,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
 		}

 	}

 

-	void Spec(RequiresSeq/*!*/ pre, IdentifierExprSeq/*!*/ mods, EnsuresSeq/*!*/ post) {

+	void Spec(List<Requires>/*!*/ pre, IdentifierExprSeq/*!*/ mods, List<Ensures>/*!*/ post) {

 		Contract.Requires(pre != null); Contract.Requires(mods != null); Contract.Requires(post != null); TokenSeq/*!*/ ms; 

 		if (la.kind == 34) {

 			Get();

@@ -897,7 +897,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
 		StmtList(out stmtList);

 	}

 

-	void SpecPrePost(bool free, RequiresSeq/*!*/ pre, EnsuresSeq/*!*/ post) {

+	void SpecPrePost(bool free, List<Requires>/*!*/ pre, List<Ensures>/*!*/ post) {

 		Contract.Requires(pre != null); Contract.Requires(post != null); Expr/*!*/ e; Token tok = null; QKeyValue kv = null; 

 		if (la.kind == 36) {

 			Get();

diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs
index ee873bd4..800a5494 100644
--- a/Source/Core/StandardVisitor.cs
+++ b/Source/Core/StandardVisitor.cs
@@ -248,10 +248,10 @@ namespace Microsoft.Boogie {
       @requires.Condition = this.VisitExpr(@requires.Condition);

       return @requires;

     }

-    public virtual RequiresSeq VisitRequiresSeq(RequiresSeq requiresSeq) {

+    public virtual List<Requires> VisitRequiresSeq(List<Requires> requiresSeq) {

       Contract.Requires(requiresSeq != null);

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

-      for (int i = 0, n = requiresSeq.Length; i < n; i++)

+      Contract.Ensures(Contract.Result<List<Requires>>() != null);

+      for (int i = 0, n = requiresSeq.Count; i < n; i++)

         requiresSeq[i] = this.VisitRequires(requiresSeq[i]);

       return requiresSeq;

     }

@@ -261,10 +261,10 @@ namespace Microsoft.Boogie {
       @ensures.Condition = this.VisitExpr(@ensures.Condition);

       return @ensures;

     }

-    public virtual EnsuresSeq VisitEnsuresSeq(EnsuresSeq ensuresSeq) {

+    public virtual List<Ensures> VisitEnsuresSeq(List<Ensures> ensuresSeq) {

       Contract.Requires(ensuresSeq != null);

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

-      for (int i = 0, n = ensuresSeq.Length; i < n; i++)

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

+      for (int i = 0, n = ensuresSeq.Count; i < n; i++)

         ensuresSeq[i] = this.VisitEnsures(ensuresSeq[i]);

       return ensuresSeq;

     }