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

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

1 files changed, 16 insertions, 4 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index e2e37345..4b4dfd9e 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -38,15 +38,27 @@ namespace Microsoft.Boogie.AbstractInterpretation {
   }

 

   public class ProcedureSummaryEntry {

-    public HashSet<CallSite>/*!*/ ReturnPoints; // whenever OnExit changes, we start analysis again at all the ReturnPoints

+

+    private HashSet<CallSite>/*!*/ _returnPoints; // whenever OnExit changes, we start analysis again at all the ReturnPoints

+

+    public HashSet<CallSite>/*!*/ ReturnPoints {

+      get {

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

+        return this._returnPoints;

+      }

+      set {

+        Contract.Requires(value != null);

+        this._returnPoints = value;

+      }

+    }

+

     [ContractInvariantMethod]

     void ObjectInvariant() {

-      Contract.Invariant(ReturnPoints != null);

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

     }

 

-

     public ProcedureSummaryEntry() {

-      this.ReturnPoints = new HashSet<CallSite>();

+      this._returnPoints = new HashSet<CallSite>();

     }

 

   } // class