Protect the Args field of NAryExpr when it is immutable.

* Made changing the reference throw an exception if the NAryExpr was
constructed as immutable
* Changed the type of NAryExpr.Args to be IList<Expr> rather than
List<Expr> so that when the NAryExpr is immutable I can return
``_Args.AsReadOnly()`` (instead of ``_Args``) which returns a read
only wrapper around the List<Expr> so that clients cannot change the
list.

I came across two problems

* Making this change required changing types all over the place (from
List<Expr> to IList<Expr>). I feel that changes are extensive enough
that there's a good chance that out of tree clients using Boogie's
libraries might break. I've waited for a code review but this didn't
happen so I'm committing anyway.

* I came across something that looks like bad design of the IAppliable
interface which potentially breaks immutability enforcement. I've left
this as a "FIXME" in this. Here's the problematic method.

```
Type Typecheck(ref List<Expr>/*!*/ args, out
TypeParamInstantiation/*!*/ tpInstantiation, TypecheckingContext/*!*/
tc);
```

It potentially allows the instance of the args to be changed which
seems very suspect.

1 files changed, 2 insertions, 1 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 9f7e57cf..a1a54024 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -4129,6 +4129,7 @@ namespace Microsoft.Boogie {
   }

 

   public static class Emitter {

+

     public static void Emit(this List<Declaration/*!*/>/*!*/ decls, TokenTextWriter stream) {

       Contract.Requires(stream != null);

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

@@ -4156,7 +4157,7 @@ namespace Microsoft.Boogie {
       }

     }

 

-    public static void Emit(this List<Expr> ts, TokenTextWriter stream) {

+    public static void Emit(this IList<Expr> ts, TokenTextWriter stream) {

       Contract.Requires(stream != null);

       string sep = "";

       stream.push();