diff options
Diffstat (limited to 'Source/UnitTests/CoreTests/ExprImmutability.cs')
-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 + } } } |