From fb2b56ff6734b210315f1bb31f27552d0b0ebaa4 Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Fri, 9 Jan 2015 15:43:46 +0100
Subject: Made invariant of class 'EEDTemplate' robust by: - making field
 private - exposing an IEnumerable - copying incoming list (with help from
 David Rohr)

---
 Source/Core/AbsyCmd.cs | 18 ++++++++++++++++--
 1 file changed, 16 insertions(+), 2 deletions(-)

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

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index 7a47a743..89a3d1d1 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -2756,11 +2756,25 @@ namespace Microsoft.Boogie {
 
   public class EEDTemplate : MiningStrategy {
     public string/*!*/ reason;
-    public List<Expr/*!*/>/*!*/ exprList;
+    private List<Expr/*!*/>/*!*/ exprList;
+    public IEnumerable<Expr> Expressions
+    {
+      get
+      {
+        Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<Expr>>()));
+        return this.exprList.AsReadOnly();
+      }
+      set
+      {
+        Contract.Requires(cce.NonNullElements(value));
+        this.exprList = new List<Expr>(value);
+      }
+    }
+
     [ContractInvariantMethod]
     void ObjectInvariant() {
       Contract.Invariant(reason != null);
-      Contract.Invariant(cce.NonNullElements(exprList));
+      Contract.Invariant(cce.NonNullElements(this.exprList));
     }
 
 
-- 
cgit v1.2.3