diff options
| author |  0biha <unknown> | 2015-01-01 21:19:23 +0100 |
|---|---|---|
| committer | 0biha <unknown> | 2015-01-01 21:19:23 +0100 |
| commit | bce4de2f7c19fe59e650cb89a14e50a817b4b9ab (patch) | |
| tree | 6ae7e4764209e39bd93e6be6a8c8645cafba756e /Source/VCExpr/Boogie2VCExpr.cs | |
| parent | bc88f73ea679457f261bdc91797a43603d3befae (diff) | |
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)
Diffstat (limited to 'Source/VCExpr/Boogie2VCExpr.cs')
| -rw-r--r-- | Source/VCExpr/Boogie2VCExpr.cs | 2 |
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/*!*/>();
|