From 2b47e4493d08c11163fdce388d9313e035e4a12a Mon Sep 17 00:00:00 2001
From: 0biha <unknown>
Date: Wed, 24 Dec 2014 20:54:51 +0100
Subject: Made some compatibility fixes after running the unit tests. Added an
 internal non-readonly version of Lhss and Rhss to 'AssignCmd'.

---
 Source/Core/AbsyCmd.cs | 28 ++++++++++++++++++++++++----
 1 file changed, 24 insertions(+), 4 deletions(-)

(limited to 'Source/Core/AbsyCmd.cs')

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;
       }
-- 
cgit v1.2.3