Made invariant of class 'EEDTemplate' robust by:

- making field private
- exposing an IEnumerable
- copying incoming list
(with help from David Rohr)

1 files changed, 16 insertions, 2 deletions

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));

     }