diff options
author | Dan Liew <daniel.liew@imperial.ac.uk> | 2015-02-12 11:42:31 +0000 |
---|---|---|
committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2015-02-12 11:42:31 +0000 |
commit | b1bd1bca3bab1912924e7401cee111bce8c28422 (patch) | |
tree | cc3b45145bf6f3594e1cbe3810d906e2b3bee9d0 /Source/UnitTests | |
parent | 4410dba67b19995e40ab51c06922937b2cc55bc3 (diff) |
Protect E0 and E1 in BvConcatExpr if Expr is immutable.
Diffstat (limited to 'Source/UnitTests')
-rw-r--r-- | Source/UnitTests/CoreTests/ExprImmutability.cs | 20 |
1 files changed, 20 insertions, 0 deletions
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 + } } } |