From 8b29c0e6b307ccfa65970d7a344bb94d433813fe Mon Sep 17 00:00:00 2001
From: 0biha <unknown>
Date: Mon, 5 Jan 2015 14:52:47 +0100
Subject: Made invariant of class 'AtomicRE' robust by changing the design
 (replaced public field by private field + getter/setter)

---
 Source/Core/Absy.cs | 24 +++++++++++++++++++++---
 1 file changed, 21 insertions(+), 3 deletions(-)

(limited to 'Source/Core')

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 56ccfa9e..9fb44108 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -4218,24 +4218,42 @@ namespace Microsoft.Boogie {
     }
   }
   public class AtomicRE : RE {
-    public Block/*!*/ b;
+    private Block/*!*/ _b;
+
+    public Block b
+    {
+      get
+      {
+        Contract.Ensures(Contract.Result<Block>() != null);
+        return this._b;
+      }
+      set
+      {
+        Contract.Requires(value != null);
+        this._b = value;
+      }
+    }
+
     [ContractInvariantMethod]
     void ObjectInvariant() {
-      Contract.Invariant(b != null);
+      Contract.Invariant(this._b != null);
     }
 
     public AtomicRE(Block block) {
       Contract.Requires(block != null);
-      b = block;
+      this._b = block;
     }
+
     public override void Resolve(ResolutionContext rc) {
       //Contract.Requires(rc != null);
       b.Resolve(rc);
     }
+
     public override void Typecheck(TypecheckingContext tc) {
       //Contract.Requires(tc != null);
       b.Typecheck(tc);
     }
+
     public override void Emit(TokenTextWriter stream, int level) {
       //Contract.Requires(stream != null);
       b.Emit(stream, level);
-- 
cgit v1.2.3