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

to check this is being enforced.

1 files changed, 13 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();

     }