Made invariant of class 'HavocCmd' 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/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index 3f675317..be712ffb 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -3008,18 +3008,31 @@ namespace Microsoft.Boogie {
   }

 

   public class HavocCmd : Cmd {

-    public List<IdentifierExpr>/*!*/ Vars;

+    private List<IdentifierExpr>/*!*/ _vars;

+

+    public List<IdentifierExpr>/*!*/ Vars {

+      get {

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

+        return this._vars;

+      }

+      set {

+        Contract.Requires(value != null);

+        this._vars = value;

+      }

+    }

+

     [ContractInvariantMethod]

     void ObjectInvariant() {

-      Contract.Invariant(Vars != null);

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

     }

 

     public HavocCmd(IToken/*!*/ tok, List<IdentifierExpr>/*!*/ vars)

       : base(tok) {

       Contract.Requires(tok != null);

       Contract.Requires(vars != null);

-      Vars = vars;

+      this._vars = vars;

     }

+

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

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

       stream.Write(this, level, "havoc ");