diff options
| author |  0biha <unknown> | 2014-12-09 18:48:33 +0100 |
|---|---|---|
| committer | 0biha <unknown> | 2014-12-09 18:48:33 +0100 |
| commit | 5cd65c78dbea38def191147c65a4450934fc068f (patch) | |
| tree | fa126fe1f1284a7b208cae68b364644b33dfcf0f /Source/Core/Absy.cs | |
| parent | ed255f339f5144c421d8e1d66a9908c7ee6237d0 (diff) | |
Made invariant of class 'Variable' robust by changing the design (replaced public field by private field + getter/setter).
Diffstat (limited to 'Source/Core/Absy.cs')
| -rw-r--r-- | Source/Core/Absy.cs | 20 |
1 files changed, 16 insertions, 4 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 80ef5551..ac4f3d63 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -1825,24 +1825,36 @@ namespace Microsoft.Boogie { }
public abstract class Variable : NamedDeclaration {
- public TypedIdent/*!*/ TypedIdent;
+ private TypedIdent/*!*/ typedIdent;
+
+ public TypedIdent TypedIdent {
+ get {
+ Contract.Ensures(Contract.Result<TypedIdent>() != null);
+ return this.typedIdent;
+ }
+ set {
+ Contract.Requires(value != null);
+ this.typedIdent = value;
+ }
+ }
+
[ContractInvariantMethod]
void ObjectInvariant() {
- Contract.Invariant(TypedIdent != null);
+ Contract.Invariant(this.typedIdent != null);
}
public Variable(IToken/*!*/ tok, TypedIdent/*!*/ typedIdent)
: base(tok, typedIdent.Name) {
Contract.Requires(tok != null);
Contract.Requires(typedIdent != null);
- this.TypedIdent = typedIdent;
+ this.typedIdent = typedIdent;
}
public Variable(IToken/*!*/ tok, TypedIdent/*!*/ typedIdent, QKeyValue kv)
: base(tok, typedIdent.Name) {
Contract.Requires(tok != null);
Contract.Requires(typedIdent != null);
- this.TypedIdent = typedIdent;
+ this.typedIdent = typedIdent;
this.Attributes = kv;
}
|