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)

4 files changed, 38 insertions, 10 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 7622cbdf..6b07eb7e 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -1421,7 +1421,7 @@ namespace Microsoft.Boogie {
       QKeyValue kv;

       for (kv = this.Attributes; kv != null; kv = kv.Next) {

         if (kv.Key == name) {

-          kv.Params.AddRange(vals);

+          kv.AddParams(vals);

           break;

         }

       }

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index 89a3d1d1..6bc41b5f 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -2599,7 +2599,7 @@ namespace Microsoft.Boogie {
         if (QKeyValue.FindBoolAttribute(e.Attributes, "candidate"))

         {

             assume.Attributes = new QKeyValue(Token.NoToken, "candidate", new List<object>(), assume.Attributes);

-            assume.Attributes.Params.Add(this.callee);

+            assume.Attributes.AddParam(this.callee);

         }

         #endregion

         newBlockBody.Add(assume);

diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs
index 9cbadc80..cb792421 100644
--- a/Source/Core/AbsyQuant.cs
+++ b/Source/Core/AbsyQuant.cs
@@ -249,22 +249,49 @@ namespace Microsoft.Boogie {
 

   public class QKeyValue : Absy {

     public readonly string/*!*/ Key;

-    public readonly List<object/*!*/>/*!*/ Params;  // each element is either a string or an Expr

+    private readonly List<object/*!*/>/*!*/ _params;  // each element is either a string or an Expr

+

+    public void AddParam(object p)

+    {

+      Contract.Requires(p != null);

+      this._params.Add(p);

+    }

+

+    public void AddParams(IEnumerable<object> ps)

+    {

+      Contract.Requires(cce.NonNullElements(ps));

+      this._params.AddRange(ps);

+    }

+

+    public void ClearParams()

+    {

+      this._params.Clear();

+    }

+

+    public IList<object> Params

+    {

+      get

+      {

+        Contract.Ensures(cce.NonNullElements(Contract.Result<IList<object>>()));

+        Contract.Ensures(Contract.Result<IList<object>>().IsReadOnly);

+        return this._params.AsReadOnly();

+      }

+    }

+

     public QKeyValue Next;

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(Key != null);

-      Contract.Invariant(cce.NonNullElements(Params));

+      Contract.Invariant(cce.NonNullElements(this._params));

     }

 

-

-    public QKeyValue(IToken tok, string key, [Captured] List<object/*!*/>/*!*/ parameters, QKeyValue next)

+    public QKeyValue(IToken tok, string key, IList<object/*!*/>/*!*/ parameters, QKeyValue next)

       : base(tok) {

       Contract.Requires(key != null);

       Contract.Requires(tok != null);

       Contract.Requires(cce.NonNullElements(parameters));

       Key = key;

-      Params = parameters;

+      this._params = new List<object>(parameters);

       Next = next;

     }

 

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);

       }