Made invariant of class 'Trigger' robust by

-replacing public field by private field + getter
-using read-only wrappers (to avoid leaking)
-cloning the tr list in the setter and constructor (to avoid capturing)

3 files changed, 29 insertions, 18 deletions

diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs
index 9cbadc80..664d243d 100644
--- a/Source/Core/AbsyQuant.cs
+++ b/Source/Core/AbsyQuant.cs
@@ -389,32 +389,43 @@ namespace Microsoft.Boogie {
   public class Trigger : Absy {

     public readonly bool Pos;

     [Rep]

-    public List<Expr>/*!*/ Tr;

+    public 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, IList<Expr>/*!*/ tr, Trigger next = null)

       : base(tok) {

       Contract.Requires(tok != null);

       Contract.Requires(tr != null);

-      Contract.Requires(1 <= tr.Count);

+      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/StandardVisitor.cs b/Source/Core/StandardVisitor.cs
index 98ea4df3..58366051 100644
--- a/Source/Core/StandardVisitor.cs
+++ b/Source/Core/StandardVisitor.cs
@@ -526,7 +526,7 @@ namespace Microsoft.Boogie {
           node.Next = newNext;

         }

       }

-      node.Tr = this.VisitExprSeq(node.Tr);

+      node.Tr = this.VisitExprSeq(new List<Expr>(node.Tr));

       return node;

     }

     // called by default for all nullary type constructors and type variables

@@ -1072,7 +1072,7 @@ namespace Microsoft.Boogie {
           {

               this.VisitTrigger(origNext);

           }

-          this.VisitExprSeq(node.Tr);

+          node.Tr = this.VisitExprSeq(new List<Expr>(node.Tr));

           return node;

       }

       // called by default for all nullary type constructors and type variables

diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs
index a9963b72..91c17b23 100644
--- a/Source/VCExpr/Boogie2VCExpr.cs
+++ b/Source/VCExpr/Boogie2VCExpr.cs
@@ -76,7 +76,7 @@ namespace Microsoft.Boogie.VCExprAST {
       return Pop();

     }

 

-    public List<VCExpr/*!*/>/*!*/ Translate(List<Expr> exprs) {

+    public List<VCExpr/*!*/>/*!*/ Translate(IList<Expr> exprs) {

       Contract.Requires(exprs != null);

       Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExpr>>()));

       List<VCExpr/*!*/>/*!*/ res = new List<VCExpr/*!*/>();