diff options
| author |  0biha <unknown> | 2015-01-01 18:14:45 +0100 |
|---|---|---|
| committer | 0biha <unknown> | 2015-01-01 18:14:45 +0100 |
| commit | 1ed6c26e0ef401481a37aac2c2838b7e96bfa3b4 (patch) | |
| tree | 4996fcabde27aa89eb64646d2f5dd672db74e994 /Source/Core/AbsyCmd.cs | |
| parent | 4eb8fc7008cc586eed361a171c5a96f1f058192c (diff) | |
Made 2 invariants of class 'IfCmd' robust by changing the design
(replaced public fields by private fields + getters/setters)
Diffstat (limited to 'Source/Core/AbsyCmd.cs')
| -rw-r--r-- | Source/Core/AbsyCmd.cs | 62 |
1 files changed, 52 insertions, 10 deletions
diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index 93303bd8..88a204a4 100644 --- a/Source/Core/AbsyCmd.cs +++ b/Source/Core/AbsyCmd.cs @@ -746,16 +746,58 @@ namespace Microsoft.Boogie { public class IfCmd : StructuredCmd {
public Expr Guard;
- public StmtList/*!*/ thn;
- public IfCmd elseIf;
- public StmtList elseBlock;
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(thn != null);
- Contract.Invariant(elseIf == null || elseBlock == null);
+
+ private StmtList/*!*/ _thn;
+
+ public StmtList/*!*/ thn
+ {
+ get
+ {
+ Contract.Ensures(Contract.Result<StmtList>() != null);
+ return this._thn;
+ }
+ set
+ {
+ Contract.Requires(value != null);
+ this._thn = value;
+ }
+ }
+
+ private IfCmd _elseIf;
+
+ public IfCmd elseIf
+ {
+ get
+ {
+ return this._elseIf;
+ }
+ set
+ {
+ Contract.Requires(value == null || this.elseBlock == null);
+ this._elseIf = value;
+ }
}
+ private StmtList _elseBlock;
+ public StmtList elseBlock
+ {
+ get
+ {
+ return this._elseBlock;
+ }
+ set
+ {
+ Contract.Requires(value == null || this.elseIf == null);
+ this._elseBlock = value;
+ }
+ }
+
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(this._thn != null);
+ Contract.Invariant(this._elseIf == null || this._elseBlock == null);
+ }
public IfCmd(IToken/*!*/ tok, Expr guard, StmtList/*!*/ thn, IfCmd elseIf, StmtList elseBlock)
: base(tok) {
@@ -763,9 +805,9 @@ namespace Microsoft.Boogie { Contract.Requires(thn != null);
Contract.Requires(elseIf == null || elseBlock == null);
this.Guard = guard;
- this.thn = thn;
- this.elseIf = elseIf;
- this.elseBlock = elseBlock;
+ this._thn = thn;
+ this._elseIf = elseIf;
+ this._elseBlock = elseBlock;
}
public override void Emit(TokenTextWriter stream, int level) {
|