Made invariant of class 'Choice' robust by changing the design (replaced public field by private field + getter/setter).

1 files changed, 16 insertions, 3 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index b2966c0b..fe0c80d1 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -4258,14 +4258,27 @@ namespace Microsoft.Boogie {
   public class Choice : CompoundRE {

     [ContractInvariantMethod]

     void ObjectInvariant() {

-      Contract.Invariant(rs != null);

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

+    }

+

+    private List<RE>/*!*/ _rs;

+    

+    public List<RE>/*!*/ rs { //Rename this (and _rs) if possible

+      get {

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

+        return this._rs;

+      }

+      set {

+        Contract.Requires(value != null);

+        this._rs = value;

+      }

     }

 

-    public List<RE>/*!*/ rs;

     public Choice(List<RE> operands) {

       Contract.Requires(operands != null);

-      rs = operands;

+      this._rs = operands;

     }

+

     public override void Emit(TokenTextWriter stream, int level) {

       //Contract.Requires(stream != null);

       stream.WriteLine();