From 6f04bf428ce8a3422877c590b931b55efd0245b8 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Thu, 29 Jan 2015 02:43:42 +0000
Subject: Protect the Type field of an Expr if is Immutable. Note if the Expr
 has never been type checked we allow the Type field to be set but once it has
 been set it cannot be changed to refer to a different Type.

---
 Source/Core/AbsyExpr.cs | 18 +++++++++++++++++-
 1 file changed, 17 insertions(+), 1 deletion(-)

diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index c0f814e8..f3945e5d 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -91,7 +91,23 @@ namespace Microsoft.Boogie {
     /// been called or Typecheck encountered an error in the expression to be
     /// typechecked).
     /// </summary>
-    public Type Type;
+    private Type _Type = null;
+    public Type Type {
+      get {
+        return _Type;
+      }
+      set {
+        if (_Type == null) {
+          // Expr has never been type checked so always allow this
+          _Type = value;
+        } else  {
+          if (Immutable && !_Type.Equals(value))
+            throw new InvalidOperationException("Cannot change the Type of an Immutable Expr");
+
+          _Type = value;
+        }
+      }
+    }
 
     public override void Typecheck(TypecheckingContext tc) {
       //Contract.Requires(tc != null);
-- 
cgit v1.2.3