From 4410dba67b19995e40ab51c06922937b2cc55bc3 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Thu, 12 Feb 2015 11:25:49 +0000
Subject: Fix what looked like a serious design issue when Type checking
 anything that implements the IAppliable interface. Type checking should never
 need to change the reference of a list of arguments (hence the removal of the
 ``ref`` keyword) and we need to use IList<Expr> instead of List<Expr> to
 allow NAryExpr to do its type checking.

---
 Source/Core/AbsyExpr.cs | 23 ++++++++++++-----------
 1 file changed, 12 insertions(+), 11 deletions(-)

(limited to 'Source/Core/AbsyExpr.cs')

diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index 7557a796..75f2c519 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -1131,7 +1131,7 @@ namespace Microsoft.Boogie {
     /// </summary>
     /// <param name="args"></param>
     /// <param name="tc"></param>
-    Type Typecheck(ref List<Expr>/*!*/ args, out TypeParamInstantiation/*!*/ tpInstantiation, TypecheckingContext/*!*/ tc);
+    Type Typecheck(IList<Expr>/*!*/ args, out TypeParamInstantiation/*!*/ tpInstantiation, TypecheckingContext/*!*/ tc);
 
     // Contract.Requires( Microsoft.SpecSharp.Collections.Reductions.Forall{Expr! arg in args; arg.Type != null});
 
@@ -1172,7 +1172,7 @@ namespace Microsoft.Boogie {
       }
     }
 
-    public Type Typecheck(ref List<Expr> args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {
+    public Type Typecheck(IList<Expr> args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {
       Contract.Requires(args != null);
       Contract.Requires(tc != null);
       Contract.Ensures(Contract.ValueAtReturn(out args) != null);
@@ -1315,7 +1315,7 @@ namespace Microsoft.Boogie {
       }
     }
 
-    public Type Typecheck(ref List<Expr> args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {
+    public Type Typecheck(IList<Expr> args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {
       //Contract.Requires(tc != null);
       //Contract.Requires(args != null);
       Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null);
@@ -1625,7 +1625,7 @@ namespace Microsoft.Boogie {
         return 2;
       }
     }
-    public Type Typecheck(ref List<Expr> args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {
+    public Type Typecheck(IList<Expr> args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {
       //Contract.Requires(tc != null);
       //Contract.Requires(args != null);
       Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null);
@@ -1997,7 +1997,7 @@ namespace Microsoft.Boogie {
         return Func.InParams.Count;
       }
     }
-    public virtual Type Typecheck(ref List<Expr> actuals, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {
+    public virtual Type Typecheck(IList<Expr> actuals, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {
       //Contract.Requires(tc != null);
       //Contract.Requires(actuals != null);
       Contract.Ensures(Contract.ValueAtReturn(out actuals) != null);
@@ -2112,7 +2112,7 @@ namespace Microsoft.Boogie {
       }
     }
 
-    public Type Typecheck(ref List<Expr>/*!*/ args,
+    public Type Typecheck(IList<Expr>/*!*/ args,
                           out TypeParamInstantiation/*!*/ tpInstantiation,
                           TypecheckingContext/*!*/ tc) {
       //Contract.Requires(args != null);
@@ -2223,7 +2223,7 @@ namespace Microsoft.Boogie {
       //Contract.Requires(rc != null);
     }
 
-    public virtual Type Typecheck(ref List<Expr> args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {
+    public virtual Type Typecheck(IList<Expr> args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {
       //Contract.Requires(tc != null);
       //Contract.Requires(args != null);
       Contract.Ensures(args != null);
@@ -2395,7 +2395,7 @@ namespace Microsoft.Boogie {
         // typechecked and does not need to be checked again
                TypeParameters == null) {
         TypeParamInstantiation tpInsts;
-        Type = Fun.Typecheck(ref _Args, out tpInsts, tc); // FIXME: Might break immutability
+        Type = Fun.Typecheck(Args, out tpInsts, tc); // Make sure we pass Args so if this Expr is immutable it is protected
         TypeParameters = tpInsts;
       }
       IOverloadedAppliable oa = Fun as IOverloadedAppliable;
@@ -2563,12 +2563,13 @@ namespace Microsoft.Boogie {
       }
     }
 
-    public Type Typecheck(ref List<Expr> args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {
+    public Type Typecheck(IList<Expr> args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {
       //Contract.Requires(tc != null);
       //Contract.Requires(args != null);
       Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null);
       Contract.Assume(args.Count == Arity + 1);
 
+      // FIXME: Wny are we passing a copy?
       List<Expr> actualArgs = new List<Expr>();
       for (int i = 1; i < args.Count; ++i)
         actualArgs.Add(args[i]);
@@ -2697,7 +2698,7 @@ namespace Microsoft.Boogie {
       return cce.NonNull(args[0]).Type;
     }
 
-    public Type Typecheck(ref List<Expr>/*!*/ args,
+    public Type Typecheck(IList<Expr>/*!*/ args,
                           out TypeParamInstantiation/*!*/ tpInstantiation,
                           TypecheckingContext/*!*/ tc) {
       //Contract.Requires(args != null);
@@ -2803,7 +2804,7 @@ namespace Microsoft.Boogie {
       }
     }
 
-    public Type Typecheck(ref List<Expr> args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {
+    public Type Typecheck(IList<Expr> args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {
       //Contract.Requires(tc != null);
       //Contract.Requires(args != null);
       Contract.Ensures(args != null);
-- 
cgit v1.2.3