Made invariant of class 'EEDTemplate' robust by changing the design

(replaced public field by private field + getter/setter)

1 files changed, 19 insertions, 4 deletions

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index e0aae39a..93303bd8 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -2838,19 +2838,34 @@ namespace Microsoft.Boogie {
   }

 

   public class EEDTemplate : MiningStrategy {

-    public string/*!*/ reason;

+    private string/*!*/ _reason;

+

+    public string/*!*/ reason

+    {

+      get

+      {

+        Contract.Ensures(Contract.Result<string>() != null);

+        return this._reason;

+      }

+      set

+      {

+        Contract.Requires(value != null);

+        this._reason = value;

+      }

+    }

+

     public List<Expr/*!*/>/*!*/ exprList;

+

     [ContractInvariantMethod]

     void ObjectInvariant() {

-      Contract.Invariant(reason != null);

+      Contract.Invariant(this._reason != null);

       Contract.Invariant(cce.NonNullElements(exprList));

     }

 

-

     public EEDTemplate(string reason, List<Expr/*!*/>/*!*/ exprList) {

       Contract.Requires(reason != null);

       Contract.Requires(cce.NonNullElements(exprList));

-      this.reason = reason;

+      this._reason = reason;

       this.exprList = exprList;

     }

   }