From bce4de2f7c19fe59e650cb89a14e50a817b4b9ab Mon Sep 17 00:00:00 2001
From: 0biha <unknown>
Date: Thu, 1 Jan 2015 21:19:23 +0100
Subject: 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)

---
 Source/VCExpr/Boogie2VCExpr.cs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Source/VCExpr')

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/*!*/>();
-- 
cgit v1.2.3