summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Dan Liew <daniel.liew@imperial.ac.uk>2015-02-12 11:51:20 +0000
committerGravatar Dan Liew <daniel.liew@imperial.ac.uk>2015-02-12 11:51:20 +0000
commit59fdb656f09cb4f51fc60d30d8c1bef59f5f908d (patch)
tree3686031fea5c60fd545ccbeb4ee0ceae2b06a73d
parentb1bd1bca3bab1912924e7401cee111bce8c28422 (diff)
Protect Bitvector field of BvExtractExpr when it is immutable.
-rw-r--r--Source/Core/AbsyExpr.cs18
-rw-r--r--Source/UnitTests/CoreTests/ExprImmutability.cs9
2 files changed, 23 insertions, 4 deletions
diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index 2427d856..f3a943b8 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -2969,11 +2969,21 @@ namespace Microsoft.Boogie {
}
public class BvExtractExpr : Expr {
- // FIXME: Protect these fields
- public /*readonly--except in StandardVisitor*/ Expr/*!*/ Bitvector;
+ private /*readonly--except in StandardVisitor*/ Expr/*!*/ _Bitvector;
+ public Expr Bitvector {
+ get {
+ return _Bitvector;
+ }
+ set {
+ if (Immutable)
+ throw new InvalidOperationException("Cannot change BitVector field of an immutable BvExtractExpr");
+
+ _Bitvector = value;
+ }
+ }
[ContractInvariantMethod]
void ObjectInvariant() {
- Contract.Invariant(Bitvector != null);
+ Contract.Invariant(_Bitvector != null);
}
public readonly int Start, End;
@@ -2982,7 +2992,7 @@ namespace Microsoft.Boogie {
: base(tok, immutable) {
Contract.Requires(tok != null);
Contract.Requires(bv != null);
- Bitvector = bv;
+ _Bitvector = bv;
Start = start;
End = end;
if (immutable)
diff --git a/Source/UnitTests/CoreTests/ExprImmutability.cs b/Source/UnitTests/CoreTests/ExprImmutability.cs
index 98e7158f..b83983b6 100644
--- a/Source/UnitTests/CoreTests/ExprImmutability.cs
+++ b/Source/UnitTests/CoreTests/ExprImmutability.cs
@@ -269,6 +269,15 @@ namespace CoreTests
Assert.IsTrue(concat.Immutable);
concat.E1 = lhs; // Should throw
}
+
+ [Test(), ExpectedException(typeof(InvalidOperationException))]
+ public void ProtectedBvExtract()
+ {
+ var bv = new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(0), 32, /*immutable=*/true);
+ var extract = new BvExtractExpr(Token.NoToken, bv, 32, 0, /*immutable=*/true);
+ Assert.IsTrue(extract.Immutable);
+ extract.Bitvector = bv; // Should throw
+ }
}
}