Merge

author: Ally Donaldson <unknown> 2015-01-13 21:00:43 +0000
committer: Ally Donaldson <unknown> 2015-01-13 21:00:43 +0000
commit: d16fd70f1678b0e3f1683ba0c8b93f21d3d88cc4 (patch)
tree: 7965c0c9c80e09d988359c9513dd9d9705f55038 /Source/Core
parent: 7b1b91e940fd8ec7ac60074c843eb08f5715bc91 (diff)
parent: a1d2ad91bb39f7789015dbe9bd7bd7cc610a53e1 (diff)
9 files changed, 588 insertions, 154 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 2fd442d4..817897b7 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -88,6 +88,7 @@ namespace Microsoft.Boogie {
   using System.Collections;
   using System.Diagnostics;
   using System.Collections.Generic;
+  using System.Collections.ObjectModel;
   using System.Diagnostics.Contracts;
   using Microsoft.Boogie.AbstractInterpretation;
   using Microsoft.Boogie.GraphUtil;
@@ -308,10 +309,18 @@ namespace Microsoft.Boogie {
     }
   }
 
-  // TODO: Ideally, this would use generics.
-  public interface IPotentialErrorNode {
-    object ErrorData {
+  public interface IPotentialErrorNode<out TGet>
+  {
+    TGet ErrorData
+    {
       get;
+    }
+  }
+
+  public interface IPotentialErrorNode<out TGet, in TSet> : IPotentialErrorNode<TGet>
+  {
+    new TSet ErrorData
+    {
       set;
     }
   }
@@ -321,7 +330,7 @@ namespace Microsoft.Boogie {
     [ContractInvariantMethod]
     void ObjectInvariant() {
       Contract.Invariant(cce.NonNullElements(this.topLevelDeclarations));
-      Contract.Invariant(globalVariablesCache == null || cce.NonNullElements(globalVariablesCache));
+      Contract.Invariant(cce.NonNullElements(this.globalVariablesCache, true));
     }
     
     public Program()
@@ -673,18 +682,17 @@ namespace Microsoft.Boogie {
       }
     }
 
-    private List<GlobalVariable/*!*/> globalVariablesCache = null;
-    public IEnumerable<GlobalVariable/*!*/>/*!*/ GlobalVariables
+    private IEnumerable<GlobalVariable/*!*/> globalVariablesCache = null;
+    public List<GlobalVariable/*!*/>/*!*/ GlobalVariables
     {
       get
       {
-        Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<GlobalVariable>>()));
+        Contract.Ensures(cce.NonNullElements(Contract.Result<List<GlobalVariable>>()));
 
         if (globalVariablesCache == null)
-        {
-          globalVariablesCache = TopLevelDeclarations.OfType<GlobalVariable>().ToList();
-        }
-        return globalVariablesCache;
+          globalVariablesCache = TopLevelDeclarations.OfType<GlobalVariable>();
+
+        return new List<GlobalVariable>(globalVariablesCache);
       }
     }
 
@@ -1420,7 +1428,7 @@ namespace Microsoft.Boogie {
       QKeyValue kv;
       for (kv = this.Attributes; kv != null; kv = kv.Next) {
         if (kv.Key == name) {
-          kv.Params.AddRange(vals);
+          kv.AddParams(vals);
           break;
         }
       }
@@ -1953,13 +1961,13 @@ namespace Microsoft.Boogie {
     // the <:-parents of the value of this constant. If the field is
     // null, no information about the parents is provided, which means
     // that the parental situation is unconstrained.
-    public readonly List<ConstantParent/*!*/> Parents;
+    public readonly ReadOnlyCollection<ConstantParent/*!*/> Parents;
+
     [ContractInvariantMethod]
     void ObjectInvariant() {
       Contract.Invariant(cce.NonNullElements(Parents, true));
     }
 
-
     // if true, it is assumed that the immediate <:-children of the
     // value of this constant are completely specified
     public readonly bool ChildrenComplete;
@@ -1986,16 +1994,16 @@ namespace Microsoft.Boogie {
     }
     public Constant(IToken/*!*/ tok, TypedIdent/*!*/ typedIdent,
                     bool unique,
-                    List<ConstantParent/*!*/> parents, bool childrenComplete,
+                    IEnumerable<ConstantParent/*!*/> parents, bool childrenComplete,
                     QKeyValue kv)
       : base(tok, typedIdent, kv) {
       Contract.Requires(tok != null);
       Contract.Requires(typedIdent != null);
-      Contract.Requires(parents == null || cce.NonNullElements(parents));
+      Contract.Requires(cce.NonNullElements(parents, true));
       Contract.Requires(typedIdent.Name != null && typedIdent.Name.Length > 0);
       Contract.Requires(typedIdent.WhereExpr == null);
       this.Unique = unique;
-      this.Parents = parents;
+      this.Parents = parents == null ? null : new ReadOnlyCollection<ConstantParent>(parents.ToList());
       this.ChildrenComplete = childrenComplete;
     }
     public override bool IsMutable {
@@ -2230,13 +2238,37 @@ namespace Microsoft.Boogie {
 
   public abstract class DeclWithFormals : NamedDeclaration {
     public List<TypeVariable>/*!*/ TypeParameters;
-    public /*readonly--except in StandardVisitor*/ List<Variable>/*!*/ InParams, OutParams;
+
+    private /*readonly--except in StandardVisitor*/ List<Variable>/*!*/ inParams, outParams;
+
+    public List<Variable>/*!*/ InParams {
+      get {
+        Contract.Ensures(Contract.Result<List<Variable>>() != null);
+        return this.inParams;
+      }
+      set {
+        Contract.Requires(value != null);
+        this.inParams = value;
+      }
+    }
+
+    public List<Variable>/*!*/ OutParams
+    {
+      get {
+        Contract.Ensures(Contract.Result<List<Variable>>() != null);
+        return this.outParams;
+      }
+      set {
+        Contract.Requires(value != null);
+        this.outParams = value;
+      }
+    }
 
     [ContractInvariantMethod]
     void ObjectInvariant() {
       Contract.Invariant(TypeParameters != null);
-      Contract.Invariant(InParams != null);
-      Contract.Invariant(OutParams != null);
+      Contract.Invariant(this.inParams != null);
+      Contract.Invariant(this.outParams != null);
     }
 
     public DeclWithFormals(IToken tok, string name, List<TypeVariable> typeParams,
@@ -2248,16 +2280,16 @@ namespace Microsoft.Boogie {
       Contract.Requires(name != null);
       Contract.Requires(tok != null);
       this.TypeParameters = typeParams;
-      this.InParams = inParams;
-      this.OutParams = outParams;
+      this.inParams = inParams;
+      this.outParams = outParams;
     }
 
     protected DeclWithFormals(DeclWithFormals that)
       : base(that.tok, cce.NonNull(that.Name)) {
       Contract.Requires(that != null);
       this.TypeParameters = that.TypeParameters;
-      this.InParams = that.InParams;
-      this.OutParams = that.OutParams;
+      this.inParams = cce.NonNull(that.InParams);
+      this.outParams = cce.NonNull(that.OutParams);
     }
 
     public byte[] MD5Checksum_;
@@ -2752,7 +2784,7 @@ namespace Microsoft.Boogie {
       : base(tok, name, args, result) { }
   }
 
-  public class Requires : Absy, IPotentialErrorNode {
+  public class Requires : Absy, IPotentialErrorNode<string, string> {
     public readonly bool Free;
     
     private Expr/*!*/ _condition;
@@ -2772,13 +2804,12 @@ namespace Microsoft.Boogie {
     [ContractInvariantMethod]
     void ObjectInvariant() {
       Contract.Invariant(this._condition != null);
-      Contract.Invariant(errorData == null || errorData is string);
     }
 
 
     // TODO: convert to use generics
-    private object errorData;
-    public object ErrorData {
+    private string errorData;
+    public string ErrorData {
       get {
         return errorData;
       }
@@ -2865,7 +2896,7 @@ namespace Microsoft.Boogie {
     }
   }
 
-  public class Ensures : Absy, IPotentialErrorNode {
+  public class Ensures : Absy, IPotentialErrorNode<string, string> {
     public readonly bool Free;
 
     private Expr/*!*/ _condition;
@@ -2884,14 +2915,13 @@ namespace Microsoft.Boogie {
     [ContractInvariantMethod]
     void ObjectInvariant() {
       Contract.Invariant(this._condition != null); 
-      Contract.Invariant(errorData == null || errorData is string);
     }
 
     public string Comment;
 
     // TODO: convert to use generics
-    private object errorData;
-    public object ErrorData {
+    private string errorData;
+    public string ErrorData {
       get {
         return errorData;
       }
@@ -4211,24 +4241,42 @@ namespace Microsoft.Boogie {
     }
   }
   public class AtomicRE : RE {
-    public Block/*!*/ b;
+    private Block/*!*/ _b;
+
+    public Block b
+    {
+      get
+      {
+        Contract.Ensures(Contract.Result<Block>() != null);
+        return this._b;
+      }
+      set
+      {
+        Contract.Requires(value != null);
+        this._b = value;
+      }
+    }
+
     [ContractInvariantMethod]
     void ObjectInvariant() {
-      Contract.Invariant(b != null);
+      Contract.Invariant(this._b != null);
     }
 
     public AtomicRE(Block block) {
       Contract.Requires(block != null);
-      b = block;
+      this._b = block;
     }
+
     public override void Resolve(ResolutionContext rc) {
       //Contract.Requires(rc != null);
       b.Resolve(rc);
     }
+
     public override void Typecheck(TypecheckingContext tc) {
       //Contract.Requires(tc != null);
       b.Typecheck(tc);
     }
+
     public override void Emit(TokenTextWriter stream, int level) {
       //Contract.Requires(stream != null);
       b.Emit(stream, level);
diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index 900d1c7a..d14250c1 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -1,4 +1,4 @@
-//-----------------------------------------------------------------------------
+//-----------------------------------------------------------------------------
 //
 // Copyright (C) Microsoft Corporation.  All Rights Reserved.
 //
@@ -24,19 +24,77 @@ namespace Microsoft.Boogie {
     [ContractInvariantMethod]
     void ObjectInvariant() {
       Contract.Invariant(tok != null);
-      Contract.Invariant(Anonymous || LabelName != null);
-      Contract.Invariant(ec == null || tc == null);
-      Contract.Invariant(simpleCmds != null);
+      Contract.Invariant(Anonymous || this.labelName != null);
+      Contract.Invariant(this._ec == null || this._tc == null);
+      Contract.Invariant(this._simpleCmds != null);
     }
 
     public readonly IToken/*!*/ tok;
-    public string LabelName;
+
     public readonly bool Anonymous;
 
+    private string labelName;
+
+    public string LabelName
+    {
+      get
+      {
+        Contract.Ensures(Anonymous || Contract.Result<string>() != null);
+        return this.labelName;
+      }
+      set
+      {
+        Contract.Requires(Anonymous || value != null);
+        this.labelName = value;
+      }
+    }
+
     [Rep]
-    public List<Cmd>/*!*/ simpleCmds;
-    public StructuredCmd ec;
-    public TransferCmd tc;
+    private List<Cmd>/*!*/ _simpleCmds;
+
+    public List<Cmd>/*!*/ simpleCmds
+    {
+      get
+      {
+        Contract.Ensures(Contract.Result<List<Cmd>>() != null);
+        return this._simpleCmds;
+      }
+      set
+      {
+        Contract.Requires(value != null);
+        this._simpleCmds = value;
+      }
+    }
+
+    private StructuredCmd _ec;
+
+    public StructuredCmd ec
+    {
+      get
+      {
+        return this._ec;
+      }
+      set
+      {
+        Contract.Requires(value == null || this.tc == null);
+        this._ec = value;
+      }
+    }
+
+    private TransferCmd _tc;
+
+    public TransferCmd tc
+    {
+      get
+      {
+        return this._tc;
+      }
+      set
+      {
+        Contract.Requires(value == null || this.ec == null);
+        this._tc = value;
+      }
+    }
 
     public BigBlock successorBigBlock;  // semantic successor (may be a back-edge, pointing back to enclosing while statement); null if successor is end of procedure body (or if field has not yet been initialized)
 
@@ -45,11 +103,11 @@ namespace Microsoft.Boogie {
       Contract.Requires(tok != null);
       Contract.Requires(ec == null || tc == null);
       this.tok = tok;
-      this.LabelName = labelName;
       this.Anonymous = labelName == null;
-      this.simpleCmds = simpleCmds;
-      this.ec = ec;
-      this.tc = tc;
+      this.labelName = labelName;
+      this._simpleCmds = simpleCmds;
+      this._ec = ec;
+      this._tc = tc;
     }
 
     public void Emit(TokenTextWriter stream, int level) {
@@ -74,25 +132,51 @@ namespace Microsoft.Boogie {
 
   public class StmtList {
     [Rep]
-    public readonly List<BigBlock/*!*/>/*!*/ BigBlocks;
+    private readonly List<BigBlock/*!*/>/*!*/ bigBlocks;
+
+    public IList<BigBlock/*!*/>/*!*/ BigBlocks
+    {
+      get
+      {
+        Contract.Ensures(Contract.Result<IList<BigBlock>>() != null);
+        Contract.Ensures(Contract.Result<IList<BigBlock>>().IsReadOnly);
+        return this.bigBlocks.AsReadOnly();
+      }
+    }
+
     public List<Cmd> PrefixCommands;
     public readonly IToken/*!*/ EndCurly;
     public StmtList ParentContext;
     public BigBlock ParentBigBlock;
-    public HashSet<string/*!*/>/*!*/ Labels = new HashSet<string/*!*/>();
+
+    private readonly HashSet<string/*!*/>/*!*/ labels = new HashSet<string/*!*/>();
+
+    public void AddLabel(string label)
+    {
+      labels.Add(label);
+    }
+
+    public IEnumerable<string/*!*/>/*!*/ Labels
+    {
+      get
+      {
+        Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<string/*!*/>/*!*/>()));
+        return this.labels.AsEnumerable<string>();
+      }
+    }
+
     [ContractInvariantMethod]
     void ObjectInvariant() {
       Contract.Invariant(EndCurly != null);
-      Contract.Invariant(cce.NonNullElements(BigBlocks));
-      Contract.Invariant(cce.NonNullElements(Labels));
+      Contract.Invariant(cce.NonNullElements(this.bigBlocks));
+      Contract.Invariant(cce.NonNullElements(this.labels));
     }
 
-
-    public StmtList([Captured] List<BigBlock/*!*/>/*!*/ bigblocks, IToken endCurly) {
+    public StmtList(IList<BigBlock/*!*/>/*!*/ bigblocks, IToken endCurly) {
       Contract.Requires(endCurly != null);
       Contract.Requires(cce.NonNullElements(bigblocks));
       Contract.Requires(bigblocks.Count > 0);
-      this.BigBlocks = bigblocks;
+      this.bigBlocks = new List<BigBlock>(bigblocks);
       this.EndCurly = endCurly;
     }
 
@@ -327,7 +411,7 @@ namespace Microsoft.Boogie {
               prefix += "0";
             }
           }
-          stmtList.Labels.Add(b.LabelName);
+          stmtList.AddLabel(b.LabelName);
         }
       }
 
@@ -647,15 +731,30 @@ namespace Microsoft.Boogie {
 
   [ContractClass(typeof(StructuredCmdContracts))]
   public abstract class StructuredCmd {
-    public IToken/*!*/ tok;
+    private IToken/*!*/ _tok;
+
+    public IToken/*!*/ tok
+    {
+      get
+      {
+        Contract.Ensures(Contract.Result<IToken>() != null);
+        return this._tok;
+      }
+      set
+      {
+        Contract.Requires(value != null);
+        this._tok = value;
+      }
+    }
+
     [ContractInvariantMethod]
     void ObjectInvariant() {
-      Contract.Invariant(tok != null);
+      Contract.Invariant(this._tok != null);
     }
 
     public StructuredCmd(IToken tok) {
       Contract.Requires(tok != null);
-      this.tok = tok;
+      this._tok = tok;
     }
 
     public abstract void Emit(TokenTextWriter/*!*/ stream, int level);
@@ -673,16 +772,58 @@ namespace Microsoft.Boogie {
 
   public class IfCmd : StructuredCmd {
     public Expr Guard;
-    public StmtList/*!*/ thn;
-    public IfCmd elseIf;
-    public StmtList elseBlock;
-    [ContractInvariantMethod]
-    void ObjectInvariant() {
-      Contract.Invariant(thn != null);
-      Contract.Invariant(elseIf == null || elseBlock == null);
+
+    private StmtList/*!*/ _thn;
+    
+    public StmtList/*!*/ thn
+    {
+      get
+      {
+        Contract.Ensures(Contract.Result<StmtList>() != null);
+        return this._thn;
+      }
+      set
+      {
+        Contract.Requires(value != null);
+        this._thn = value;
+      }
     }
 
+    private IfCmd _elseIf;
 
+    public IfCmd elseIf
+    {
+      get
+      {
+        return this._elseIf;
+      }
+      set
+      {
+        Contract.Requires(value == null || this.elseBlock == null);
+        this._elseIf = value;
+      }
+    }
+
+    private StmtList _elseBlock;
+
+    public StmtList elseBlock
+    {
+      get
+      {
+        return this._elseBlock;
+      }
+      set
+      {
+        Contract.Requires(value == null || this.elseIf == null);
+        this._elseBlock = value;
+      }
+    }
+
+    [ContractInvariantMethod]
+    void ObjectInvariant() {
+      Contract.Invariant(this._thn != null);
+      Contract.Invariant(this._elseIf == null || this._elseBlock == null);
+    }
 
     public IfCmd(IToken/*!*/ tok, Expr guard, StmtList/*!*/ thn, IfCmd elseIf, StmtList elseBlock)
       : base(tok) {
@@ -690,9 +831,9 @@ namespace Microsoft.Boogie {
       Contract.Requires(thn != null);
       Contract.Requires(elseIf == null || elseBlock == null);
       this.Guard = guard;
-      this.thn = thn;
-      this.elseIf = elseIf;
-      this.elseBlock = elseBlock;
+      this._thn = thn;
+      this._elseIf = elseIf;
+      this._elseBlock = elseBlock;
     }
 
     public override void Emit(TokenTextWriter stream, int level) {
@@ -796,10 +937,40 @@ namespace Microsoft.Boogie {
   //---------------------------------------------------------------------
   // Block
   public sealed class Block : Absy {
-    public string/*!*/ Label;  // Note, Label is mostly readonly, but it can change to the name of a nearby block during block coalescing and empty-block removal
+    private string/*!*/ label; // Note, Label is mostly readonly, but it can change to the name of a nearby block during block coalescing and empty-block removal
+
+    public string/*!*/ Label
+    {
+      get
+      {
+        Contract.Ensures(Contract.Result<string>() != null);
+        return this.label;
+      }
+      set
+      {
+        Contract.Requires(value != null);
+        this.label = value;
+      }
+    }
+
     [Rep]
     [ElementsPeer]
-    public List<Cmd>/*!*/ Cmds;
+    public List<Cmd>/*!*/ cmds;
+
+    public List<Cmd>/*!*/ Cmds
+    {
+      get
+      {
+        Contract.Ensures(Contract.Result<List<Cmd>>() != null);
+        return this.cmds;
+      }
+      set
+      {
+        Contract.Requires(value != null);
+        this.cmds = value;
+      }
+    }
+
     [Rep]  //PM: needed to verify Traverse.Visit
     public TransferCmd TransferCmd; // maybe null only because we allow deferred initialization (necessary for cyclic structures)
 
@@ -826,12 +997,33 @@ namespace Microsoft.Boogie {
     // This field is used during passification to null-out entries in block2Incartion hashtable early
     public int succCount;
 
-    public HashSet<Variable/*!*/> liveVarsBefore;
+    private HashSet<Variable/*!*/> _liveVarsBefore;
+
+    public IEnumerable<Variable/*!*/> liveVarsBefore
+    {
+      get
+      {
+        Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<Variable/*!*/>>(), true));
+        if (this._liveVarsBefore == null)
+          return null;
+        else
+          return this._liveVarsBefore.AsEnumerable<Variable>();
+      }
+      set
+      {
+        Contract.Requires(cce.NonNullElements(value, true));
+        if (value == null)
+          this._liveVarsBefore = null;
+        else
+          this._liveVarsBefore = new HashSet<Variable>(value);
+      }
+    }
+
     [ContractInvariantMethod]
     void ObjectInvariant() {
-      Contract.Invariant(Label != null);
-      Contract.Invariant(Cmds != null);
-      Contract.Invariant(cce.NonNullElements(liveVarsBefore, true));
+      Contract.Invariant(this.label != null);
+      Contract.Invariant(this.cmds != null);
+      Contract.Invariant(cce.NonNullElements(this._liveVarsBefore, true));
     }
 
     public bool IsLive(Variable v) {
@@ -851,11 +1043,11 @@ namespace Microsoft.Boogie {
       Contract.Requires(label != null);
       Contract.Requires(cmds != null);
       Contract.Requires(tok != null);
-      this.Label = label;
-      this.Cmds = cmds;
+      this.label = label;
+      this.cmds = cmds;
       this.TransferCmd = transferCmd;
       this.Predecessors = new List<Block>();
-      this.liveVarsBefore = null;
+      this._liveVarsBefore = null;
       this.TraversingStatus = VisitState.ToVisit;
       this.iterations = 0;
     }
@@ -1289,8 +1481,8 @@ namespace Microsoft.Boogie {
       Contract.Requires(lhs != null);
       Contract.Ensures(this.Lhss[index] == lhs);
       this._lhss[index] = lhs;
-    }
-
+    }
+
     private List<Expr/*!*/>/*!*/ _rhss;
 
     public IList<Expr/*!*/>/*!*/ Rhss {
@@ -1997,7 +2189,7 @@ namespace Microsoft.Boogie {
     }
   }
 
-  public class ParCallCmd : CallCommonality, IPotentialErrorNode
+  public class ParCallCmd : CallCommonality, IPotentialErrorNode<object, object>
   {
       public List<CallCmd> CallCmds;
       public ParCallCmd(IToken tok, List<CallCmd> callCmds)
@@ -2086,7 +2278,8 @@ namespace Microsoft.Boogie {
       }
   }
 
-  public class CallCmd : CallCommonality, IPotentialErrorNode {
+  public class CallCmd : CallCommonality, IPotentialErrorNode<object, object>
+  {
     public string/*!*/ callee { get; set; }
     public Procedure Proc;
     public LocalVariable AssignedAssumptionVariable;
@@ -2578,7 +2771,7 @@ namespace Microsoft.Boogie {
         if (QKeyValue.FindBoolAttribute(e.Attributes, "candidate"))
         {
             assume.Attributes = new QKeyValue(Token.NoToken, "candidate", new List<object>(), assume.Attributes);
-            assume.Attributes.Params.Add(this.callee);
+            assume.Attributes.AddParam(this.callee);
         }
         #endregion
         newBlockBody.Add(assume);
@@ -2720,38 +2913,82 @@ namespace Microsoft.Boogie {
   }
 
   public class ListOfMiningStrategies : MiningStrategy {
-    public List<MiningStrategy>/*!*/ msList;
+
+    private List<MiningStrategy>/*!*/ _msList;
+
+    public List<MiningStrategy>/*!*/ msList
+    {
+      get
+      {
+        Contract.Ensures(Contract.Result<List<MiningStrategy>>() != null);
+        return this._msList;
+      }
+      set
+      {
+        Contract.Requires(value != null);
+        this._msList = value;
+      }
+    }
+
     [ContractInvariantMethod]
     void ObjectInvariant() {
-      Contract.Invariant(msList != null);
+      Contract.Invariant(this._msList != null);
     }
 
-
     public ListOfMiningStrategies(List<MiningStrategy> l) {
       Contract.Requires(l != null);
-      this.msList = l;
+      this._msList = l;
     }
   }
 
   public class EEDTemplate : MiningStrategy {
-    public string/*!*/ reason;
-    public List<Expr/*!*/>/*!*/ exprList;
+    private string/*!*/ _reason;
+    public string/*!*/ reason
+    {
+      get
+      {
+        Contract.Ensures(Contract.Result<string>() != null);
+        return this._reason;
+      }
+      set
+      {
+        Contract.Requires(value != null);
+        this._reason = value;
+      }
+    }
+    
+    private List<Expr/*!*/>/*!*/ exprList;
+    public IEnumerable<Expr> Expressions
+    {
+      get
+      {
+        Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<Expr>>()));
+        return this.exprList.AsReadOnly();
+      }
+      set
+      {
+        Contract.Requires(cce.NonNullElements(value));
+        this.exprList = new List<Expr>(value);
+      }
+    }
+
+
     [ContractInvariantMethod]
     void ObjectInvariant() {
-      Contract.Invariant(reason != null);
-      Contract.Invariant(cce.NonNullElements(exprList));
+      Contract.Invariant(this._reason != null);
+      Contract.Invariant(cce.NonNullElements(this.exprList));
     }
 
-
     public EEDTemplate(string reason, List<Expr/*!*/>/*!*/ exprList) {
       Contract.Requires(reason != null);
       Contract.Requires(cce.NonNullElements(exprList));
-      this.reason = reason;
+      this._reason = reason;
       this.exprList = exprList;
     }
   }
 
-  public class AssertCmd : PredicateCmd, IPotentialErrorNode {
+  public class AssertCmd : PredicateCmd, IPotentialErrorNode<object, object>
+  {
     public Expr OrigExpr;
     public Dictionary<Variable, Expr> IncarnationMap;
 
diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index 8918115b..e2113ab5 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -2530,16 +2530,30 @@ namespace Microsoft.Boogie {
 
   public class IfThenElse : IAppliable {
 
-    public IToken/*!*/ tok;
+    private IToken/*!*/ _tok;
+
+    public IToken/*!*/ tok
+    {
+      get
+      {
+        Contract.Ensures(Contract.Result<IToken>() != null);
+        return this._tok;
+      }
+      set
+      {
+        Contract.Requires(value != null);
+        this._tok = value;
+      }
+    }
+    
     [ContractInvariantMethod]
     void ObjectInvariant() {
-      Contract.Invariant(tok != null);
+      Contract.Invariant(this._tok != null);
     }
 
-
     public IfThenElse(IToken tok) {
       Contract.Requires(tok != null);
-      this.tok = tok;
+      this._tok = tok;
     }
 
     public string/*!*/ FunctionName {
@@ -2566,7 +2580,7 @@ namespace Microsoft.Boogie {
     public void Emit(List<Expr> args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {
       //Contract.Requires(stream != null);
       //Contract.Requires(args != null);
-      stream.SetToken(ref this.tok);
+      stream.SetToken(this);
       Contract.Assert(args.Count == 3);
       stream.push();
       stream.Write("(if ");     
diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs
index 9cbadc80..c5b7b317 100644
--- a/Source/Core/AbsyQuant.cs
+++ b/Source/Core/AbsyQuant.cs
@@ -1,4 +1,4 @@
-//-----------------------------------------------------------------------------
+//-----------------------------------------------------------------------------
 //
 // Copyright (C) Microsoft Corporation.  All Rights Reserved.
 //
@@ -249,22 +249,49 @@ namespace Microsoft.Boogie {
 
   public class QKeyValue : Absy {
     public readonly string/*!*/ Key;
-    public readonly List<object/*!*/>/*!*/ Params;  // each element is either a string or an Expr
+    private readonly List<object/*!*/>/*!*/ _params;  // each element is either a string or an Expr
+
+    public void AddParam(object p)
+    {
+      Contract.Requires(p != null);
+      this._params.Add(p);
+    }
+
+    public void AddParams(IEnumerable<object> ps)
+    {
+      Contract.Requires(cce.NonNullElements(ps));
+      this._params.AddRange(ps);
+    }
+
+    public void ClearParams()
+    {
+      this._params.Clear();
+    }
+
+    public IList<object> Params
+    {
+      get
+      {
+        Contract.Ensures(cce.NonNullElements(Contract.Result<IList<object>>()));
+        Contract.Ensures(Contract.Result<IList<object>>().IsReadOnly);
+        return this._params.AsReadOnly();
+      }
+    }
+
     public QKeyValue Next;
     [ContractInvariantMethod]
     void ObjectInvariant() {
       Contract.Invariant(Key != null);
-      Contract.Invariant(cce.NonNullElements(Params));
+      Contract.Invariant(cce.NonNullElements(this._params));
     }
 
-
-    public QKeyValue(IToken tok, string key, [Captured] List<object/*!*/>/*!*/ parameters, QKeyValue next)
+    public QKeyValue(IToken tok, string key, IList<object/*!*/>/*!*/ parameters, QKeyValue next)
       : base(tok) {
       Contract.Requires(key != null);
       Contract.Requires(tok != null);
       Contract.Requires(cce.NonNullElements(parameters));
       Key = key;
-      Params = parameters;
+      this._params = new List<object>(parameters);
       Next = next;
     }
 
@@ -389,32 +416,43 @@ namespace Microsoft.Boogie {
   public class Trigger : Absy {
     public readonly bool Pos;
     [Rep]
-    public List<Expr>/*!*/ Tr;
+    private List<Expr>/*!*/ tr;
+
+    public IList<Expr>/*!*/ Tr
+    {
+      get
+      {
+        Contract.Ensures(Contract.Result<IList<Expr>>() != null);
+        Contract.Ensures(Contract.Result<IList<Expr>>().Count >= 1);
+        Contract.Ensures(this.Pos || Contract.Result<IList<Expr>>().Count == 1);
+        return this.tr.AsReadOnly();
+      }
+      set
+      {
+        Contract.Requires(value != null);
+        Contract.Requires(value.Count >= 1);
+        Contract.Requires(this.Pos || value.Count == 1);
+        this.tr = new List<Expr>(value);
+      }
+    }
+
     [ContractInvariantMethod]
     void ObjectInvariant() {
-      Contract.Invariant(Tr != null);
-      Contract.Invariant(1 <= Tr.Count);
-      Contract.Invariant(Pos || Tr.Count == 1);
+      Contract.Invariant(this.tr != null);
+      Contract.Invariant(this.tr.Count >= 1);
+      Contract.Invariant(Pos || this.tr.Count == 1);
     }
 
     public Trigger Next;
 
-    public Trigger(IToken tok, bool pos, List<Expr> tr)
-      : this(tok, pos, tr, null) {
-      Contract.Requires(tr != null);
-      Contract.Requires(tok != null);
-      Contract.Requires(1 <= tr.Count);
-      Contract.Requires(pos || tr.Count == 1);
-    }
-
-    public Trigger(IToken/*!*/ tok, bool pos, List<Expr>/*!*/ tr, Trigger next)
+    public Trigger(IToken/*!*/ tok, bool pos, IEnumerable<Expr>/*!*/ tr, Trigger next = null)
       : base(tok) {
       Contract.Requires(tok != null);
       Contract.Requires(tr != null);
-      Contract.Requires(1 <= tr.Count);
-      Contract.Requires(pos || tr.Count == 1);
+      Contract.Requires(tr.Count() >= 1);
+      Contract.Requires(pos || tr.Count() == 1);
       this.Pos = pos;
-      this.Tr = tr;
+      this.Tr = new List<Expr>(tr);
       this.Next = next;
     }
 
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 6bed4e75..072e0323 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -1,4 +1,4 @@
-//-----------------------------------------------------------------------------
+//-----------------------------------------------------------------------------
 //
 // Copyright (C) Microsoft Corporation.  All Rights Reserved.
 //
@@ -218,6 +218,7 @@ namespace Microsoft.Boogie {
       /// </summary>
       public bool GetNumericArgument(ref int arg, int limit) {
         Contract.Requires(this.i < args.Length);
+        Contract.Ensures(Math.Min(arg, 0) <= Contract.ValueAtReturn(out arg) && Contract.ValueAtReturn(out arg) < limit);
         //modifies nextIndex, encounteredErrors, Console.Error.*;
         int a = arg;
         if (!GetNumericArgument(ref a)) {
@@ -236,6 +237,7 @@ namespace Microsoft.Boogie {
       /// Otherwise, emit an error message, leave "arg" unchanged, and return "false".
       /// </summary>
       public bool GetNumericArgument(ref double arg) {
+        Contract.Ensures(Contract.ValueAtReturn(out arg) >= 0);
         //modifies nextIndex, encounteredErrors, Console.Error.*;
         if (this.ConfirmArgumentCount(1)) {
           try {
@@ -508,8 +510,8 @@ namespace Microsoft.Boogie {
       Contract.Invariant((0 <= PrintErrorModel && PrintErrorModel <= 2) || PrintErrorModel == 4);
       Contract.Invariant(0 <= EnhancedErrorMessages && EnhancedErrorMessages < 2);
       Contract.Invariant(0 <= StepsBeforeWidening && StepsBeforeWidening <= 9);
-      Contract.Invariant(-1 <= BracketIdsInVC && BracketIdsInVC < 2);
-      Contract.Invariant(cce.NonNullElements(ProverOptions));
+      Contract.Invariant(-1 <= this.bracketIdsInVC && this.bracketIdsInVC <= 1);
+      Contract.Invariant(cce.NonNullElements(this.proverOptions));
     }
 
     public int LoopUnrollCount = -1;  // -1 means don't unroll loops
@@ -543,7 +545,21 @@ namespace Microsoft.Boogie {
     public bool ExpandLambdas = true; // not useful from command line, only to be set to false programatically
     public bool DoModSetAnalysis = false;
     public bool UseAbstractInterpretation = true;          // true iff the user want to use abstract interpretation
-    public int  /*0..9*/StepsBeforeWidening = 0;           // The number of steps that must be done before applying a widen operator
+    private int  /*0..9*/stepsBeforeWidening = 0;           // The number of steps that must be done before applying a widen operator
+
+    public int StepsBeforeWidening
+    {
+      get
+      {
+        Contract.Ensures(0 <= Contract.Result<int>() && Contract.Result<int>() <= 9);
+        return this.stepsBeforeWidening;
+      }
+      set
+      {
+        Contract.Requires(0 <= value && value <= 9);
+        this.stepsBeforeWidening = value;
+      }
+    }
 
     public string OwickiGriesDesugaredOutputFile = null;
     public bool TrustAtomicityTypes = false;
@@ -573,9 +589,42 @@ namespace Microsoft.Boogie {
     public ProverFactory TheProverFactory;
     public string ProverName;
     [Peer]
-    public List<string/*!*/>/*!*/ ProverOptions = new List<string/*!*/>();
+    private List<string> proverOptions = new List<string>();
+
+    public IEnumerable<string> ProverOptions
+    {
+      get
+      {
+        Contract.Ensures(Contract.Result<IEnumerable<string>>() != null);
+        foreach (string s in this.proverOptions)
+          yield return s;
+      }
+    }
+
+    public void AddProverOption(string option)
+    {
+      Contract.Requires(option != null);
+      this.proverOptions.Add(option);
+    }
+
+    public void RemoveAllProverOptions(Predicate<string> match)
+    {
+      this.proverOptions.RemoveAll(match);
+    }
+
+    private int bracketIdsInVC = -1;  // -1 - not specified, 0 - no, 1 - yes
+
+    public int BracketIdsInVC {
+      get {
+        Contract.Ensures(-1 <= Contract.Result<int>() && Contract.Result<int>() <= 1);
+        return this.bracketIdsInVC;
+      }
+      set {
+        Contract.Requires(-1 <= value && value <= 1);
+        this.bracketIdsInVC = value;
+      }
+    }
 
-    public int BracketIdsInVC = -1;  // -1 - not specified, 0 - no, 1 - yes
     public bool CausalImplies = false;
 
     public int SimplifyProverMatchDepth = -1;  // -1 means not specified
@@ -609,12 +658,29 @@ namespace Microsoft.Boogie {
     }
     [ContractInvariantMethod]
     void ObjectInvariant4() {
-      Contract.Invariant(cce.NonNullElements(Z3Options));
+      Contract.Invariant(cce.NonNullElements(this.z3Options));
       Contract.Invariant(0 <= Z3lets && Z3lets < 4);
     }
 
     [Peer]
-    public List<string/*!*/>/*!*/ Z3Options = new List<string/*!*/>();
+    private List<string> z3Options = new List<string>();
+
+    public IEnumerable<string> Z3Options
+    {
+      get
+      {
+        Contract.Ensures(Contract.Result<IEnumerable<string>>() != null);
+        foreach (string s in z3Options)
+          yield return s;
+      }
+    }
+
+    public void AddZ3Option(string option)
+    {
+      Contract.Requires(option != null);
+      this.z3Options.Add(option);
+    }
+
     public bool Z3types = false;
     public int Z3lets = 3;  // 0 - none, 1 - only LET TERM, 2 - only LET FORMULA, 3 - (default) any
 
@@ -699,10 +765,18 @@ namespace Microsoft.Boogie {
       }
     }
 
-    public List<string/*!*/> ProcsToCheck = null;  // null means "no restriction"
+    public IEnumerable<string/*!*/> ProcsToCheck {
+      get {
+        Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<string/*!*/>>(), true));
+        return this.procsToCheck != null ? this.procsToCheck.AsEnumerable() : null;
+      }
+    }
+
+    private List<string/*!*/> procsToCheck = null;  // null means "no restriction"
+    
     [ContractInvariantMethod]
     void ObjectInvariant5() {
-      Contract.Invariant(cce.NonNullElements(ProcsToCheck, true));
+      Contract.Invariant(cce.NonNullElements(this.procsToCheck, true));
       Contract.Invariant(Ai != null);
     }
 
@@ -776,11 +850,11 @@ namespace Microsoft.Boogie {
           return true;
 
         case "proc":
-          if (ProcsToCheck == null) {
-            ProcsToCheck = new List<string/*!*/>();
+          if (this.procsToCheck == null) {
+            this.procsToCheck = new List<string/*!*/>();
           }
           if (ps.ConfirmArgumentCount(1)) {
-            ProcsToCheck.Add(cce.NonNull(args[ps.i]));
+            this.procsToCheck.Add(cce.NonNull(args[ps.i]));
           }
           return true;
 
@@ -1099,7 +1173,7 @@ namespace Microsoft.Boogie {
         case "p":
         case "proverOpt":
           if (ps.ConfirmArgumentCount(1)) {
-            ProverOptions.Add(cce.NonNull(args[ps.i]));
+            AddProverOption(cce.NonNull(args[ps.i]));
           }
           return true;
 
@@ -1296,7 +1370,7 @@ namespace Microsoft.Boogie {
           return true;
 
         case "vcBrackets":
-          ps.GetNumericArgument(ref BracketIdsInVC, 2);
+          ps.GetNumericArgument(ref bracketIdsInVC, 2);
           return true;
 
         case "proverMemoryLimit": {
@@ -1392,7 +1466,7 @@ namespace Microsoft.Boogie {
 		
         case "z3opt":
           if (ps.ConfirmArgumentCount(1)) {
-            Z3Options.Add(cce.NonNull(args[ps.i]));
+            AddZ3Option(cce.NonNull(args[ps.i]));
           }
           return true;
 
diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs
index ad4dd4df..77086f0f 100644
--- a/Source/Core/DeadVarElim.cs
+++ b/Source/Core/DeadVarElim.cs
@@ -28,13 +28,13 @@ namespace Microsoft.Boogie {
       List<Variable>/*!*/ vars = new List<Variable>();
       foreach (Variable/*!*/ var in impl.LocVars) {
         Contract.Assert(var != null);
-        if (usedVars.Contains(var))
+        if (_usedVars.Contains(var))
           vars.Add(var);
       }
       impl.LocVars = vars;
       //Console.WriteLine("New number of local variables = {0}", impl.LocVars.Length);
       //Console.WriteLine("---------------------------------");
-      usedVars.Clear();
+      _usedVars.Clear();
       return impl;
     }
   }
@@ -274,19 +274,35 @@ namespace Microsoft.Boogie {
   }
 
   public class VariableCollector : ReadOnlyVisitor {
-    public HashSet<Variable/*!*/>/*!*/ usedVars;
-    public HashSet<Variable/*!*/>/*!*/ oldVarsUsed;
+    protected HashSet<Variable/*!*/>/*!*/ _usedVars;
+    public IEnumerable<Variable /*!*/>/*!*/ usedVars
+    {
+      get
+      {
+        return _usedVars.AsEnumerable();
+      }
+    }
+
+    protected HashSet<Variable/*!*/>/*!*/ _oldVarsUsed;
+    public IEnumerable<Variable /*!*/>/*!*/ oldVarsUsed
+    {
+      get
+      {
+        return _oldVarsUsed.AsEnumerable();
+      }
+    }
+
     [ContractInvariantMethod]
     void ObjectInvariant() {
-      Contract.Invariant(cce.NonNullElements(usedVars));
-      Contract.Invariant(cce.NonNullElements(oldVarsUsed));
+      Contract.Invariant(cce.NonNullElements(_usedVars));
+      Contract.Invariant(cce.NonNullElements(_oldVarsUsed));
     }
 
     int insideOldExpr;
 
     public VariableCollector() {
-      usedVars = new System.Collections.Generic.HashSet<Variable/*!*/>();
-      oldVarsUsed = new System.Collections.Generic.HashSet<Variable/*!*/>();
+      _usedVars = new System.Collections.Generic.HashSet<Variable/*!*/>();
+      _oldVarsUsed = new System.Collections.Generic.HashSet<Variable/*!*/>();
       insideOldExpr = 0;
     }
 
@@ -303,9 +319,9 @@ namespace Microsoft.Boogie {
       //Contract.Requires(node != null);
       Contract.Ensures(Contract.Result<Expr>() != null);
       if (node.Decl != null) {
-        usedVars.Add(node.Decl);
+        _usedVars.Add(node.Decl);
         if (insideOldExpr > 0) {
-          oldVarsUsed.Add(node.Decl);
+          _oldVarsUsed.Add(node.Decl);
         }
       }
       return node;
diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs
index 98ea4df3..f7538b53 100644
--- a/Source/Core/StandardVisitor.cs
+++ b/Source/Core/StandardVisitor.cs
@@ -1,4 +1,4 @@
-//-----------------------------------------------------------------------------
+//-----------------------------------------------------------------------------
 //
 // Copyright (C) Microsoft Corporation.  All Rights Reserved.
 //
@@ -438,12 +438,13 @@ namespace Microsoft.Boogie {
     public virtual QKeyValue VisitQKeyValue(QKeyValue node) {
       Contract.Requires(node != null);
       Contract.Ensures(Contract.Result<QKeyValue>() != null);
+      var newParams = new List<object>();
       for (int i = 0, n = node.Params.Count; i < n; i++) {
         var e = node.Params[i] as Expr;
-        if (e != null) {
-          node.Params[i] = (Expr)this.Visit(e);
-        }
+        newParams.Add(e != null ? this.Visit(e) : node.Params[i]);
       }
+      node.ClearParams();
+      node.AddParams(newParams);
       if (node.Next != null) {
         node.Next = (QKeyValue)this.Visit(node.Next);
       }
@@ -522,11 +523,11 @@ namespace Microsoft.Boogie {
       if (origNext != null) {
         Trigger newNext = this.VisitTrigger(origNext);
         if (newNext != origNext) {
-          node = new Trigger(node.tok, node.Pos, node.Tr);  // note: this creates sharing between the old and new Tr sequence
+          node = new Trigger(node.tok, node.Pos, node.Tr.ToList());
           node.Next = newNext;
         }
       }
-      node.Tr = this.VisitExprSeq(node.Tr);
+      node.Tr = this.VisitExprSeq(node.Tr.ToList());
       return node;
     }
     // called by default for all nullary type constructors and type variables
@@ -1072,7 +1073,7 @@ namespace Microsoft.Boogie {
           {
               this.VisitTrigger(origNext);
           }
-          this.VisitExprSeq(node.Tr);
+          this.VisitExprSeq(node.Tr.ToList());
           return node;
       }
       // called by default for all nullary type constructors and type variables
diff --git a/Source/Core/Util.cs b/Source/Core/Util.cs
index b28ac042..73008742 100644
--- a/Source/Core/Util.cs
+++ b/Source/Core/Util.cs
@@ -229,6 +229,12 @@ namespace Microsoft.Boogie {
       this.SetToken(t => absy.tok = t);
     }
 
+    public void SetToken(IfThenElse expr)
+    {
+      Contract.Requires(expr != null);
+      this.SetToken(t => expr.tok = t);
+    }
+
     public void SetToken(Action<IToken> setter) {
       Contract.Requires(setter != null);
       if (this.setTokens) {
diff --git a/Source/Core/VCExp.cs b/Source/Core/VCExp.cs
index 5a8100a7..87b8f3e6 100644
--- a/Source/Core/VCExp.cs
+++ b/Source/Core/VCExp.cs
@@ -81,7 +81,7 @@ The generic options may or may not be used by the prover plugin.
       }
     }
 
-    public virtual void Parse(List<string/*!*/>/*!*/ opts) {
+    public virtual void Parse(IEnumerable<string/*!*/>/*!*/ opts) {
       Contract.Requires(cce.NonNullElements(opts));
       StringBuilder sb = new StringBuilder(stringRepr);
       Contract.Assert(sb != null);
author	Ally Donaldson <unknown>	2015-01-13 21:00:43 +0000
committer	Ally Donaldson <unknown>	2015-01-13 21:00:43 +0000
commit	d16fd70f1678b0e3f1683ba0c8b93f21d3d88cc4 (patch)
tree	7965c0c9c80e09d988359c9513dd9d9705f55038 /Source/Core
parent	7b1b91e940fd8ec7ac60074c843eb08f5715bc91 (diff)
parent	a1d2ad91bb39f7789015dbe9bd7bd7cc610a53e1 (diff)