diff options
author | 0biha <unknown> | 2014-12-23 16:47:50 +0100 |
---|---|---|
committer | 0biha <unknown> | 2014-12-23 16:47:50 +0100 |
commit | 1454a11306c5b16d1650814aec7502f20c7cce1a (patch) | |
tree | 7657649b45291036501b4ccb3c21aefadebc6d46 /Source/Core | |
parent | e58edfeb28cfff929954606203a6046d79904d9b (diff) |
Made invariant of class 'ProcedureSummaryEntry' robust by changing the design
(replaced public field by private field + getter/setter).
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
|