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