diff options
| -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); + } } } |