summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
authorGravatar Dan Liew <daniel.liew@imperial.ac.uk>2015-02-12 11:42:31 +0000
committerGravatar Dan Liew <daniel.liew@imperial.ac.uk>2015-02-12 11:42:31 +0000
commitb1bd1bca3bab1912924e7401cee111bce8c28422 (patch)
treecc3b45145bf6f3594e1cbe3810d906e2b3bee9d0 /Source
parent4410dba67b19995e40ab51c06922937b2cc55bc3 (diff)
Protect E0 and E1 in BvConcatExpr if Expr is immutable.
Diffstat (limited to 'Source')
-rw-r--r--Source/Core/AbsyExpr.cs29
-rw-r--r--Source/UnitTests/CoreTests/ExprImmutability.cs20
2 files changed, 45 insertions, 4 deletions
diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index 75f2c519..2427d856 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -3080,8 +3080,29 @@ namespace Microsoft.Boogie {
}
public class BvConcatExpr : Expr {
- // FIXME: Protect these fields
- public /*readonly--except in StandardVisitor*/ Expr/*!*/ E0, E1;
+ private /*readonly--except in StandardVisitor*/ Expr/*!*/ _E0, _E1;
+ public Expr E0 {
+ get {
+ return _E0;
+ }
+ set {
+ if (Immutable)
+ throw new InvalidOperationException("Can't change E0 reference on immutable Expr");
+
+ _E0 = value;
+ }
+ }
+ public Expr E1 {
+ get {
+ return _E1;
+ }
+ set {
+ if (Immutable)
+ throw new InvalidOperationException("Can't change E1 reference on immutable Expr");
+
+ _E1 = value;
+ }
+ }
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(E0 != null);
@@ -3094,8 +3115,8 @@ namespace Microsoft.Boogie {
Contract.Requires(tok != null);
Contract.Requires(e0 != null);
Contract.Requires(e1 != null);
- E0 = e0;
- E1 = e1;
+ _E0 = e0;
+ _E1 = e1;
if (immutable)
CachedHashCode = ComputeHashCode();
}
diff --git a/Source/UnitTests/CoreTests/ExprImmutability.cs b/Source/UnitTests/CoreTests/ExprImmutability.cs
index a26f8b8b..98e7158f 100644
--- a/Source/UnitTests/CoreTests/ExprImmutability.cs
+++ b/Source/UnitTests/CoreTests/ExprImmutability.cs
@@ -249,6 +249,26 @@ namespace CoreTests
null, body, /*immutable=*/true);
lambda.Body = Expr.Lt(xId, yId); // Changing the body of an immutable ExistsExpr should fail
}
+
+ [Test(), ExpectedException(typeof(InvalidOperationException))]
+ public void ProtectedBvConcatExprLhs()
+ {
+ var lhs = new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(0), 32, /*immutable=*/true);
+ var rhs = new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1), 32, /*immutable=*/true);
+ var concat = new BvConcatExpr(Token.NoToken, lhs, rhs,/* immutable=*/true);
+ Assert.IsTrue(concat.Immutable);
+ concat.E0 = rhs; // Should throw
+ }
+
+ [Test(), ExpectedException(typeof(InvalidOperationException))]
+ public void ProtectedBvConcatExprRhs()
+ {
+ var lhs = new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(0), 32, /*immutable=*/true);
+ var rhs = new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1), 32, /*immutable=*/true);
+ var concat = new BvConcatExpr(Token.NoToken, lhs, rhs,/* immutable=*/true);
+ Assert.IsTrue(concat.Immutable);
+ concat.E1 = lhs; // Should throw
+ }
}
}