From 9ecdcd65b9173736a191662072865ec0bb075c04 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Thu, 29 Jan 2015 03:21:50 +0000
Subject: Protect the Expr field of OldExpr if it is immutable. Add unit test
 to check this is being enforced.

---
 Source/Core/AbsyExpr.cs | 16 +++++++++++++---
 1 file changed, 13 insertions(+), 3 deletions(-)

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

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