Protect the Expr field of OldExpr if it is immutable. Add unit test

to check this is being enforced.

2 files changed, 20 insertions, 3 deletions

diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index f3945e5d..e6c21e1f 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -947,8 +947,18 @@ namespace Microsoft.Boogie {
 

   public class OldExpr : Expr

   {

-    // FIXME: protect this field

-    public Expr/*!*/ Expr;

+    private Expr _Expr;

+    public Expr/*!*/ Expr {

+      get {

+        return _Expr;

+      }

+      set {

+        if (Immutable)

+          throw new InvalidOperationException("Cannot change Expr of an Immutable OldExpr");

+

+        _Expr = value;

+      }

+    }

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(Expr != null);

@@ -958,7 +968,7 @@ namespace Microsoft.Boogie {
       : base(tok, immutable) {

       Contract.Requires(tok != null);

       Contract.Requires(expr != null);

-      Expr = expr;

+      _Expr = expr;

       if (immutable)

         CachedHashCode = ComputeHashCode();

     }

diff --git a/Source/UnitTests/CoreTests/ExprImmutability.cs b/Source/UnitTests/CoreTests/ExprImmutability.cs
index 68b71083..e13feca7 100644
--- a/Source/UnitTests/CoreTests/ExprImmutability.cs
+++ b/Source/UnitTests/CoreTests/ExprImmutability.cs
@@ -89,6 +89,13 @@ namespace CoreTests
             // Trying to assign the same Type should succeed
             e.Type = BasicType.Bool;
         }
+
+        [Test(), ExpectedException(typeof(InvalidOperationException))]
+        public void ProtectedOldExpr()
+        {
+            var e = new OldExpr(Token.NoToken, Expr.True, /*immutable=*/ true);
+            e.Expr = Expr.False;
+        }
     }
 }