diff options
author | Dan Liew <daniel.liew@imperial.ac.uk> | 2015-02-12 10:52:46 +0000 |
---|---|---|
committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2015-02-12 10:52:46 +0000 |
commit | 1f8368fd50c720fe8080d6724e8bbfaecb6f486d (patch) | |
tree | d9825284ac43ba4e6eee182e474a55441f67328f /Source/UnitTests | |
parent | 882a965c3d212a2d79825e0d06200758ce3b9db4 (diff) |
Protect the Args field of NAryExpr when it is immutable.
* Made changing the reference throw an exception if the NAryExpr was
constructed as immutable
* Changed the type of NAryExpr.Args to be IList<Expr> rather than
List<Expr> so that when the NAryExpr is immutable I can return
``_Args.AsReadOnly()`` (instead of ``_Args``) which returns a read
only wrapper around the List<Expr> so that clients cannot change the
list.
I came across two problems
* Making this change required changing types all over the place (from
List<Expr> to IList<Expr>). I feel that changes are extensive enough
that there's a good chance that out of tree clients using Boogie's
libraries might break. I've waited for a code review but this didn't
happen so I'm committing anyway.
* I came across something that looks like bad design of the IAppliable
interface which potentially breaks immutability enforcement. I've left
this as a "FIXME" in this. Here's the problematic method.
```
Type Typecheck(ref List<Expr>/*!*/ args, out
TypeParamInstantiation/*!*/ tpInstantiation, TypecheckingContext/*!*/
tc);
```
It potentially allows the instance of the args to be changed which
seems very suspect.
Diffstat (limited to 'Source/UnitTests')
-rw-r--r-- | Source/UnitTests/CoreTests/ExprImmutability.cs | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/Source/UnitTests/CoreTests/ExprImmutability.cs b/Source/UnitTests/CoreTests/ExprImmutability.cs index 3dd2e427..a26f8b8b 100644 --- a/Source/UnitTests/CoreTests/ExprImmutability.cs +++ b/Source/UnitTests/CoreTests/ExprImmutability.cs @@ -199,6 +199,20 @@ namespace CoreTests e.Fun = new BinaryOperator(Token.NoToken, BinaryOperator.Opcode.Sub); } + [Test(), ExpectedException(typeof(NotSupportedException))] + public void ProtectedNAryArgsList() + { + var e = GetUnTypedImmutableNAry(); + e.Args.Add(null); + } + + [Test(), ExpectedException(typeof(InvalidOperationException))] + public void ProtectedNAryArgs() + { + var e = GetUnTypedImmutableNAry(); + e.Args = new List<Expr>(); + } + [Test(), ExpectedException(typeof(InvalidOperationException))] public void ProtectedForAllExprBody() { |