From fe2bc442dc600f540930f8a119722ca80f7da8e3 Mon Sep 17 00:00:00 2001
From: 0biha <unknown>
Date: Fri, 19 Dec 2014 13:05:19 +0100
Subject: Made 2 invariants of type 'StateCmd' robust by changing the design
 (replaced public fields by private fields + getters/setters).

---
 Source/Core/AbsyCmd.cs | 35 +++++++++++++++++++++++++++++------
 1 file changed, 29 insertions(+), 6 deletions(-)

(limited to 'Source/Core')

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index 2c00bd8b..3f675317 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -1724,20 +1724,43 @@ namespace Microsoft.Boogie {
   public class StateCmd : Cmd {
     [ContractInvariantMethod]
     void ObjectInvariant() {
-      Contract.Invariant(Locals != null);
-      Contract.Invariant(Cmds != null);
+      Contract.Invariant(this._locals != null);
+      Contract.Invariant(this._cmds != null);
+    }
+
+    private List<Variable> _locals;
+
+    public /*readonly, except for the StandardVisitor*/ List<Variable>/*!*/ Locals {
+      get {
+        Contract.Ensures(Contract.Result<List<Variable>>() != null);
+        return this._locals;
+      }
+      internal set {
+        Contract.Requires(value != null);
+        this._locals = value;
+      }
     }
 
-    public /*readonly, except for the StandardVisitor*/ List<Variable>/*!*/ Locals;
-    public /*readonly, except for the StandardVisitor*/ List<Cmd>/*!*/ Cmds;
+    private List<Cmd> _cmds;
+
+    public /*readonly, except for the StandardVisitor*/ List<Cmd>/*!*/ Cmds {
+      get {
+        Contract.Ensures(Contract.Result<List<Variable>>() != null);
+        return this._cmds;
+      }
+      internal set {
+        Contract.Requires(value != null);
+        this._cmds = value;
+      }
+    }
 
     public StateCmd(IToken tok, List<Variable>/*!*/ locals, List<Cmd>/*!*/ cmds)
       : base(tok) {
       Contract.Requires(locals != null);
       Contract.Requires(cmds != null);
       Contract.Requires(tok != null);
-      this.Locals = locals;
-      this.Cmds = cmds;
+      this._locals = locals;
+      this._cmds = cmds;
     }
 
     public override void Resolve(ResolutionContext rc) {
-- 
cgit v1.2.3