diff options
| author |  0biha <unknown> | 2014-12-15 17:26:59 +0100 |
|---|---|---|
| committer | 0biha <unknown> | 2014-12-15 17:26:59 +0100 |
| commit | 5b2af140747404e55afe38395a51e4a7866ccc52 (patch) | |
| tree | 3e6e503c6bf878dbd94651d5e6a6b9303b332ae0 /Source/Core/Absy.cs | |
| parent | ffa1e5ea550a6f3c4e88c1fe82691ca128bafd84 (diff) | |
Made 2 invariants of class 'Sequential' 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 | 43 |
1 files changed, 34 insertions, 9 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index fe0c80d1..5bd52d90 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -4227,20 +4227,45 @@ namespace Microsoft.Boogie { }
}
public class Sequential : CompoundRE {
- public RE/*!*/ first;
- public RE/*!*/ second;
+ private RE/*!*/ _first;
+
+ public RE/*!*/ first {
+ get {
+ Contract.Ensures(Contract.Result<RE>() != null);
+ return this._first;
+ }
+ set {
+ Contract.Requires(value != null);
+ this._first = value;
+ }
+ }
+
+ private RE/*!*/ _second;
+
+ public RE/*!*/ second {
+ get {
+ Contract.Ensures(Contract.Result<RE>() != null);
+ return this._second;
+ }
+ set {
+ Contract.Requires(value != null);
+ this._second = value;
+ }
+ }
+
[ContractInvariantMethod]
void ObjectInvariant() {
- Contract.Invariant(first != null);
- Contract.Invariant(second != null);
+ Contract.Invariant(this._first != null);
+ Contract.Invariant(this._second != null);
}
- public Sequential(RE a, RE b) {
- Contract.Requires(b != null);
- Contract.Requires(a != null);
- first = a;
- second = b;
+ public Sequential(RE first, RE second) {
+ Contract.Requires(first != null);
+ Contract.Requires(second != null);
+ this._first = first;
+ this._second = second;
}
+
public override void Emit(TokenTextWriter stream, int level) {
//Contract.Requires(stream != null);
stream.WriteLine();
|