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.

1 files changed, 17 insertions, 1 deletions

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);