diff options
author | Dan Liew <daniel.liew@imperial.ac.uk> | 2015-01-29 03:47:05 +0000 |
---|---|---|
committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2015-01-29 03:47:05 +0000 |
commit | cef89809053b0679019491a227ed03c98be44854 (patch) | |
tree | 12cb272e3b1f0a56f0bdd7bcee111d2be2d863a9 | |
parent | 9ecdcd65b9173736a191662072865ec0bb075c04 (diff) |
Protect the NAryExpr.Fun field when the NAryExpr is immutable.
Add a unit test for this. We need to protect the Args field too
but that is going to be much harder to enforce.
-rw-r--r-- | Source/Core/AbsyExpr.cs | 17 | ||||
-rw-r--r-- | Source/UnitTests/CoreTests/ExprImmutability.cs | 7 |
2 files changed, 21 insertions, 3 deletions
diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs index e6c21e1f..75a5741a 100644 --- a/Source/Core/AbsyExpr.cs +++ b/Source/Core/AbsyExpr.cs @@ -2230,8 +2230,19 @@ namespace Microsoft.Boogie { public class NAryExpr : Expr {
[Additive]
[Peer]
- // FIXME: Protect these fields
- public IAppliable/*!*/ Fun;
+ private IAppliable _Fun;
+ public IAppliable/*!*/ Fun {
+ get {
+ return _Fun;
+ }
+ set {
+ if (Immutable)
+ throw new InvalidOperationException("Cannot change Function used by Immutable NAryExpr");
+
+ _Fun = value;
+ }
+ }
+ // FIXME: Protect this field when immutable
public List<Expr> Args;
[ContractInvariantMethod]
@@ -2251,7 +2262,7 @@ namespace Microsoft.Boogie { Contract.Requires(tok != null);
Contract.Requires(fun != null);
Contract.Requires(args != null);
- Fun = fun;
+ _Fun = fun;
Args = args;
Contract.Assert(Contract.ForAll(0, args.Count, index => args[index] != null));
if (immutable)
diff --git a/Source/UnitTests/CoreTests/ExprImmutability.cs b/Source/UnitTests/CoreTests/ExprImmutability.cs index e13feca7..aff0acea 100644 --- a/Source/UnitTests/CoreTests/ExprImmutability.cs +++ b/Source/UnitTests/CoreTests/ExprImmutability.cs @@ -96,6 +96,13 @@ namespace CoreTests var e = new OldExpr(Token.NoToken, Expr.True, /*immutable=*/ true); e.Expr = Expr.False; } + + [Test(), ExpectedException(typeof(InvalidOperationException))] + public void ProtectedNAryFunc() + { + var e = GetUnTypedImmutableNAry(); + e.Fun = new BinaryOperator(Token.NoToken, BinaryOperator.Opcode.Sub); + } } } |