From b1bd1bca3bab1912924e7401cee111bce8c28422 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Thu, 12 Feb 2015 11:42:31 +0000 Subject: Protect E0 and E1 in BvConcatExpr if Expr is immutable. --- Source/UnitTests/CoreTests/ExprImmutability.cs | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) (limited to 'Source/UnitTests/CoreTests/ExprImmutability.cs') 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 + } } } -- cgit v1.2.3