Merge

15 files changed, 273 insertions, 223 deletions

diff --git a/.hgignore b/.hgignore
index a3ce089b..ccf5384a 100644
--- a/.hgignore
+++ b/.hgignore
@@ -7,9 +7,11 @@ syntax: regexp
 ^.*(bin|obj)/([^/]*/)?(Debug|Release|Checked|Debug All|DEBUG ALL)/.*$

 ^Binaries/BytecodeTranslator$

 ^BCT/Binaries/.*$

+^Chalice/bin/

 Test/([^/]*)/Output

 Test/([^/]*)/([^/]*)\.sx

-Test/(dafny0|dafny1|VSI-Benchmarks|vacid0|VSComp2010)/out\.cs

+Test/(dafny0|dafny1|VSI-Benchmarks|vacid0|VSComp2010)/(out\.cs|.*\.dll|.*\.pdb|.*\.exe)

+Test/desktop/

 ^.*~$

 syntax: glob

 BCT/TestResults/

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index e4f8d1ff..2ec38e8b 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -424,18 +424,18 @@ namespace BytecodeTranslator
     /// </summary>

     /// <param name="methodCall"></param>

     /// <remarks>Stub, This one really needs comments!</remarks>

-    public override void Visit(IMethodCall methodCall)

-    {

-      var resolvedMethod = methodCall.MethodToCall.ResolvedMethod;

+    public override void Visit(IMethodCall methodCall) {

+      var resolvedMethod = Sink.Unspecialize(methodCall.MethodToCall).ResolvedMethod;

+

       if (resolvedMethod == Dummy.Method) {

         throw new TranslationException(

           ExceptionType.UnresolvedMethod,

           MemberHelper.GetMethodSignature(methodCall.MethodToCall, NameFormattingOptions.None));

       }

-        

-      #region Translate In Parameters

 

+      #region Translate In and Out Parameters

       var inexpr = new List<Bpl.Expr>();

+      var outvars = new List<Bpl.IdentifierExpr>();

 

       #region Create the 'this' argument for the function call

       Bpl.IdentifierExpr thisExpr = null;

@@ -443,8 +443,7 @@ namespace BytecodeTranslator
       List<IFieldDefinition> args = null;

       Bpl.Expr arrayExpr = null;

       Bpl.Expr indexExpr = null;

-      if (!methodCall.IsStaticCall)

-      {

+      if (!methodCall.IsStaticCall) {

         this.collectStructFields = true;

         this.structFields = new List<IFieldDefinition>();

         this.arrayExpr = null;

@@ -456,175 +455,145 @@ namespace BytecodeTranslator
         indexExpr = this.indexExpr;

 

         var e = this.TranslatedExpressions.Pop();

-        if (false && methodCall.MethodToCall.ContainingType.IsValueType)

-        {

-          // then the "this arg" was actually an AddressOf the struct

-          // but we are going to ignore that and just get the identifier

-          // that it was the address of

-          var nAry = e as Bpl.NAryExpr;

-          var nAryArgs = nAry.Args;

-          e = nAryArgs[0] as Bpl.IdentifierExpr;

-        }

         inexpr.Add(e);

-        if (e is Bpl.NAryExpr)

-        {

+        if (e is Bpl.NAryExpr) {

           e = ((Bpl.NAryExpr)e).Args[0];

         }

         thisExpr = e as Bpl.IdentifierExpr;

         locals = new List<Bpl.Variable>();

         Bpl.Variable x = thisExpr.Decl;

         locals.Add(x);

-        for (int i = 0; i < args.Count; i++)

-        {

+        for (int i = 0; i < args.Count; i++) {

           Bpl.IdentifierExpr g = Bpl.Expr.Ident(this.sink.FindOrCreateFieldVariable(args[i]));

           Bpl.Variable y = this.sink.CreateFreshLocal(args[i].Type);

           StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(y), this.sink.Heap.ReadHeap(Bpl.Expr.Ident(x), g, args[i].ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap, y.TypedIdent.Type)));

           x = y;

           locals.Add(y);

         }

-        //thisExpr = Bpl.Expr.Ident(x);

-        //inexpr.Add(thisExpr);

+      }

+      if (!methodCall.IsStaticCall && methodCall.MethodToCall.ContainingType.ResolvedType.IsStruct) {

+        outvars.Add(thisExpr);

       }

       #endregion

 

-      Dictionary<IParameterDefinition, Bpl.Expr> p2eMap = new Dictionary<IParameterDefinition, Bpl.Expr>();

+      Dictionary<Bpl.IdentifierExpr, Bpl.IdentifierExpr> toBoxed = new Dictionary<Bpl.IdentifierExpr, Bpl.IdentifierExpr>();

+      Dictionary<IParameterDefinition, Bpl.IdentifierExpr> p2eMap = new Dictionary<IParameterDefinition, Bpl.IdentifierExpr>();

       IEnumerator<IParameterDefinition> penum = resolvedMethod.Parameters.GetEnumerator();

       penum.MoveNext();

-      foreach (IExpression exp in methodCall.Arguments)

-      {

-        if (penum.Current == null)

-        {

-          throw new TranslationException("More Arguments than Parameters in functioncall");

+      foreach (IExpression exp in methodCall.Arguments) {

+        if (penum.Current == null) {

+          throw new TranslationException("More arguments than parameters in method call");

         }

         this.Visit(exp);

         Bpl.Expr e = this.TranslatedExpressions.Pop();

-

-        p2eMap.Add(penum.Current, e);

-        if (!penum.Current.IsOut)

-        {

+        if (penum.Current.Type is IGenericTypeParameter)

+          inexpr.Add(sink.Heap.Box(methodCall.Token(), this.sink.CciTypeToBoogie(exp.Type), e));

+        else

           inexpr.Add(e);

+        if (penum.Current.IsByReference) {

+          Bpl.IdentifierExpr unboxed = e as Bpl.IdentifierExpr;

+          if (unboxed == null) {

+            throw new TranslationException("Trying to pass a complex expression for an out or ref parameter");

+          }

+          if (penum.Current.Type is IGenericTypeParameter) {

+            Bpl.IdentifierExpr boxed = Bpl.Expr.Ident(sink.CreateFreshLocal(this.sink.Heap.BoxType));

+            toBoxed[unboxed] = boxed;

+            outvars.Add(boxed);

+          }

+          else {

+            outvars.Add(unboxed);

+          }

         }

-

         penum.MoveNext();

       }

       #endregion

 

       Bpl.IToken cloc = methodCall.Token();

-

-      // meeting a constructor is always something special

-      if (false && resolvedMethod.IsConstructor)

-      {

-        // Todo: do something with the constructor call

-      }

-      else

-      {

-        // Todo: if there is no stmttraverser we are visiting a contract and should use a boogie function instead of procedure!

-

-        #region Translate Out vars

-        var outvars = new List<Bpl.IdentifierExpr>();

-        if (!methodCall.IsStaticCall && methodCall.MethodToCall.ContainingType.ResolvedType.IsStruct) {

-          outvars.Add(thisExpr);

+      if (resolvedMethod.Type.ResolvedType.TypeCode != PrimitiveTypeCode.Void) {

+        Bpl.Variable v = this.sink.CreateFreshLocal(methodCall.Type.ResolvedType);

+        Bpl.IdentifierExpr unboxed = new Bpl.IdentifierExpr(cloc, v);

+        if (resolvedMethod.Type is IGenericTypeParameter) {

+          Bpl.IdentifierExpr boxed = Bpl.Expr.Ident(this.sink.CreateFreshLocal(this.sink.Heap.BoxType));

+          toBoxed[unboxed] = boxed;

+          outvars.Add(boxed);

         }

-        foreach (KeyValuePair<IParameterDefinition, Bpl.Expr> kvp in p2eMap)

-        {

-          if (kvp.Key.IsOut || kvp.Key.IsByReference)

-          {

-            Bpl.IdentifierExpr iexp = kvp.Value as Bpl.IdentifierExpr;

-            if (iexp == null)

-            {

-              throw new TranslationException("Trying to pass complex expression as out in functioncall");

-            }

-            outvars.Add(iexp);

-          }

+        else {

+          outvars.Add(unboxed);

         }

-        #endregion

+        TranslatedExpressions.Push(unboxed);

+      }

+      var proc = this.sink.FindOrCreateProcedure(resolvedMethod);

+      string methodname = proc.Name;

 

-        if (methodCall.Type.ResolvedType.TypeCode != PrimitiveTypeCode.Void)

-        {

-          Bpl.Variable v = this.sink.CreateFreshLocal(methodCall.Type.ResolvedType);

-          outvars.Add(new Bpl.IdentifierExpr(cloc, v));

-          TranslatedExpressions.Push(new Bpl.IdentifierExpr(cloc, v));

+      Bpl.QKeyValue attrib = null;

+      foreach (var a in resolvedMethod.Attributes) {

+        if (TypeHelper.GetTypeName(a.Type).EndsWith("AsyncAttribute")) {

+          attrib = new Bpl.QKeyValue(cloc, "async", new List<object>(), null);

         }

-        var proc = this.sink.FindOrCreateProcedure(resolvedMethod);

-        string methodname = proc.Name;

+      }

 

-        Bpl.QKeyValue attrib = null;

-        foreach (var a in resolvedMethod.Attributes)

-        {

-          if (TypeHelper.GetTypeName(a.Type).EndsWith("AsyncAttribute"))

-          {

-            attrib = new Bpl.QKeyValue(cloc, "async", new List<object>(), null);

-          }

+      Bpl.CallCmd call;

+      bool isEventAdd = resolvedMethod.IsSpecialName && resolvedMethod.Name.Value.StartsWith("add_");

+      bool isEventRemove = resolvedMethod.IsSpecialName && resolvedMethod.Name.Value.StartsWith("remove_");

+      if (isEventAdd || isEventRemove) {

+        var mName = resolvedMethod.Name.Value;

+        var eventName = mName.Substring(mName.IndexOf('_') + 1);

+        var eventDef = TypeHelper.GetEvent(resolvedMethod.ContainingTypeDefinition, this.sink.host.NameTable.GetNameFor(eventName));

+        Contract.Assert(eventDef != Dummy.Event);

+        Bpl.Variable eventVar = this.sink.FindOrCreateEventVariable(eventDef);

+        Bpl.Variable local = this.sink.CreateFreshLocal(eventDef.Type);

+

+        if (methodCall.IsStaticCall) {

+          this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(local), Bpl.Expr.Ident(eventVar)));

+          inexpr.Insert(0, Bpl.Expr.Ident(local));

+        }

+        else {

+          this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(local), this.sink.Heap.ReadHeap(thisExpr, Bpl.Expr.Ident(eventVar), resolvedMethod.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap, local.TypedIdent.Type)));

+          inexpr[0] = Bpl.Expr.Ident(local);

         }

 

-        Bpl.CallCmd call;

-        bool isEventAdd = resolvedMethod.IsSpecialName && resolvedMethod.Name.Value.StartsWith("add_");

-        bool isEventRemove = resolvedMethod.IsSpecialName && resolvedMethod.Name.Value.StartsWith("remove_");

-        if (isEventAdd || isEventRemove)

-        {

-          var mName = resolvedMethod.Name.Value;

-          var eventName = mName.Substring(mName.IndexOf('_')+1);

-          var eventDef = TypeHelper.GetEvent(resolvedMethod.ContainingTypeDefinition, this.sink.host.NameTable.GetNameFor(eventName));

-          Contract.Assert(eventDef != Dummy.Event);

-          Bpl.Variable eventVar = this.sink.FindOrCreateEventVariable(eventDef);

-          Bpl.Variable local = this.sink.CreateFreshLocal(eventDef.Type);

-

-          if (methodCall.IsStaticCall)

-          {

-            this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(local), Bpl.Expr.Ident(eventVar)));

-            inexpr.Insert(0, Bpl.Expr.Ident(local));

-          }

-          else 

-          {

-            this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(local), this.sink.Heap.ReadHeap(thisExpr, Bpl.Expr.Ident(eventVar), resolvedMethod.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap, local.TypedIdent.Type)));

-            inexpr[0] = Bpl.Expr.Ident(local);

-          }

-

-          System.Diagnostics.Debug.Assert(outvars.Count == 0);

-          outvars.Add(Bpl.Expr.Ident(local));

-          string methodName = isEventAdd ? this.sink.DelegateAddName : this.sink.DelegateRemoveName;

-          call = new Bpl.CallCmd(methodCall.Token(), methodName, inexpr, outvars);

-          this.StmtTraverser.StmtBuilder.Add(call);

-          if (methodCall.IsStaticCall)

-          {

-            this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(eventVar), Bpl.Expr.Ident(local)));

-          }

-          else

-          {

-            this.StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(methodCall.Token(), thisExpr, Bpl.Expr.Ident(eventVar), Bpl.Expr.Ident(local), resolvedMethod.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap, local.TypedIdent.Type));

-          }

+        System.Diagnostics.Debug.Assert(outvars.Count == 0);

+        outvars.Add(Bpl.Expr.Ident(local));

+        string methodName = isEventAdd ? this.sink.DelegateAddName : this.sink.DelegateRemoveName;

+        call = new Bpl.CallCmd(methodCall.Token(), methodName, inexpr, outvars);

+        this.StmtTraverser.StmtBuilder.Add(call);

+        if (methodCall.IsStaticCall) {

+          this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(eventVar), Bpl.Expr.Ident(local)));

         }

-        else

-        {

-          if (attrib != null)

-            call = new Bpl.CallCmd(cloc, methodname, inexpr, outvars, attrib);

-          else

-            call = new Bpl.CallCmd(cloc, methodname, inexpr, outvars);

-          this.StmtTraverser.StmtBuilder.Add(call);

+        else {

+          this.StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(methodCall.Token(), thisExpr, Bpl.Expr.Ident(eventVar), Bpl.Expr.Ident(local), resolvedMethod.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap, local.TypedIdent.Type));

         }

+      }

+      else {

+        if (attrib != null)

+          call = new Bpl.CallCmd(cloc, methodname, inexpr, outvars, attrib);

+        else

+          call = new Bpl.CallCmd(cloc, methodname, inexpr, outvars);

+        this.StmtTraverser.StmtBuilder.Add(call);

+      }

 

-        if (!methodCall.IsStaticCall) {

-          Debug.Assert(args != null && locals != null);

-          int count = args.Count;

-          Bpl.Variable x = locals[count];

+      foreach (KeyValuePair<Bpl.IdentifierExpr, Bpl.IdentifierExpr> kv in toBoxed) {

+        this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(kv.Key, this.sink.Heap.Unbox(Bpl.Token.NoToken, kv.Key.Type, kv.Value)));

+      }

+

+      if (!methodCall.IsStaticCall) {

+        Debug.Assert(args != null && locals != null);

+        int count = args.Count;

+        Bpl.Variable x = locals[count];

+        count--;

+        while (0 <= count) {

+          IFieldDefinition currField = args[count];

+          Bpl.IdentifierExpr g = Bpl.Expr.Ident(this.sink.FindOrCreateFieldVariable(currField));

+          Bpl.Variable y = locals[count];

+          StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(methodCall.Token(), Bpl.Expr.Ident(y), g, Bpl.Expr.Ident(x), currField.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap, x.TypedIdent.Type));

+          x = y;

           count--;

-          while (0 <= count)

-          {

-            IFieldDefinition currField = args[count];

-            Bpl.IdentifierExpr g = Bpl.Expr.Ident(this.sink.FindOrCreateFieldVariable(currField));

-            Bpl.Variable y = locals[count];

-            StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(methodCall.Token(), Bpl.Expr.Ident(y), g, Bpl.Expr.Ident(x), currField.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap, x.TypedIdent.Type));

-            x = y;

-            count--;

-          }

-          if (indexExpr != null) {

-            Debug.Assert(arrayExpr != null);

-            StmtTraverser.StmtBuilder.Add(sink.Heap.WriteHeap(Bpl.Token.NoToken, arrayExpr, indexExpr, Bpl.Expr.Ident(x), AccessType.Array, x.TypedIdent.Type));

-          }

         }

-

+        if (indexExpr != null) {

+          Debug.Assert(arrayExpr != null);

+          StmtTraverser.StmtBuilder.Add(sink.Heap.WriteHeap(Bpl.Token.NoToken, arrayExpr, indexExpr, Bpl.Expr.Ident(x), AccessType.Array, x.TypedIdent.Type));

+        }

       }

-

     }

 

     #endregion

@@ -762,7 +731,7 @@ namespace BytecodeTranslator
     /// </summary>

     public override void Visit(ICreateObjectInstance createObjectInstance)

     {

-      TranslateObjectCreation(createObjectInstance.MethodToCall, createObjectInstance.Arguments, createObjectInstance.Type, createObjectInstance);

+      TranslateObjectCreation(createObjectInstance.MethodToCall, createObjectInstance.Arguments, createObjectInstance);

     }

 

     public override void Visit(ICreateArray createArrayInstance)

@@ -794,35 +763,32 @@ namespace BytecodeTranslator
       TranslatedExpressions.Push(Bpl.Expr.Ident(a));

     }

 

-    private void TranslateObjectCreation(IMethodReference ctor, IEnumerable<IExpression> arguments, ITypeReference ctorType, IExpression creationAST)

+    private void TranslateObjectCreation(IMethodReference ctor, IEnumerable<IExpression> arguments, IExpression creationAST)

     {

+      var resolvedMethod = Sink.Unspecialize(ctor).ResolvedMethod;

       Bpl.IToken token = creationAST.Token();

-

+      

       var a = this.sink.CreateFreshLocal(creationAST.Type);

 

       // First generate an Alloc() call

       this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(token, this.sink.AllocationMethodName, new Bpl.ExprSeq(), new Bpl.IdentifierExprSeq(Bpl.Expr.Ident(a))));

 

       // Second, generate the call to the appropriate ctor

-      var proc = this.sink.FindOrCreateProcedure(ctor.ResolvedMethod);

+      var proc = this.sink.FindOrCreateProcedure(resolvedMethod);

       Bpl.ExprSeq inexpr = new Bpl.ExprSeq();

       inexpr.Add(Bpl.Expr.Ident(a));

-      IEnumerator<IParameterDefinition> penum = ctor.ResolvedMethod.Parameters.GetEnumerator();

+      IEnumerator<IParameterDefinition> penum = resolvedMethod.Parameters.GetEnumerator();

       penum.MoveNext();

-      foreach (IExpression exp in arguments)

-      {

-        if (penum.Current == null)

-        {

+      foreach (IExpression exp in arguments) {

+        if (penum.Current == null) {

           throw new TranslationException("More Arguments than Parameters in functioncall");

         }

         this.Visit(exp);

         Bpl.Expr e = this.TranslatedExpressions.Pop();

-

-        if (!penum.Current.IsOut)

-        {

+        if (penum.Current.Type is IGenericTypeParameter)

+          inexpr.Add(sink.Heap.Box(ctor.Token(), this.sink.CciTypeToBoogie(exp.Type), e));

+        else

           inexpr.Add(e);

-        }

-

         penum.MoveNext();

       }

 

diff --git a/BCT/BytecodeTranslator/HeapFactory.cs b/BCT/BytecodeTranslator/HeapFactory.cs
index 812fddb1..6d03ef9f 100644
--- a/BCT/BytecodeTranslator/HeapFactory.cs
+++ b/BCT/BytecodeTranslator/HeapFactory.cs
@@ -148,6 +148,9 @@ namespace BytecodeTranslator {
     [RepresentationFor("Real2Box", "function Real2Box(Real): Box;")]

     public Bpl.Function Real2Box = null;

 

+    [RepresentationFor("Box2Box", "function {:inline true} Box2Box(b: Box): Box { b }")]

+    public Bpl.Function Box2Box = null;

+

     public Bpl.Expr Box(Bpl.IToken tok, Bpl.Type boogieType, Bpl.Expr expr) {

       Bpl.Function conversion;

       if (boogieType == Bpl.Type.Bool)

@@ -160,6 +163,8 @@ namespace BytecodeTranslator {
         conversion = this.Ref2Box;

       else if (boogieType == RealType)

         conversion = this.Real2Box;

+      else if (boogieType == BoxType)

+        conversion = this.Box2Box;

       else

         throw new InvalidOperationException(String.Format("Unknown Boogie type: '{0}'", boogieType.ToString()));

 

@@ -183,6 +188,8 @@ namespace BytecodeTranslator {
         conversion = this.Box2Ref;

       else if (boogieType == RealType)

         conversion = this.Box2Real;

+      else if (boogieType == BoxType)

+        conversion = this.Box2Box;

       else

         throw new InvalidOperationException(String.Format("Unknown Boogie type: '{0}'", boogieType.ToString()));

 

diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs
index 1fa59767..58bec27f 100644
--- a/BCT/BytecodeTranslator/MetadataTraverser.cs
+++ b/BCT/BytecodeTranslator/MetadataTraverser.cs
@@ -262,7 +262,7 @@ namespace BytecodeTranslator {
         #region Create Local Vars For Implementation

         List<Bpl.Variable> vars = new List<Bpl.Variable>();

         foreach (MethodParameter mparam in formalMap.Values) {

-          if (!(mparam.underlyingParameter.IsByReference || mparam.underlyingParameter.IsOut))

+          if (!mparam.underlyingParameter.IsByReference)

             vars.Add(mparam.outParameterCopy);

         }

         foreach (Bpl.Variable v in this.sink.LocalVarMap.Values) {

diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs
index 629e7e54..b8d8334d 100644
--- a/BCT/BytecodeTranslator/Sink.cs
+++ b/BCT/BytecodeTranslator/Sink.cs
@@ -99,6 +99,9 @@ namespace BytecodeTranslator {
         return Bpl.Expr.Ident(this.Heap.DefaultStruct);

       } else if (bplType == this.Heap.RefType) {

         return Bpl.Expr.Ident(this.Heap.NullRef);

+      }

+      else if (bplType == this.Heap.BoxType) {

+        return Bpl.Expr.Ident(this.Heap.DefaultBox);

       } else {

         throw new NotImplementedException(String.Format("Don't know how to translate type: '{0}'", TypeHelper.GetTypeName(type)));

       }

@@ -113,9 +116,11 @@ namespace BytecodeTranslator {
         return heap.RealType;

       else if (type.ResolvedType.IsStruct)

         return heap.StructType;

-      else if (type.IsEnum) {

+      else if (type.IsEnum)

         return Bpl.Type.Int; // The underlying type of an enum is always some kind of integer

-      } else

+      else if (type is IGenericTypeParameter) 

+        return heap.BoxType;

+      else

         return heap.RefType;

     }

 

@@ -134,6 +139,14 @@ namespace BytecodeTranslator {
       return v;

     }

 

+    public Bpl.Variable CreateFreshLocal(Bpl.Type t) {

+      Bpl.IToken loc = Bpl.Token.NoToken; // Helper Variables do not have a location

+      Bpl.LocalVariable v = new Bpl.LocalVariable(loc, new Bpl.TypedIdent(loc, TranslationHelper.GenerateTempVarName(), t));

+      ILocalDefinition dummy = new LocalDefinition(); // Creates a dummy entry for the Dict, since only locals in the dict are translated to boogie

+      localVarMap.Add(dummy, v);

+      return v;

+    }

+

     /// <summary>

     /// State that gets re-initialized per method

     /// </summary>

@@ -335,10 +348,9 @@ namespace BytecodeTranslator {
         MethodParameter mp;

         var formalMap = new Dictionary<IParameterDefinition, MethodParameter>();

         foreach (IParameterDefinition formal in method.Parameters) {

-

           mp = new MethodParameter(formal, this.CciTypeToBoogie(formal.Type));

           if (mp.inParameterCopy != null) in_count++;

-          if (mp.outParameterCopy != null && (formal.IsByReference || formal.IsOut))

+          if (mp.outParameterCopy != null && formal.IsByReference)

             out_count++;

           formalMap.Add(formal, mp);

         }

@@ -397,7 +409,7 @@ namespace BytecodeTranslator {
             invars[i++] = mparam.inParameterCopy;

           }

           if (mparam.outParameterCopy != null) {

-            if (mparam.underlyingParameter.IsByReference || mparam.underlyingParameter.IsOut)

+            if (mparam.underlyingParameter.IsByReference)

               outvars[j++] = mparam.outParameterCopy;

           }

         }

@@ -563,7 +575,7 @@ namespace BytecodeTranslator {
       this.FindOrCreateProcedure(method);

       return this.declaredMethods[method.InternedKey];

     }

-    private static IMethodReference Unspecialize(IMethodReference method) {

+    public static IMethodReference Unspecialize(IMethodReference method) {

       IMethodReference result = method;

       var gmir = result as IGenericMethodInstanceReference;

       if (gmir != null) {

diff --git a/BCT/BytecodeTranslator/TranslationHelper.cs b/BCT/BytecodeTranslator/TranslationHelper.cs
index 42b1a4d0..54ed1700 100644
--- a/BCT/BytecodeTranslator/TranslationHelper.cs
+++ b/BCT/BytecodeTranslator/TranslationHelper.cs
@@ -37,22 +37,18 @@ namespace BytecodeTranslator {
     public IParameterDefinition underlyingParameter;

 

     public MethodParameter(IParameterDefinition parameterDefinition, Bpl.Type ptype) {

-

       this.underlyingParameter = parameterDefinition;

 

       var parameterToken = parameterDefinition.Token();

       var typeToken = parameterDefinition.Type.Token();

       var parameterName = parameterDefinition.Name.Value;

 

-      if (!parameterDefinition.IsOut) {

-        this.inParameterCopy = new Bpl.Formal(parameterToken, new Bpl.TypedIdent(typeToken, parameterName + "$in", ptype), true);

-      }

-      if (parameterDefinition.IsByReference || parameterDefinition.IsOut) {

+      this.inParameterCopy = new Bpl.Formal(parameterToken, new Bpl.TypedIdent(typeToken, parameterName + "$in", ptype), true);

+      if (parameterDefinition.IsByReference) {

         this.outParameterCopy = new Bpl.Formal(parameterToken, new Bpl.TypedIdent(typeToken, parameterName + "$out", ptype), false);

       } else {

         this.outParameterCopy = new Bpl.LocalVariable(parameterToken, new Bpl.TypedIdent(typeToken, parameterName, ptype));

       }

-      

     }

 

     public override string ToString() {

diff --git a/BCT/BytecodeTranslator/WholeProgram.cs b/BCT/BytecodeTranslator/WholeProgram.cs
index f4cc59af..92154020 100644
--- a/BCT/BytecodeTranslator/WholeProgram.cs
+++ b/BCT/BytecodeTranslator/WholeProgram.cs
@@ -149,13 +149,11 @@ namespace BytecodeTranslator {
 

         Bpl.IToken token = methodCall.Token();

 

-        // TODO: if there is no stmttraverser we are visiting a contract and should use a boogie function instead of procedure!

-

         #region Translate Out vars

         var outvars = new List<Bpl.IdentifierExpr>();

 

         foreach (KeyValuePair<IParameterDefinition, Bpl.Expr> kvp in p2eMap) {

-          if (kvp.Key.IsOut || kvp.Key.IsByReference) {

+          if (kvp.Key.IsByReference) {

             Bpl.IdentifierExpr iexp = kvp.Value as Bpl.IdentifierExpr;

             if (iexp == null) {

               throw new TranslationException("Trying to pass complex expression as out in functioncall");

diff --git a/BCT/Samples/Generics/GenericsExample.cs b/BCT/Samples/Generics/GenericsExample.cs
new file mode 100644
index 00000000..c7016ceb
--- /dev/null
+++ b/BCT/Samples/Generics/GenericsExample.cs
@@ -0,0 +1,20 @@
+using System;

+using System.Collections.Generic;

+using System.Diagnostics.Contracts;

+using System.Linq;

+using System.Text;

+

+/* Simple example of generics/dictionary support needed by Poirot */

+class GenericsExample

+{

+    public static void Main()

+    {

+        Dictionary<String, String> dict = new Dictionary<String, String>();

+        dict["foo"] = "bar";

+        Contract.Assert(dict.ContainsKey("foo"));

+        Contract.Assert(dict.ContainsValue("bar"));

+        Contract.Assert(dict["foo"] == "bar");

+        dict.Remove("foo");

+        Contract.Assert(dict["foo"] == "bar"); // should fail

+    }

+}
\ No newline at end of file
diff --git a/BCT/Samples/Strings/StringsExample.cs b/BCT/Samples/Strings/StringsExample.cs
new file mode 100644
index 00000000..a04fc9a0
--- /dev/null
+++ b/BCT/Samples/Strings/StringsExample.cs
@@ -0,0 +1,20 @@
+using System;

+using System.Collections.Generic;

+using System.Diagnostics.Contracts;

+using System.Linq;

+using System.Text;

+

+/* Example of string functionality needed by Poirot: concatenation and equality */

+class StringsExample

+{

+    public static void Main()

+    {

+        string foo = "delicious";

+        string bar = "cake";

+        Contract.Assert(!foo.Equals(bar));

+        string foo_bar = foo + bar;

+        Contract.Assert(foo_bar.Equals("deliciouscake"));

+        string delish = "delicious";

+        Contract.Assert(foo.Equals(delish));

+    }

+}
\ No newline at end of file
diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs
index 63cca64a..b10aeac9 100644
--- a/Binaries/DafnyRuntime.cs
+++ b/Binaries/DafnyRuntime.cs
@@ -122,6 +122,7 @@ namespace Dafny
         // return the first one

         return t;

       }

+      return default(T);

     }

   }

   public class Sequence<T>

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 62270067..9495d64e 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -66,7 +66,7 @@ namespace Microsoft.Dafny {
       foreach (ModuleDecl m in program.Modules) {

         int indent = 0;

         if (!m.IsDefaultModule) {

-          wr.WriteLine("namespace {0} {{", m.Name);

+          wr.WriteLine("namespace @{0} {{", m.Name);

           indent += IndentAmount;

         }

         foreach (TopLevelDecl d in m.TopLevelDecls) {

@@ -84,7 +84,7 @@ namespace Microsoft.Dafny {
           } else {

             ClassDecl cl = (ClassDecl)d;

             Indent(indent);

-            wr.Write("public class {0}", cl.Name);

+            wr.Write("public class @{0}", cl.Name);

             if (cl.TypeArgs.Count != 0) {

               wr.Write("<{0}>", TypeParameters(cl.TypeArgs));

             }

@@ -199,17 +199,17 @@ namespace Microsoft.Dafny {
           wr.Write(">");

         }

         wr.Write(" : Base_{0}", dt.Name);

-        wr.WriteLine(" {");

         if (dt.TypeArgs.Count != 0) {

           wr.Write("<{0}>", TypeParameters(dt.TypeArgs));

         }

+        wr.WriteLine(" {");

         int ind = indent + IndentAmount;

 

         int i = 0;

         foreach (Formal arg in ctor.Formals) {

           if (!arg.IsGhost) {

             Indent(ind);

-            wr.WriteLine("public readonly {0} {1};", TypeName(arg.Type), FormalName(arg, i));

+            wr.WriteLine("public readonly {0} @{1};", TypeName(arg.Type), FormalName(arg, i));

             i++;

           }

         }

@@ -222,7 +222,7 @@ namespace Microsoft.Dafny {
         foreach (Formal arg in ctor.Formals) {

           if (!arg.IsGhost) {

             Indent(ind + IndentAmount);

-            wr.WriteLine("this.{0} = {0};", FormalName(arg, i));

+            wr.WriteLine("this.@{0} = @{0};", FormalName(arg, i));

             i++;

           }

         }

@@ -232,10 +232,12 @@ namespace Microsoft.Dafny {
       }

     }

     

-    void CompileDatatypeStruct(DatatypeDecl dt, int indent) {Contract.Requires(dt != null);

+    void CompileDatatypeStruct(DatatypeDecl dt, int indent) {

+      Contract.Requires(dt != null);

+

       // public struct Dt<T> {

       //   Base_Dt<T> d;

-      //   public Base_Dt<T> D {

+      //   public Base_Dt<T> _D {

       //     get { if (d == null) { d = Default; } return d; }

       //   }

       //   public Dt(Base_Dt<T> d) { this.d = d; }

@@ -243,9 +245,9 @@ namespace Microsoft.Dafny {
       //     get { return ...; }

       //   }

       //   public override bool Equals(object other) {

-      //     return other is Dt<T> && D.Equals(((Dt<T>)other).D);

+      //     return other is Dt<T> && _D.Equals(((Dt<T>)other)._D);

       //   }

-      //   public override int GetHashCode() { return D.GetHashCode(); }

+      //   public override int GetHashCode() { return _D.GetHashCode(); }

       // }

       string DtT = dt.Name;

       if (dt.TypeArgs.Count != 0) {

@@ -253,27 +255,29 @@ namespace Microsoft.Dafny {
       }

       

       Indent(indent);

-      wr.WriteLine("public struct {0} {{", DtT);

+      wr.WriteLine("public struct @{0} {{", DtT);

       int ind = indent + IndentAmount;

       

       Indent(ind);

       wr.WriteLine("Base_{0} d;", DtT);

       

       Indent(ind);

-      wr.WriteLine("public Base_{0} D {{", DtT);

+      wr.WriteLine("public Base_{0} _D {{", DtT);

       Indent(ind + IndentAmount);

       wr.WriteLine("get { if (d == null) { d = Default; } return d; }");

       Indent(ind);  wr.WriteLine("}");

       

       Indent(ind);

-      wr.WriteLine("public {0}(Base_{1} d) {{ this.d = d; }}", dt.Name, DtT);

+      wr.WriteLine("public @{0}(Base_{1} d) {{ this.d = d; }}", dt.Name, DtT);

       

       Indent(ind);

       wr.WriteLine("public static Base_{0} Default {{", DtT);

       Indent(ind + IndentAmount);

       wr.Write("get { return ");

       wr.Write("new {0}", DtCtorName(cce.NonNull(dt.DefaultCtor)));

-      // todo: type parameters

+      if (dt.TypeArgs.Count != 0) {

+        wr.Write("<{0}>", TypeParameters(dt.TypeArgs));

+      }

       wr.Write("(");

       string sep = "";

       foreach (Formal f in dt.DefaultCtor.Formals) {

@@ -288,11 +292,11 @@ namespace Microsoft.Dafny {
 

       Indent(ind);  wr.WriteLine("public override bool Equals(object other) {");

       Indent(ind + IndentAmount);

-      wr.WriteLine("return other is {0} && D.Equals((({0})other).D);", DtT);

+      wr.WriteLine("return other is @{0} && _D.Equals(((@{0})other)._D);", DtT);

       Indent(ind);  wr.WriteLine("}");

 

       Indent(ind);

-      wr.WriteLine("public override int GetHashCode() { return D.GetHashCode(); }");

+      wr.WriteLine("public override int GetHashCode() { return _D.GetHashCode(); }");

       

       Indent(indent);

       wr.WriteLine("}");

@@ -306,7 +310,7 @@ namespace Microsoft.Dafny {
       foreach (Formal arg in formals) {

         if (!arg.IsGhost) {

           string name = FormalName(arg, i);

-          wr.Write("{0}{1}{2} {3}", sep, arg.InParam ? "" : "out ", TypeName(arg.Type), name);

+          wr.Write("{0}{1}{2} @{3}", sep, arg.InParam ? "" : "out ", TypeName(arg.Type), name);

           sep = ", ";

           i++;

         }

@@ -314,7 +318,8 @@ namespace Microsoft.Dafny {
     }

     

     string FormalName(Formal formal, int i) {

-      Contract.Requires(formal != null);Contract.Ensures(Contract.Result<string>() != null);

+      Contract.Requires(formal != null);

+      Contract.Ensures(Contract.Result<string>() != null);

 

       return formal.Name.StartsWith("#") ? "a" + i : formal.Name;

     }

@@ -333,7 +338,7 @@ namespace Microsoft.Dafny {
           Field f = (Field)member;

           if (!f.IsGhost) {

             Indent(indent);

-            wr.WriteLine("public {0} {1} = {2};", TypeName(f.Type), f.Name, DefaultValue(f.Type));

+            wr.WriteLine("public {0} @{1} = {2};", TypeName(f.Type), f.Name, DefaultValue(f.Type));

           }

           

         } else if (member is Function) {

@@ -344,7 +349,7 @@ namespace Microsoft.Dafny {
             Error("Function {0} has no body", f.FullName);

           } else {

             Indent(indent);

-            wr.Write("public {0}{1} {2}", f.IsStatic ? "static " : "", TypeName(f.ResultType), f.Name);

+            wr.Write("public {0}{1} @{2}", f.IsStatic ? "static " : "", TypeName(f.ResultType), f.Name);

             if (f.TypeArgs.Count != 0) {

               wr.Write("<{0}>", TypeParameters(f.TypeArgs));

             }

@@ -354,8 +359,8 @@ namespace Microsoft.Dafny {
             if (f.Body is MatchExpr) {

               MatchExpr me = (MatchExpr)f.Body;

               // Type source = e;

-              // if (source.D is Dt_Ctor0) {

-              //   FormalType f0 = ((Dt_Ctor0)source.D).a0;

+              // if (source._D is Dt_Ctor0) {

+              //   FormalType f0 = ((Dt_Ctor0)source._D).a0;

               //   ...

               //   return Body0;

               // } else if (...) {

@@ -397,7 +402,7 @@ namespace Microsoft.Dafny {
           Method m = (Method)member;

           if (!m.IsGhost) {

             Indent(indent);

-            wr.Write("public {0}void {1}", m.IsStatic ? "static " : "", m.Name);

+            wr.Write("public {0}void @{1}", m.IsStatic ? "static " : "", m.Name);

             if (m.TypeArgs.Count != 0) {

               wr.Write("<{0}>", TypeParameters(m.TypeArgs));

             }

@@ -412,7 +417,7 @@ namespace Microsoft.Dafny {
             foreach (Formal p in m.Outs) {

               if (!p.IsGhost) {

                 Indent(indent + IndentAmount);

-                wr.WriteLine("{0} = {1};", p.Name, DefaultValue(p.Type));

+                wr.WriteLine("@{0} = {1};", p.Name, DefaultValue(p.Type));

               }

             }

             if (m.Body == null) {

@@ -428,7 +433,7 @@ namespace Microsoft.Dafny {
               wr.WriteLine("public static void Main(string[] args) {");

               ClassDecl cl = cce.NonNull(m.EnclosingClass);

               Indent(indent + IndentAmount);

-              wr.Write("{0} b = new {0}", cl.Name);

+              wr.Write("@{0} b = new @{0}", cl.Name);

               if (cl.TypeArgs.Count != 0) {

                 // instantiate every parameter, it doesn't particularly matter how

                 wr.Write("<");

@@ -493,7 +498,7 @@ namespace Microsoft.Dafny {
         return name + "]";

       } else if (type is UserDefinedType) {

         UserDefinedType udt = (UserDefinedType)type;

-        string s = udt.Name;

+        string s = "@" + udt.Name;

         if (udt.TypeArgs.Count != 0) {

           if (Contract.Exists(udt.TypeArgs, argType =>argType is ObjectType)) {

             Error("compilation does not support type 'object' as a type parameter; consider introducing a ghost");

@@ -538,7 +543,7 @@ namespace Microsoft.Dafny {
       string s = "";

       string sep = "";

       foreach (TypeParameter tp in targs) {

-        s += sep + tp.Name;

+        s += sep + "@" + tp.Name;

         sep = ",";

       }

       return s;

@@ -569,14 +574,14 @@ namespace Microsoft.Dafny {
         return "null";

       } else if (type.IsDatatype) {

         UserDefinedType udt = (UserDefinedType)type;

-        string s = udt.Name;

+        string s = "@" + udt.Name;

         if (udt.TypeArgs.Count != 0) {

           s += "<" + TypeNames(udt.TypeArgs) + ">";

         }

-        return s + ".Default";

+        return string.Format("new {0}({0}.Default)", s);

       } else if (type.IsTypeParameter) {

         UserDefinedType udt = (UserDefinedType)type;

-        return "default(" + udt.Name + ")";

+        return "default(@" + udt.Name + ")";

       } else if (type is SetType) {

         return DafnySetClass + "<" + TypeName(((SetType)type).Arg) + ">.Empty";

       } else if (type is SeqType) {

@@ -667,12 +672,10 @@ namespace Microsoft.Dafny {
             string nw = "_nw" + tmpVarCount;

             tmpVarCount++;

             Indent(indent);

-            wr.Write("{0} = ", nw);

+            wr.Write("var {0} = ", nw);

             TrAssignmentRhs(s.Rhs);

             wr.WriteLine(";");

-            Indent(indent);

             TrCallStmt(tRhs.InitCall, nw, indent);

-            wr.WriteLine(";");

             Indent(indent);

             TrExpr(s.Lhs);

             wr.WriteLine(" = {0};", nw);

@@ -709,7 +712,7 @@ namespace Microsoft.Dafny {
         }

         

         TrStmt(s.Thn, indent);

-        if (s.Els != null) {

+        if (s.Els != null && s.Guard != null) {

           Indent(indent);  wr.WriteLine("else");

           TrStmt(s.Els, indent);

         }

@@ -749,7 +752,7 @@ namespace Microsoft.Dafny {
         wr.WriteLine("List<Pair<{0},{1}>> {2} = new List<Pair<{0},{1}>>();", TType, RhsType, pu);

         

         Indent(indent);

-        wr.Write("foreach ({0} {1} in (", TType, s.BoundVar.Name);

+        wr.Write("foreach ({0} @{1} in (", TType, s.BoundVar.Name);

         TrExpr(s.Collection);

         wr.WriteLine(").Elements) {");

         

@@ -762,7 +765,7 @@ namespace Microsoft.Dafny {
           TrStmt(p, indent + 2*IndentAmount);

         }

         Indent(indent + 2*IndentAmount);

-        wr.Write("{0}.Add(new Pair<{1},{2}>({3}, ", pu, TType, RhsType, s.BoundVar.Name);

+        wr.Write("{0}.Add(new Pair<{1},{2}>(@{3}, ", pu, TType, RhsType, s.BoundVar.Name);

         ExprRhs rhsExpr = s.BodyAssign.Rhs as ExprRhs;

         if (rhsExpr != null) {

           TrExpr(rhsExpr.Expr);

@@ -783,8 +786,8 @@ namespace Microsoft.Dafny {
       } else if (stmt is MatchStmt) {

         MatchStmt s = (MatchStmt)stmt;

         // Type source = e;

-        // if (source.D is Dt_Ctor0) {

-        //   FormalType f0 = ((Dt_Ctor0)source.D).a0;

+        // if (source._D is Dt_Ctor0) {

+        //   FormalType f0 = ((Dt_Ctor0)source._D).a0;

         //   ...

         //   Body0;

         // } else if (...) {

@@ -823,13 +826,13 @@ namespace Microsoft.Dafny {
       Contract.Assert(s.Method != null);  // follows from the fact that stmt has been successfully resolved

       Indent(indent);

       if (receiverReplacement != null) {

-        wr.Write(receiverReplacement);

+        wr.Write("@" + receiverReplacement);

       } else if (s.Method.IsStatic) {

         wr.Write(TypeName(cce.NonNull(s.Receiver.Type)));

       } else {

         TrParenExpr(s.Receiver);

       }

-      wr.Write(".{0}(", s.Method.Name);

+      wr.Write(".@{0}(", s.Method.Name);

 

       string sep = "";

       for (int i = 0; i < s.Method.Ins.Count; i++) {

@@ -921,8 +924,13 @@ namespace Microsoft.Dafny {
 

     void TrVarDecl(VarDecl s, bool alwaysInitialize, int indent) {

       Contract.Requires(s != null);

+      if (s.IsGhost) {

+        // only emit non-ghosts (we get here only for local variables introduced implicitly by call statements)

+        return;

+      }

+

       Indent(indent);

-      wr.Write("{0} {1}", TypeName(s.Type), s.Name);

+      wr.Write("{0} @{1}", TypeName(s.Type), s.Name);

       if (s.Rhs != null) {

         wr.Write(" = ");

         TrAssignmentRhs(s.Rhs);

@@ -943,15 +951,15 @@ namespace Microsoft.Dafny {
       Contract.Requires(source != null);

       Contract.Requires(ctor != null);

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

-      // if (source.D is Dt_Ctor0) {

-      //   FormalType f0 = ((Dt_Ctor0)source.D).a0;

+      // if (source._D is Dt_Ctor0) {

+      //   FormalType f0 = ((Dt_Ctor0)source._D).a0;

       //   ...

       Indent(indent);

       wr.Write("{0}if (", caseIndex == 0 ? "" : "} else ");

       if (caseIndex == caseCount - 1) {

         wr.Write("true");

       } else {

-        wr.Write("{0}.D is {1}", source, DtCtorName(ctor));

+        wr.Write("{0}._D is {1}", source, DtCtorName(ctor));

       }

       wr.WriteLine(") {");

 

@@ -960,9 +968,9 @@ namespace Microsoft.Dafny {
         Formal arg = ctor.Formals[m];

         if (!arg.IsGhost) {

           BoundVar bv = arguments[m];

-          // FormalType f0 = ((Dt_Ctor0)source.D).a0;

+          // FormalType f0 = ((Dt_Ctor0)source._D).a0;

           Indent(indent + IndentAmount);

-          wr.WriteLine("{0} {1} = (({2}){3}.D).{4};",

+          wr.WriteLine("{0} @{1} = (({2}){3}._D).@{4};",

             TypeName(bv.Type), bv.Name, DtCtorName(ctor), source, FormalName(arg, k));

           k++;

         }

@@ -1022,7 +1030,7 @@ namespace Microsoft.Dafny {
         

       } else if (expr is IdentifierExpr) {

         IdentifierExpr e = (IdentifierExpr)expr;

-        wr.Write(cce.NonNull(e.Var).Name);

+        wr.Write("@" + e.Var.Name);

       

       } else if (expr is SetDisplayExpr) {

         SetDisplayExpr e = (SetDisplayExpr)expr;

@@ -1050,7 +1058,7 @@ namespace Microsoft.Dafny {
           }

         } else {

           TrParenExpr(e.Obj);

-          wr.Write(".{0}", e.Field.Name);

+          wr.Write(".@{0}", e.Field.Name);

         }

         

       } else if (expr is SeqSelectExpr) {

@@ -1103,7 +1111,7 @@ namespace Microsoft.Dafny {
         } else {

           TrParenExpr(e.Receiver);

         }

-        wr.Write(".{0}", f.Name);

+        wr.Write(".@{0}", f.Name);

         wr.Write("(");

         string sep = "";

         for (int i = 0; i < e.Args.Count; i++) {

@@ -1325,7 +1333,7 @@ namespace Microsoft.Dafny {
             Contract.Assert(false); throw new cce.UnreachableException();  // unexpected BoundedPool type

           }

           wr.Write("{0}, ", expr is ForallExpr ? "true" : "false");

-          wr.Write("{0} => ", bv.Name);

+          wr.Write("@{0} => ", bv.Name);

         }

         TrExpr(e.Body);

         for (int i = 0; i < n; i++) {

diff --git a/Test/VSComp2010/runtest.bat b/Test/VSComp2010/runtest.bat
index e39abe7d..e16eda13 100644
--- a/Test/VSComp2010/runtest.bat
+++ b/Test/VSComp2010/runtest.bat
@@ -4,7 +4,7 @@ setlocal
 set BOOGIEDIR=..\..\Binaries

 set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe

 set BPLEXE=%BOOGIEDIR%\Boogie.exe

-

+set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe

 

 for %%f in (Problem1-SumMax.dfy Problem2-Invert.dfy

             Problem3-FindZero.dfy Problem4-Queens.dfy

@@ -12,4 +12,6 @@ for %%f in (Problem1-SumMax.dfy Problem2-Invert.dfy
   echo.

   echo -------------------- %%f --------------------

   %DAFNY_EXE% %* %%f

+

+  IF NOT "%COMPILEDAFNY%"=="" %CSC% /nologo /debug /t:library /out:out.dll /r:System.Numerics.dll out.cs

 )

diff --git a/Test/VSI-Benchmarks/runtest.bat b/Test/VSI-Benchmarks/runtest.bat
index 0cd898c4..a733a1c0 100644
--- a/Test/VSI-Benchmarks/runtest.bat
+++ b/Test/VSI-Benchmarks/runtest.bat
@@ -4,12 +4,16 @@ setlocal
 set BOOGIEDIR=..\..\Binaries

 set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe

 set BPLEXE=%BOOGIEDIR%\Boogie.exe

+set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe

 

-

-

-for %%f in ( b1.dfy b2.dfy b3.dfy b4.dfy b5.dfy b6.dfy b7.dfy

-             b8.dfy ) do (

+for %%f in (b1.dfy b2.dfy b3.dfy b4.dfy b5.dfy b6.dfy b7.dfy b8.dfy) do (

   echo.

   echo -------------------- %%f --------------------

-  %DAFNY_EXE% /compile:0 %* %%f

+

+  REM The following line will just run the verifier

+  IF "%COMPILEDAFNY%"=="" %DAFNY_EXE% /compile:0 %* %%f

+

+  REM Alternatively, the following lines also produce C# code and compile it

+  IF NOT "%COMPILEDAFNY%"=="" %DAFNY_EXE% %* %%f

+  IF NOT "%COMPILEDAFNY%"=="" %CSC% /nologo /debug /t:library /out:out.dll /r:System.Numerics.dll out.cs

 )

diff --git a/Test/dafny1/runtest.bat b/Test/dafny1/runtest.bat
index b6fc7f62..36b93883 100644
--- a/Test/dafny1/runtest.bat
+++ b/Test/dafny1/runtest.bat
@@ -4,6 +4,7 @@ setlocal
 set BOOGIEDIR=..\..\Binaries

 set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe

 set BPLEXE=%BOOGIEDIR%\Boogie.exe

+set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe

 

 for %%f in (BQueue.bpl) do (

   echo.

@@ -25,5 +26,11 @@ for %%f in (Queue.dfy PriorityQueue.dfy ExtensibleArray.dfy
             UltraFilter.dfy) do (

   echo.

   echo -------------------- %%f --------------------

-  %DAFNY_EXE% /compile:0 %* %%f

+

+  REM The following line will just run the verifier

+  IF "%COMPILEDAFNY%"=="" %DAFNY_EXE% /compile:0 %* %%f

+

+  REM Alternatively, the following lines also produce C# code and compile it

+  IF NOT "%COMPILEDAFNY%"=="" %DAFNY_EXE% %* %%f

+  IF NOT "%COMPILEDAFNY%"=="" %CSC% /nologo /debug /t:library /out:out.dll /r:System.Numerics.dll out.cs

 )

diff --git a/Test/vacid0/runtest.bat b/Test/vacid0/runtest.bat
index d6af7b71..32c6a984 100644
--- a/Test/vacid0/runtest.bat
+++ b/Test/vacid0/runtest.bat
@@ -4,9 +4,16 @@ setlocal
 set BOOGIEDIR=..\..\Binaries

 set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe

 set BPLEXE=%BOOGIEDIR%\Boogie.exe

+set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe

 

 for %%f in (LazyInitArray.dfy SparseArray.dfy Composite.dfy) do (

   echo.

   echo -------------------- %%f --------------------

-  %DAFNY_EXE% /compile:0 %* %%f

+

+  REM The following line will just run the verifier

+  IF "%COMPILEDAFNY%"=="" %DAFNY_EXE% /compile:0 %* %%f

+

+  REM Alternatively, the following lines also produce C# code and compile it

+  IF NOT "%COMPILEDAFNY%"=="" %DAFNY_EXE% %* %%f

+  IF NOT "%COMPILEDAFNY%"=="" %CSC% /nologo /debug /t:library /out:out.dll /r:System.Numerics.dll out.cs

 )