From 506c17c312bf12188a9b1eabcdf80a71f92d9bb9 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Thu, 29 Jan 2015 03:12:00 +0000
Subject: Add some unit tests to check the enforcement of Expr immutability.
 For IdentifierExpr and the Type field of Expr.

There are lots of places where it still isn't enforced but hopefully
we'll fix those in due time.
---
 Source/UnitTests/CoreTests/CoreTests.csproj    |  1 +
 Source/UnitTests/CoreTests/ExprImmutability.cs | 94 ++++++++++++++++++++++++++
 2 files changed, 95 insertions(+)
 create mode 100644 Source/UnitTests/CoreTests/ExprImmutability.cs

(limited to 'Source/UnitTests')

diff --git a/Source/UnitTests/CoreTests/CoreTests.csproj b/Source/UnitTests/CoreTests/CoreTests.csproj
index 76f7b985..9b319d85 100644
--- a/Source/UnitTests/CoreTests/CoreTests.csproj
+++ b/Source/UnitTests/CoreTests/CoreTests.csproj
@@ -47,6 +47,7 @@
     <Compile Include="ExprEquality.cs" />
     <Compile Include="Properties\AssemblyInfo.cs" />
     <Compile Include="ExprTypeChecking.cs" />
+    <Compile Include="ExprImmutability.cs" />
   </ItemGroup>
   <ItemGroup>
     <None Include="packages.config" />
diff --git a/Source/UnitTests/CoreTests/ExprImmutability.cs b/Source/UnitTests/CoreTests/ExprImmutability.cs
new file mode 100644
index 00000000..68b71083
--- /dev/null
+++ b/Source/UnitTests/CoreTests/ExprImmutability.cs
@@ -0,0 +1,94 @@
+using NUnit.Framework;
+using System;
+using Microsoft.Boogie;
+using System.Collections.Generic;
+
+namespace CoreTests
+{
+    [TestFixture()]
+    public class ExprImmutability : IErrorSink
+    {
+
+        public void Error(IToken tok, string msg)
+        {
+            Assert.Fail (msg);
+        }
+
+        [Test(), ExpectedException(typeof(InvalidOperationException))]
+        public void IdentifierExprName()
+        {
+            var id = new IdentifierExpr(Token.NoToken, "foo", BasicType.Bool, /*immutable=*/true);
+            Assert.IsTrue(id.Immutable);
+            id.Name = "foo2";
+        }
+
+        [Test(), ExpectedException(typeof(InvalidOperationException))]
+        public void IdentifierExprDecl()
+        {
+            var id = new IdentifierExpr(Token.NoToken, "foo", BasicType.Bool, /*immutable=*/true);
+            Assert.IsTrue(id.Immutable);
+            var typedIdent = new TypedIdent(Token.NoToken, "foo2", BasicType.Bool);
+            id.Decl = new GlobalVariable(Token.NoToken, typedIdent);
+        }
+
+        private NAryExpr GetUnTypedImmutableNAry()
+        {
+            var id = new IdentifierExpr(Token.NoToken, "foo", BasicType.Bool, /*immutable=*/true);
+            Assert.IsTrue(id.Immutable);
+            Assert.IsTrue(id.Type.IsBool);
+            var e = new NAryExpr(Token.NoToken, new BinaryOperator(Token.NoToken, BinaryOperator.Opcode.And), new List<Expr>() {
+                id,
+                id
+            }, /*immutable=*/true);
+            Assert.IsNull(e.Type);
+            Assert.IsTrue(e.Immutable);
+            return e;
+        }
+
+        [Test()]
+        public void ProtectedExprType()
+        {
+            var e = GetUnTypedImmutableNAry();
+
+            // Now Typecheck
+            // Even though it's immutable we allow the TypeCheck field to be set if the Expr has never been type checked
+            var TC = new TypecheckingContext(this);
+            e.Typecheck(TC);
+            Assert.IsNotNull(e.Type);
+            Assert.IsTrue(e.Type.IsBool);
+        }
+
+        [Test(), ExpectedException(typeof(InvalidOperationException))]
+        public void ProtectedExprChangeTypeFail()
+        {
+            var e = GetUnTypedImmutableNAry();
+
+            // Now Typecheck
+            // Even though it's immutable we allow the TypeCheck field to be set if the Expr has never been type checked
+            var TC = new TypecheckingContext(this);
+            e.Typecheck(TC);
+            Assert.IsNotNull(e.Type);
+            Assert.IsTrue(e.Type.IsBool);
+
+            // Trying to modify the Type to a different Type now should fail
+            e.Type = BasicType.Int;
+        }
+
+        [Test()]
+        public void ProtectedExprTypeChangeTypeSucceed()
+        {
+            var e = GetUnTypedImmutableNAry();
+
+            // Now Typecheck
+            // Even though it's immutable we allow the TypeCheck field to be set if the Expr has never been type checked
+            var TC = new TypecheckingContext(this);
+            e.Typecheck(TC);
+            Assert.IsNotNull(e.Type);
+            Assert.IsTrue(e.Type.IsBool);
+
+            // Trying to assign the same Type should succeed
+            e.Type = BasicType.Bool;
+        }
+    }
+}
+
-- 
cgit v1.2.3