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.

1 files changed, 14 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)