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