From 1ed6c26e0ef401481a37aac2c2838b7e96bfa3b4 Mon Sep 17 00:00:00 2001
From: 0biha <unknown>
Date: Thu, 1 Jan 2015 18:14:45 +0100
Subject: Made 2 invariants of class 'IfCmd' robust by changing the design
 (replaced public fields by private fields + getters/setters)

---
 Source/Core/AbsyCmd.cs | 62 ++++++++++++++++++++++++++++++++++++++++++--------
 1 file changed, 52 insertions(+), 10 deletions(-)

(limited to 'Source/Core/AbsyCmd.cs')

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) {
-- 
cgit v1.2.3