Merging changes from 0biha/BoogieInvariantFixesII

1 files changed, 32 insertions, 7 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index f348c788..7622cbdf 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

@@ -2856,10 +2868,23 @@ namespace Microsoft.Boogie {
 

   public class Ensures : Absy, IPotentialErrorNode {

     public readonly bool Free;

-    public Expr/*!*/ Condition;

+

+    private Expr/*!*/ _condition;

+ 	  

+ 	  public Expr/*!*/ Condition {

+ 	    get {

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

+ 	      return this._condition;

+ 	    }

+ 	    set {

+ 	      Contract.Requires(value != null);

+ 	      this._condition = value;

+ 	    }

+ 	  }

+

     [ContractInvariantMethod]

     void ObjectInvariant() {

-      Contract.Invariant(Condition != null);

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

       Contract.Invariant(errorData == null || errorData is string);

     }

 

@@ -2899,7 +2924,7 @@ namespace Microsoft.Boogie {
       Contract.Requires(condition != null);

       Contract.Requires(token != null);

       this.Free = free;

-      this.Condition = condition;

+      this._condition = condition; 

       this.Comment = comment;

       this.Attributes = kv;

     }