diff options
author | 0biha <unknown> | 2014-12-19 10:34:30 +0100 |
---|---|---|
committer | 0biha <unknown> | 2014-12-19 10:34:30 +0100 |
commit | 6829b36b0323a6fa11ff1ccd7da6df535171436a (patch) | |
tree | 969debdb078af602a088a5a8778bf1000ff586f8 /Source | |
parent | 86cb1bc74ca8b0242131145ce9d4cbab085c02fd (diff) |
Made invariant of class 'Ensures' robust by changing the design (replaced public field by private field + getter/setter).
Diffstat (limited to 'Source')
-rw-r--r-- | Source/Core/Absy.cs | 19 |
1 files changed, 16 insertions, 3 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 37c86d59..e2e37345 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -2780,10 +2780,23 @@ namespace Microsoft.Boogie { public class Ensures : Absy, IPotentialErrorNode {
public readonly bool Free;
- public Expr/*!*/ Condition;
+
+ private Expr/*!*/ _condition;
+
+ public Expr/*!*/ Condition {
+ get {
+ Contract.Ensures(Contract.Result<Expr>() != null);
+ return this._condition;
+ }
+ set {
+ Contract.Requires(value != null);
+ this._condition = value;
+ }
+ }
+
[ContractInvariantMethod]
void ObjectInvariant() {
- Contract.Invariant(Condition != null);
+ Contract.Invariant(this._condition != null);
Contract.Invariant(errorData == null || errorData is string);
}
@@ -2823,7 +2836,7 @@ namespace Microsoft.Boogie { Contract.Requires(condition != null);
Contract.Requires(token != null);
this.Free = free;
- this.Condition = condition;
+ this._condition = condition;
this.Comment = comment;
this.Attributes = kv;
}
|