diff options
| -rw-r--r-- | Source/Core/AbsyExpr.cs | 16 | ||||
| -rw-r--r-- | Source/UnitTests/CoreTests/ExprImmutability.cs | 7 |
2 files changed, 20 insertions, 3 deletions
diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs index f3945e5d..e6c21e1f 100644 --- a/Source/Core/AbsyExpr.cs +++ b/Source/Core/AbsyExpr.cs @@ -947,8 +947,18 @@ namespace Microsoft.Boogie { public class OldExpr : Expr
{
- // FIXME: protect this field
- public Expr/*!*/ Expr;
+ private Expr _Expr;
+ public Expr/*!*/ Expr {
+ get {
+ return _Expr;
+ }
+ set {
+ if (Immutable)
+ throw new InvalidOperationException("Cannot change Expr of an Immutable OldExpr");
+
+ _Expr = value;
+ }
+ }
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(Expr != null);
@@ -958,7 +968,7 @@ namespace Microsoft.Boogie { : base(tok, immutable) {
Contract.Requires(tok != null);
Contract.Requires(expr != null);
- Expr = expr;
+ _Expr = expr;
if (immutable)
CachedHashCode = ComputeHashCode();
}
diff --git a/Source/UnitTests/CoreTests/ExprImmutability.cs b/Source/UnitTests/CoreTests/ExprImmutability.cs index 68b71083..e13feca7 100644 --- a/Source/UnitTests/CoreTests/ExprImmutability.cs +++ b/Source/UnitTests/CoreTests/ExprImmutability.cs @@ -89,6 +89,13 @@ namespace CoreTests // Trying to assign the same Type should succeed e.Type = BasicType.Bool; } + + [Test(), ExpectedException(typeof(InvalidOperationException))] + public void ProtectedOldExpr() + { + var e = new OldExpr(Token.NoToken, Expr.True, /*immutable=*/ true); + e.Expr = Expr.False; + } } } |