From 79c6aec21f69a6d8968fdd96834d591c1e505260 Mon Sep 17 00:00:00 2001
From: 0biha <unknown>
Date: Thu, 1 Jan 2015 18:23:20 +0100
Subject: Made invariant of class 'IfThenElse' robust by changing the design
 (replaced public field by private field + getter/setter)

---
 Source/Core/AbsyExpr.cs | 24 +++++++++++++++++++-----
 Source/Core/Util.cs     |  6 ++++++
 2 files changed, 25 insertions(+), 5 deletions(-)

(limited to 'Source/Core')

diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index 8918115b..e2113ab5 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -2530,16 +2530,30 @@ namespace Microsoft.Boogie {
 
   public class IfThenElse : IAppliable {
 
-    public IToken/*!*/ tok;
+    private IToken/*!*/ _tok;
+
+    public IToken/*!*/ tok
+    {
+      get
+      {
+        Contract.Ensures(Contract.Result<IToken>() != null);
+        return this._tok;
+      }
+      set
+      {
+        Contract.Requires(value != null);
+        this._tok = value;
+      }
+    }
+    
     [ContractInvariantMethod]
     void ObjectInvariant() {
-      Contract.Invariant(tok != null);
+      Contract.Invariant(this._tok != null);
     }
 
-
     public IfThenElse(IToken tok) {
       Contract.Requires(tok != null);
-      this.tok = tok;
+      this._tok = tok;
     }
 
     public string/*!*/ FunctionName {
@@ -2566,7 +2580,7 @@ namespace Microsoft.Boogie {
     public void Emit(List<Expr> args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {
       //Contract.Requires(stream != null);
       //Contract.Requires(args != null);
-      stream.SetToken(ref this.tok);
+      stream.SetToken(this);
       Contract.Assert(args.Count == 3);
       stream.push();
       stream.Write("(if ");     
diff --git a/Source/Core/Util.cs b/Source/Core/Util.cs
index b28ac042..73008742 100644
--- a/Source/Core/Util.cs
+++ b/Source/Core/Util.cs
@@ -229,6 +229,12 @@ namespace Microsoft.Boogie {
       this.SetToken(t => absy.tok = t);
     }
 
+    public void SetToken(IfThenElse expr)
+    {
+      Contract.Requires(expr != null);
+      this.SetToken(t => expr.tok = t);
+    }
+
     public void SetToken(Action<IToken> setter) {
       Contract.Requires(setter != null);
       if (this.setTokens) {
-- 
cgit v1.2.3