diff options
| author |  0biha <unknown> | 2014-12-09 17:11:41 +0100 |
|---|---|---|
| committer | 0biha <unknown> | 2014-12-09 17:11:41 +0100 |
| commit | eca04b7217d923dd8fcf67198654a66f5e0f26c8 (patch) | |
| tree | c692a8ed460da499d03cca39196e8fbade53a46a | |
| parent | edc37cbeb0f4c46c844949c25bf6d94ffaa74222 (diff) | |
Made invariant of class 'Absy' robust by changing the design (added getter/setter instead of public field).
| -rw-r--r-- | Source/Core/Absy.cs | 16 | ||||
| -rw-r--r-- | Source/Core/Util.cs | 9 |
2 files changed, 21 insertions, 4 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index b491f872..4f743910 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -83,13 +83,23 @@ namespace Microsoft.Boogie { [ContractClass(typeof(AbsyContracts))]
public abstract class Absy {
- public IToken/*!*/ tok;
+ private IToken/*!*/ _tok;
private int uniqueId;
[ContractInvariantMethod]
void ObjectInvariant() {
- Contract.Invariant(tok != null);
+ Contract.Invariant(this._tok != null);
}
+ public IToken tok { //Rename this property and "_tok" if possible
+ get {
+ Contract.Ensures(Contract.Result<IToken>() != null);
+ return this._tok;
+ }
+ set {
+ Contract.Requires(value != null);
+ this._tok = value;
+ }
+ }
public int Line {
get {
@@ -104,7 +114,7 @@ namespace Microsoft.Boogie { public Absy(IToken tok) {
Contract.Requires(tok != null);
- this.tok = tok;
+ this._tok = tok;
this.uniqueId = AbsyNodeCount++;
}
diff --git a/Source/Core/Util.cs b/Source/Core/Util.cs index 06e4fcf0..b28ac042 100644 --- a/Source/Core/Util.cs +++ b/Source/Core/Util.cs @@ -226,7 +226,14 @@ namespace Microsoft.Boogie { public void SetToken(Absy absy) {
Contract.Requires(absy != null);
- this.SetToken(ref absy.tok);
+ this.SetToken(t => absy.tok = t);
+ }
+
+ public void SetToken(Action<IToken> setter) {
+ Contract.Requires(setter != null);
+ if (this.setTokens) {
+ setter(this.CurrentToken);
+ }
}
public void SetToken(ref IToken tok) {
|