From cef89809053b0679019491a227ed03c98be44854 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Thu, 29 Jan 2015 03:47:05 +0000
Subject: Protect the NAryExpr.Fun field when the NAryExpr is immutable. Add a
 unit test for this. We need to protect the Args field too but that is going
 to be much harder to enforce.

---
 Source/Core/AbsyExpr.cs                        | 17 ++++++++++++++---
 Source/UnitTests/CoreTests/ExprImmutability.cs |  7 +++++++
 2 files changed, 21 insertions(+), 3 deletions(-)

diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index e6c21e1f..75a5741a 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -2230,8 +2230,19 @@ namespace Microsoft.Boogie {
   public class NAryExpr : Expr {
     [Additive]
     [Peer]
-    // FIXME: Protect these fields
-    public IAppliable/*!*/ Fun;
+    private IAppliable _Fun;
+    public IAppliable/*!*/ Fun {
+      get {
+        return _Fun;
+      }
+      set {
+        if (Immutable)
+          throw new InvalidOperationException("Cannot change Function used by Immutable NAryExpr");
+
+        _Fun = value;
+      }
+    }
+    // FIXME: Protect this field when immutable
     public List<Expr> Args;
 
     [ContractInvariantMethod]
@@ -2251,7 +2262,7 @@ namespace Microsoft.Boogie {
       Contract.Requires(tok != null);
       Contract.Requires(fun != null);
       Contract.Requires(args != null);
-      Fun = fun;
+      _Fun = fun;
       Args = args;
       Contract.Assert(Contract.ForAll(0, args.Count, index => args[index] != null));
       if (immutable)
diff --git a/Source/UnitTests/CoreTests/ExprImmutability.cs b/Source/UnitTests/CoreTests/ExprImmutability.cs
index e13feca7..aff0acea 100644
--- a/Source/UnitTests/CoreTests/ExprImmutability.cs
+++ b/Source/UnitTests/CoreTests/ExprImmutability.cs
@@ -96,6 +96,13 @@ namespace CoreTests
             var e = new OldExpr(Token.NoToken, Expr.True, /*immutable=*/ true);
             e.Expr = Expr.False;
         }
+
+        [Test(), ExpectedException(typeof(InvalidOperationException))]
+        public void ProtectedNAryFunc()
+        {
+            var e = GetUnTypedImmutableNAry();
+            e.Fun = new BinaryOperator(Token.NoToken, BinaryOperator.Opcode.Sub);
+        }
     }
 }
 
-- 
cgit v1.2.3