diff options
author | 0biha <unknown> | 2015-01-01 17:23:10 +0100 |
---|---|---|
committer | 0biha <unknown> | 2015-01-01 17:23:10 +0100 |
commit | 820bde31cbd5526f56bbe8d0bde2b37812b25b3d (patch) | |
tree | 89362913a3c6c7ab768e5732fa192f658d403556 /Source/Core/AbsyCmd.cs | |
parent | f8727eec039b443909e7737a852141f36f8e7b3b (diff) |
Made invariant of class 'StructuredCmd' robust by changing the design
(replaced public field by private field + getter/setter)
Diffstat (limited to 'Source/Core/AbsyCmd.cs')
-rw-r--r-- | Source/Core/AbsyCmd.cs | 21 |
1 files changed, 18 insertions, 3 deletions
diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index dc57e7fc..e0aae39a 100644 --- a/Source/Core/AbsyCmd.cs +++ b/Source/Core/AbsyCmd.cs @@ -705,15 +705,30 @@ namespace Microsoft.Boogie { [ContractClass(typeof(StructuredCmdContracts))]
public abstract class StructuredCmd {
- 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 StructuredCmd(IToken tok) {
Contract.Requires(tok != null);
- this.tok = tok;
+ this._tok = tok;
}
public abstract void Emit(TokenTextWriter/*!*/ stream, int level);
|