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)

1 files changed, 1 insertions, 1 deletions

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/*!*/>();