Made invariant of class 'QKeyValue' robust by:

- making field private
- exposing read-only list
- copying incoming list
- adding methods 'AddParam', 'AddParams', and 'ClearParams'
(with help from David Rohr)

1 files changed, 4 insertions, 3 deletions

diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs
index 98ea4df3..68de45f6 100644
--- a/Source/Core/StandardVisitor.cs
+++ b/Source/Core/StandardVisitor.cs
@@ -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);

       }