diff options
author | 0biha <unknown> | 2015-01-01 18:23:20 +0100 |
---|---|---|
committer | 0biha <unknown> | 2015-01-01 18:23:20 +0100 |
commit | 79c6aec21f69a6d8968fdd96834d591c1e505260 (patch) | |
tree | df95d4ae79dbb323e61b2d392f0415ac46c2809a /Source/Core | |
parent | 1ed6c26e0ef401481a37aac2c2838b7e96bfa3b4 (diff) |
Made invariant of class 'IfThenElse' robust by changing the design
(replaced public field by private field + getter/setter)
Diffstat (limited to 'Source/Core')
-rw-r--r-- | Source/Core/AbsyExpr.cs | 24 | ||||
-rw-r--r-- | Source/Core/Util.cs | 6 |
2 files changed, 25 insertions, 5 deletions
diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs index 8918115b..e2113ab5 100644 --- a/Source/Core/AbsyExpr.cs +++ b/Source/Core/AbsyExpr.cs @@ -2530,16 +2530,30 @@ namespace Microsoft.Boogie { public class IfThenElse : IAppliable {
- public IToken/*!*/ tok;
+ private IToken/*!*/ _tok;
+
+ public IToken/*!*/ tok
+ {
+ get
+ {
+ Contract.Ensures(Contract.Result<IToken>() != null);
+ return this._tok;
+ }
+ set
+ {
+ Contract.Requires(value != null);
+ this._tok = value;
+ }
+ }
+
[ContractInvariantMethod]
void ObjectInvariant() {
- Contract.Invariant(tok != null);
+ Contract.Invariant(this._tok != null);
}
-
public IfThenElse(IToken tok) {
Contract.Requires(tok != null);
- this.tok = tok;
+ this._tok = tok;
}
public string/*!*/ FunctionName {
@@ -2566,7 +2580,7 @@ namespace Microsoft.Boogie { public void Emit(List<Expr> args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {
//Contract.Requires(stream != null);
//Contract.Requires(args != null);
- stream.SetToken(ref this.tok);
+ stream.SetToken(this);
Contract.Assert(args.Count == 3);
stream.push();
stream.Write("(if ");
diff --git a/Source/Core/Util.cs b/Source/Core/Util.cs index b28ac042..73008742 100644 --- a/Source/Core/Util.cs +++ b/Source/Core/Util.cs @@ -229,6 +229,12 @@ namespace Microsoft.Boogie { this.SetToken(t => absy.tok = t);
}
+ public void SetToken(IfThenElse expr)
+ {
+ Contract.Requires(expr != null);
+ this.SetToken(t => expr.tok = t);
+ }
+
public void SetToken(Action<IToken> setter) {
Contract.Requires(setter != null);
if (this.setTokens) {
|