From 3eb1b720b8222b6415bed0faed12bd7b04ca5425 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Thu, 29 Jan 2015 09:08:14 +0000 Subject: Protect the body of ForAllExpr, ExistsExpr and LambdaExpr when they are immutable. Add unit tests to check this. --- Source/UnitTests/CoreTests/ExprImmutability.cs | 37 ++++++++++++++++++++++++++ 1 file changed, 37 insertions(+) (limited to 'Source/UnitTests/CoreTests/ExprImmutability.cs') diff --git a/Source/UnitTests/CoreTests/ExprImmutability.cs b/Source/UnitTests/CoreTests/ExprImmutability.cs index f3225b0f..9a9536c1 100644 --- a/Source/UnitTests/CoreTests/ExprImmutability.cs +++ b/Source/UnitTests/CoreTests/ExprImmutability.cs @@ -140,6 +140,43 @@ namespace CoreTests var e = GetUnTypedImmutableNAry(); e.Fun = new BinaryOperator(Token.NoToken, BinaryOperator.Opcode.Sub); } + + [Test(), ExpectedException(typeof(InvalidOperationException))] + public void ProtectedForAllExprBody() + { + var x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", BasicType.Int)); + var y = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", BasicType.Int)); + var xId = new IdentifierExpr(Token.NoToken, x, /*immutable=*/true); + var yId = new IdentifierExpr(Token.NoToken, y, /*immutable=*/true); + var body = Expr.Gt(xId, yId); + var forAll = new ForallExpr(Token.NoToken, new List () { x, y }, body, /*immutable=*/true); + forAll.Body = Expr.Lt(xId, yId); // Changing the body of an immutable ForAllExpr should fail + } + + [Test(), ExpectedException(typeof(InvalidOperationException))] + public void ProtectedExistsExprBody() + { + var x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", BasicType.Int)); + var y = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", BasicType.Int)); + var xId = new IdentifierExpr(Token.NoToken, x, /*immutable=*/true); + var yId = new IdentifierExpr(Token.NoToken, y, /*immutable=*/true); + var body = Expr.Gt(xId, yId); + var exists = new ExistsExpr(Token.NoToken, new List () { x, y }, body, /*immutable=*/true); + exists.Body = Expr.Lt(xId, yId); // Changing the body of an immutable ExistsExpr should fail + } + + [Test(), ExpectedException(typeof(InvalidOperationException))] + public void ProtectedLambdaExprBody() + { + var x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", BasicType.Int)); + var y = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", BasicType.Int)); + var xId = new IdentifierExpr(Token.NoToken, x, /*immutable=*/true); + var yId = new IdentifierExpr(Token.NoToken, y, /*immutable=*/true); + var body = Expr.Gt(xId, yId); + var lambda = new LambdaExpr(Token.NoToken, new List(), new List() { x, y}, + null, body, /*immutable=*/true); + lambda.Body = Expr.Lt(xId, yId); // Changing the body of an immutable ExistsExpr should fail + } } } -- cgit v1.2.3