Made some compatibility fixes after running the unit tests.

Added an internal non-readonly version of Lhss and Rhss to 'AssignCmd'.

2 files changed, 26 insertions, 6 deletions

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index be712ffb..ed079a58 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -1281,6 +1281,16 @@ namespace Microsoft.Boogie {
         Contract.Requires(cce.NonNullElements(value));

         this._lhss = new List<AssignLhs>(value);

       }

+    }

+

+    internal IList<AssignLhs/*!*/>/*!*/ Lhss_NRO

+    {

+      get

+      {

+        Contract.Ensures(cce.NonNullElements(Contract.Result<IList<AssignLhs>>()));

+        Contract.Ensures(!Contract.Result<IList<AssignLhs>>().IsReadOnly);

+        return this._lhss;

+      }

     }
 
     private List<Expr/*!*/>/*!*/ _rhss;

@@ -1297,6 +1307,16 @@ namespace Microsoft.Boogie {
       }

     }

 

+    internal IList<Expr/*!*/>/*!*/ Rhss_NRO

+    {

+      get

+      {

+        Contract.Ensures(cce.NonNullElements(Contract.Result<IList<Expr>>()));

+        Contract.Ensures(!Contract.Result<IList<Expr>>().IsReadOnly);

+        return this._rhss;

+      }

+    }

+

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(cce.NonNullElements(this._lhss));

@@ -1304,13 +1324,13 @@ namespace Microsoft.Boogie {
     }

 

 

-    public AssignCmd(IToken tok, List<AssignLhs/*!*/>/*!*/ lhss, List<Expr/*!*/>/*!*/ rhss)

+    public AssignCmd(IToken tok, IList<AssignLhs/*!*/>/*!*/ lhss, IList<Expr/*!*/>/*!*/ rhss)

       : base(tok) {

       Contract.Requires(tok != null);

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

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

-      this._lhss = lhss;

-      this._rhss = rhss;

+      this._lhss = new List<AssignLhs>(lhss);

+      this._rhss = new List<Expr>(rhss);

     }

 

     public override void Emit(TokenTextWriter stream, int level) {

@@ -1748,7 +1768,7 @@ namespace Microsoft.Boogie {
         Contract.Ensures(Contract.Result<List<Variable>>() != null);

         return this._cmds;

       }

-      internal set {

+      set {

         Contract.Requires(value != null);

         this._cmds = value;

       }

diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs
index 3f3ad5ae..0284549b 100644
--- a/Source/Core/StandardVisitor.cs
+++ b/Source/Core/StandardVisitor.cs
@@ -75,8 +75,8 @@ namespace Microsoft.Boogie {
       Contract.Requires(node != null);

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

       for (int i = 0; i < node.Lhss.Count; ++i) {

-        node.Lhss[i] = cce.NonNull((AssignLhs)this.Visit(node.Lhss[i]));

-        node.Rhss[i] = cce.NonNull((Expr/*!*/)this.Visit(node.Rhss[i]));

+        node.Lhss_NRO[i] = cce.NonNull((AssignLhs)this.Visit(node.Lhss[i]));

+        node.Rhss_NRO[i] = cce.NonNull((Expr/*!*/)this.Visit(node.Rhss[i]));

       }

       return node;

     }