diff options
| author |  0biha <unknown> | 2014-12-15 16:58:58 +0100 |
|---|---|---|
| committer | 0biha <unknown> | 2014-12-15 16:58:58 +0100 |
| commit | f3a090c00f6d40e6020d1c6a2b5f8e822b8375ef (patch) | |
| tree | 1349479139435f6f7f805739b1d47927f06c9186 /Source/Core/Absy.cs | |
| parent | a52c0284e81842302786cfc1c8cca6b7be2ac6dc (diff) | |
Made 2 invariants of class 'TypepedIdent' robust by changing the design (replaced public fields by private fields + getters/setters).
Diffstat (limited to 'Source/Core/Absy.cs')
| -rw-r--r-- | Source/Core/Absy.cs | 37 |
1 files changed, 31 insertions, 6 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 35232e6b..b2966c0b 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -3959,12 +3959,37 @@ namespace Microsoft.Boogie { public class TypedIdent : Absy {
public const string NoName = "";
- public string/*!*/ Name;
- public Type/*!*/ Type;
+
+ private string/*!*/ _name;
+
+ public string/*!*/ Name {
+ get {
+ Contract.Ensures(Contract.Result<string>() != null);
+ return this._name;
+ }
+ set {
+ Contract.Requires(value != null);
+ this._name = value;
+ }
+ }
+
+ private Type/*!*/ _type;
+
+ public Type/*!*/ Type {
+ get {
+ Contract.Ensures(Contract.Result<Type>() != null);
+ return this._type;
+ }
+ set {
+ Contract.Requires(value != null);
+ this._type = value;
+ }
+ }
+
[ContractInvariantMethod]
void ObjectInvariant() {
- Contract.Invariant(Name != null);
- Contract.Invariant(Type != null);
+ Contract.Invariant(this._name != null);
+ Contract.Invariant(this._type != null);
}
public Expr WhereExpr;
@@ -3984,8 +4009,8 @@ namespace Microsoft.Boogie { Contract.Requires(name != null);
Contract.Requires(type != null);
Contract.Ensures(this.WhereExpr == whereExpr);
- this.Name = name;
- this.Type = type;
+ this._name = name;
+ this._type = type;
this.WhereExpr = whereExpr;
}
public bool HasName {
|