summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Dan Liew <daniel.liew@imperial.ac.uk>2015-01-29 02:43:42 +0000
committerGravatar Dan Liew <daniel.liew@imperial.ac.uk>2015-01-29 02:43:42 +0000
commit6f04bf428ce8a3422877c590b931b55efd0245b8 (patch)
tree13bffe35bf291a7683f1eea54455bf863b292a21
parentd6e6e3471cffcfe6099e8e0633780f4af952eeb4 (diff)
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.
-rw-r--r--Source/Core/AbsyExpr.cs18
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);