diff options
Diffstat (limited to 'Source/Core')
-rw-r--r-- | Source/Core/Absy.cs | 20 |
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
|