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.

2 files changed, 95 insertions, 0 deletions

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;
+        }
+    }
+}
+