summaryrefslogtreecommitdiff
path: root/Source/Core
diff options
context:
space:
mode:
authorGravatar Dan Liew <daniel.liew@imperial.ac.uk>2015-01-29 03:21:50 +0000
committerGravatar Dan Liew <daniel.liew@imperial.ac.uk>2015-01-29 03:21:50 +0000
commit9ecdcd65b9173736a191662072865ec0bb075c04 (patch)
tree9466bdf4628aba85ab52003c7479c7996550f502 /Source/Core
parent506c17c312bf12188a9b1eabcdf80a71f92d9bb9 (diff)
Protect the Expr field of OldExpr if it is immutable. Add unit test
to check this is being enforced.
Diffstat (limited to 'Source/Core')
-rw-r--r--Source/Core/AbsyExpr.cs16
1 files changed, 13 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();
}