Merge

18 files changed, 753 insertions, 376 deletions

diff --git a/.hgtags b/.hgtags
index e69de29b..6e2337a0 100644
--- a/.hgtags
+++ b/.hgtags
@@ -0,0 +1,2 @@
+42ab6e4ab0b1f5e66b0d142df0df98c9495414f5 emicvccbld_build_2.1.30608.0
+7dffe3976b9dcd1153c2b03e5a3d04278eee1633 emicvccbld_build_2.1.30608.1
diff --git a/BCT/BytecodeTranslator/CLRSemantics.cs b/BCT/BytecodeTranslator/CLRSemantics.cs
index b0749e6c..e08da536 100644
--- a/BCT/BytecodeTranslator/CLRSemantics.cs
+++ b/BCT/BytecodeTranslator/CLRSemantics.cs
@@ -24,11 +24,13 @@ namespace BytecodeTranslator {
       return new CLRExpressionSemantics(sink, statementTraverser, contractContext);

     }

 

+

     public class CLRExpressionSemantics : ExpressionTraverser {

 

       public CLRExpressionSemantics(Sink sink, StatementTraverser/*?*/ statementTraverser, bool contractContext)

         : base(sink, statementTraverser, contractContext) { }

 

+      /*

       public override void Visit(IDivision division) {

         this.Visit(division.LeftOperand);

         this.Visit(division.RightOperand);

@@ -42,11 +44,13 @@ namespace BytecodeTranslator {
         var storeLocal = Bpl.Cmd.SimpleAssign(tok, locExpr, rexp);

         this.StmtTraverser.StmtBuilder.Add(storeLocal);

 

-        var a = new Bpl.AssertCmd(tok, Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, locExpr, Bpl.Expr.Literal(0)));

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

+//        Assertion fails if denominator is Real or something else than int

+//        var a = new Bpl.AssertCmd(tok, Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, locExpr, Bpl.Expr.Literal(0)));

+//        this.StmtTraverser.StmtBuilder.Add(a);

 

         TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Div, lexp, locExpr));

       }

+       * */

     }

   }

 }
\ No newline at end of file
diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index 1dc02c74..a0487567 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -104,6 +104,11 @@ namespace BytecodeTranslator
         this.Visit(addressDereference);

         return;

       }

+      IBlockExpression block = addressableExpression.Definition as IBlockExpression;

+      if (block != null) {

+        this.Visit(block);

+        return;

+      }

       IMethodReference/*?*/ method = addressableExpression.Definition as IMethodReference;

       if (method != null)

       {

@@ -286,16 +291,6 @@ namespace BytecodeTranslator
     public override void Visit(IAddressOf addressOf)

     {

       Visit(addressOf.Expression);

-      //if (addressOf.Expression.Type.IsValueType)

-      //{

-      //  var e = this.TranslatedExpressions.Pop();

-      //  var callBox = new Bpl.NAryExpr(

-      //    addressOf.Token(),

-      //  new Bpl.FunctionCall(this.sink.Heap.Struct2Ref),

-      //  new Bpl.ExprSeq(e)

-      //  );

-      //  TranslatedExpressions.Push(callBox);

-      //}

     }

     #endregion

 

@@ -333,14 +328,18 @@ namespace BytecodeTranslator
           }

           break;

         case PrimitiveTypeCode.Char: // chars are represented as ints

-        case PrimitiveTypeCode.Int16:

-        case PrimitiveTypeCode.Int32:

-        case PrimitiveTypeCode.Int64:

         case PrimitiveTypeCode.Int8:

-          var lit = Bpl.Expr.Literal((int)constant.Value);

+        case PrimitiveTypeCode.Int16:

+          var lit = Bpl.Expr.Literal((short)constant.Value);

           lit.Type = Bpl.Type.Int;

           TranslatedExpressions.Push(lit);

           break;

+        case PrimitiveTypeCode.Int32:

+        case PrimitiveTypeCode.Int64:

+          var lit2 = Bpl.Expr.Literal((int)constant.Value);

+          lit2.Type = Bpl.Type.Int;

+          TranslatedExpressions.Push(lit2);

+          break;

         case PrimitiveTypeCode.UInt16:

         case PrimitiveTypeCode.UInt32:

         case PrimitiveTypeCode.UInt64:

@@ -481,11 +480,6 @@ namespace BytecodeTranslator
         // So this code is the same as Visit(ICreateObjectInstance)

         // TODO: factor the code into a single method?

 

-        var addrOf = methodCall.ThisArgument as IAddressOf;

-        var ae = addrOf.Expression as IAddressableExpression;

-        var local = ae.Definition as ILocalDefinition;

-        var s = this.sink.CreateFreshLocal(local.Type);

-

         // First generate an Alloc() call

         this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(methodCallToken, this.sink.AllocationMethodName, new Bpl.ExprSeq(), new Bpl.IdentifierExprSeq(thisExpr)));

 

@@ -497,7 +491,7 @@ namespace BytecodeTranslator
             new Bpl.AssumeCmd(methodCallToken,

               Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq,

               this.sink.Heap.DynamicType(thisExpr),

-              this.sink.FindOrCreateType(resolvedMethod.ContainingTypeDefinition)

+              this.sink.FindOrCreateType(methodCall.MethodToCall.ResolvedMethod.ContainingTypeDefinition)

               )

               )

             );

@@ -527,7 +521,7 @@ namespace BytecodeTranslator
         }

 

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

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

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

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

         call = new Bpl.CallCmd(methodCallToken, methodName, inexpr, outvars);

         this.StmtTraverser.StmtBuilder.Add(call);

@@ -561,6 +555,8 @@ namespace BytecodeTranslator
         this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(kv.Key, this.sink.Heap.Unbox(Bpl.Token.NoToken, kv.Key.Type, kv.Value)));

       }

 

+      Bpl.Expr expr = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, Bpl.Expr.Ident(this.sink.Heap.ExceptionVariable), Bpl.Expr.Ident(this.sink.Heap.NullRef));

+      this.StmtTraverser.RaiseException(expr);

     }

 

     // REVIEW: Does "thisExpr" really need to come back as an identifier? Can't it be a general expression?

@@ -629,9 +625,8 @@ namespace BytecodeTranslator
         }

       }

 

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

-      

-      var translateAsFunctionCall = proc is Bpl.Function;

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

+      var translateAsFunctionCall = procInfo.Decl is Bpl.Function;

       if (!translateAsFunctionCall) {

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

           Bpl.Variable v = this.sink.CreateFreshLocal(methodToCall.ResolvedMethod.Type.ResolvedType);

@@ -647,7 +642,7 @@ namespace BytecodeTranslator
         }

       }

 

-      return proc;

+      return procInfo.Decl;

     }

 

     #endregion

@@ -723,23 +718,14 @@ namespace BytecodeTranslator
         if (instance == null) {

           // static fields are not kept in the heap

           StmtTraverser.StmtBuilder.Add(Bpl.Cmd.SimpleAssign(tok, f, e));

-        } else {

-          if (false && field.ContainingType.ResolvedType.IsStruct) {

-            //var s_prime = this.sink.CreateFreshLocal(this.sink.Heap.StructType);

-            //var s_prime_expr = Bpl.Expr.Ident(s_prime);

-            //var boogieType = sink.CciTypeToBoogie(field.Type);

-            //StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(tok, s_prime_expr, f, e,

-            //  field.ResolvedField.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap,

-            //  boogieType));

-            UpdateStruct(tok, instance, field, e);

-          } else {

-            this.Visit(instance);

-            var x = this.TranslatedExpressions.Pop();

-            var boogieType = sink.CciTypeToBoogie(field.Type);

-            StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(tok, x, f, e,

-              field.ResolvedField.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap,

-              boogieType));

-          }

+        }

+        else {

+          this.Visit(instance);

+          var x = this.TranslatedExpressions.Pop();

+          var boogieType = sink.CciTypeToBoogie(field.Type);

+          StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(tok, x, f, e,

+            field.ResolvedField.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap,

+            boogieType));

         }

         return;

       }

@@ -772,6 +758,11 @@ namespace BytecodeTranslator
             TranslateAssignment(tok, be.Definition, be.Instance, source);

             return;

           }

+          var ao = popValue as IAddressOf;

+          if (ao != null) {

+            TranslateAssignment(tok, ao.Expression.Definition, ao.Expression.Instance, source);

+            return;

+          }

         }

         var be2 = addressDereference.Address as IBoundExpression;

         if (be2 != null) {

@@ -795,34 +786,7 @@ namespace BytecodeTranslator
 

       Contract.Assume(false);

     }

-

-    private void UpdateStruct(Bpl.IToken tok, IExpression iExpression, IFieldReference field, Bpl.Expr e) {

-      var addrOf = iExpression as IAddressOf;

-      if (addrOf == null) return;

-      var addressableExpression = addrOf.Expression as IAddressableExpression;

-      if (addressableExpression == null) return;

-

-      var f = Bpl.Expr.Ident(this.sink.FindOrCreateFieldVariable(field));

-

-      if (addressableExpression.Instance == null) {

-        var boogieType = sink.CciTypeToBoogie(field.Type);

-        this.Visit(addressableExpression);

-        var def = this.TranslatedExpressions.Pop();

-        StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(tok, def, f, e,

-          AccessType.Struct,

-          boogieType));

-      } else {

-        var s_prime = this.sink.CreateFreshLocal(this.sink.Heap.StructType);

-        var s_prime_expr = Bpl.Expr.Ident(s_prime);

-        var boogieType = sink.CciTypeToBoogie(field.Type);

-        StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(tok, s_prime_expr, f, e,

-          AccessType.Struct,

-          boogieType));

-        UpdateStruct(tok, addressableExpression.Instance, addressableExpression.Definition as IFieldReference, s_prime_expr);

-      }

-    }

-

-

+    

     #endregion

 

     #region Translate Object Creation

@@ -1053,7 +1017,23 @@ namespace BytecodeTranslator
       base.Visit(greaterThan);

       Bpl.Expr rexp = TranslatedExpressions.Pop();

       Bpl.Expr lexp = TranslatedExpressions.Pop();

-      TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Gt, lexp, rexp));

+

+      Bpl.Expr e;

+      switch (greaterThan.LeftOperand.Type.TypeCode) {

+        case PrimitiveTypeCode.Float32:

+        case PrimitiveTypeCode.Float64:

+          e = new Bpl.NAryExpr(

+            greaterThan.Token(),

+            new Bpl.FunctionCall(this.sink.Heap.RealGreaterThan),

+            new Bpl.ExprSeq(lexp, rexp)

+            );

+          break;

+        default:

+          e = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Gt, lexp, rexp);

+          break;

+      }

+

+      TranslatedExpressions.Push(e);

     }

 

     public override void Visit(IGreaterThanOrEqual greaterEqual)

@@ -1061,7 +1041,23 @@ namespace BytecodeTranslator
       base.Visit(greaterEqual);

       Bpl.Expr rexp = TranslatedExpressions.Pop();

       Bpl.Expr lexp = TranslatedExpressions.Pop();

-      TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Ge, lexp, rexp));

+

+      Bpl.Expr e;

+      switch (greaterEqual.LeftOperand.Type.TypeCode) {

+        case PrimitiveTypeCode.Float32:

+        case PrimitiveTypeCode.Float64:

+          e = new Bpl.NAryExpr(

+            greaterEqual.Token(),

+            new Bpl.FunctionCall(this.sink.Heap.RealGreaterThanOrEqual),

+            new Bpl.ExprSeq(lexp, rexp)

+            );

+          break;

+        default:

+          e = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Ge, lexp, rexp);

+          break;

+      } 

+      

+      TranslatedExpressions.Push(e);

     }

 

     public override void Visit(ILessThan lessThan)

@@ -1069,7 +1065,23 @@ namespace BytecodeTranslator
       base.Visit(lessThan);

       Bpl.Expr rexp = TranslatedExpressions.Pop();

       Bpl.Expr lexp = TranslatedExpressions.Pop();

-      TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Lt, lexp, rexp));

+

+      Bpl.Expr e;

+      switch (lessThan.LeftOperand.Type.TypeCode) {

+        case PrimitiveTypeCode.Float32:

+        case PrimitiveTypeCode.Float64:

+          e = new Bpl.NAryExpr(

+            lessThan.Token(),

+            new Bpl.FunctionCall(this.sink.Heap.RealLessThan),

+            new Bpl.ExprSeq(lexp, rexp)

+            );

+          break;

+        default:

+          e = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Lt, lexp, rexp);

+          break;

+      }

+

+      TranslatedExpressions.Push(e);

     }

 

     public override void Visit(ILessThanOrEqual lessEqual)

@@ -1077,7 +1089,23 @@ namespace BytecodeTranslator
       base.Visit(lessEqual);

       Bpl.Expr rexp = TranslatedExpressions.Pop();

       Bpl.Expr lexp = TranslatedExpressions.Pop();

-      TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Le, lexp, rexp));

+

+      Bpl.Expr e;

+      switch (lessEqual.LeftOperand.Type.TypeCode) {

+        case PrimitiveTypeCode.Float32:

+        case PrimitiveTypeCode.Float64:

+          e = new Bpl.NAryExpr(

+            lessEqual.Token(),

+            new Bpl.FunctionCall(this.sink.Heap.RealLessThanOrEqual),

+            new Bpl.ExprSeq(lexp, rexp)

+            );

+          break;

+        default:

+          e = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Le, lexp, rexp);

+          break;

+      }

+

+      TranslatedExpressions.Push(e);

     }

 

     public override void Visit(IEquality equal)

@@ -1314,7 +1342,7 @@ namespace BytecodeTranslator
               func = this.sink.Heap.Int2Ref;

           } else if (conversion.ValueToConvert.Type.TypeCode == PrimitiveTypeCode.NotPrimitive) {

             // REVIEW: Do we need to check to make sure that conversion.ValueToConvert.Type.IsValueType?

-            func = this.sink.Heap.Struct2Ref;

+            func = this.sink.Heap.Box2Ref;

           } else if (conversion.ValueToConvert.Type.TypeCode == PrimitiveTypeCode.Float32 ||

             conversion.ValueToConvert.Type.TypeCode == PrimitiveTypeCode.Float64) {

               func = this.sink.Heap.Real2Ref;

@@ -1375,14 +1403,39 @@ namespace BytecodeTranslator
     {

       base.Visit(unaryNegation);

       Bpl.Expr exp = TranslatedExpressions.Pop();

-      Bpl.Expr zero = Bpl.Expr.Literal(0); // TODO: (mschaef) will this work in any case?

-      TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Sub, zero, exp));

+      Bpl.Expr e, zero, realZero;

+      zero = Bpl.Expr.Literal(0);

+      realZero = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.sink.Heap.Int2Real), new Bpl.ExprSeq(zero));

+      switch (unaryNegation.Type.TypeCode) {

+        case PrimitiveTypeCode.Float32:

+        case PrimitiveTypeCode.Float64:

+          e = new Bpl.NAryExpr(

+            unaryNegation.Token(),

+            new Bpl.FunctionCall(this.sink.Heap.RealMinus),

+            new Bpl.ExprSeq(realZero, exp)

+            );

+          break;

+        default:

+          e = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Sub, Bpl.Expr.Literal(0), exp);

+          break;

+      }

+      TranslatedExpressions.Push(e);

     }

 

     public override void Visit(ILogicalNot logicalNot)

     {

       base.Visit(logicalNot.Operand);

       Bpl.Expr exp = TranslatedExpressions.Pop();

+      Bpl.Type operandType = this.sink.CciTypeToBoogie(logicalNot.Operand.Type);

+      if (operandType == this.sink.Heap.RefType) {

+        exp = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, exp, Bpl.Expr.Ident(this.sink.Heap.NullRef));

+      }

+      else if (operandType == Bpl.Type.Int) {

+        exp = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, exp, Bpl.Expr.Literal(0));

+      }

+      else {

+        //System.Diagnostics.Debug.Assert(operandType == Bpl.Type.Bool);

+      }

       TranslatedExpressions.Push(Bpl.Expr.Unary(

           logicalNot.Token(),

           Bpl.UnaryOperator.Opcode.Not, exp));

@@ -1416,12 +1469,12 @@ namespace BytecodeTranslator
 

     public override void Visit(IReturnValue returnValue)

     {

-      if (this.sink.RetVariable == null)

+      if (this.sink.ReturnVariable == null)

       {

         throw new TranslationException(String.Format("Don't know what to do with return value {0}", returnValue.ToString()));

       }

       TranslatedExpressions.Push(new Bpl.IdentifierExpr(returnValue.Token(),

-        this.sink.RetVariable));

+        this.sink.ReturnVariable));

 

     }

     #endregion

diff --git a/BCT/BytecodeTranslator/Heap.cs b/BCT/BytecodeTranslator/Heap.cs
index 8da78bca..74121074 100644
--- a/BCT/BytecodeTranslator/Heap.cs
+++ b/BCT/BytecodeTranslator/Heap.cs
@@ -32,67 +32,15 @@ namespace BytecodeTranslator {
     /// <summary>

     /// Prelude text for which access to the ASTs is not needed

     /// </summary>

-    private readonly string InitialPreludeText =

-      @"type Struct = [Field]Box;

-type HeapType = [Ref,Field]Box;

-var $Heap: HeapType;

-

-var $Alloc: [Ref] bool;

-procedure {:inline 1} Alloc() returns (x: Ref)

-  modifies $Alloc;

-{

-  assume $Alloc[x] == false && x != null;

-  $Alloc[x] := true;

-}

-

-//axiom (forall x : Field :: $DefaultStruct[x] == $DefaultBox);

-axiom Box2Int($DefaultBox) == 0;

-axiom Box2Bool($DefaultBox) == false;

-axiom Box2Ref($DefaultBox) == null;

-//axiom Box2Struct($DefaultBox) == $DefaultStruct;

-

-axiom (forall x: int :: { Int2Box(x) } Box2Int(Int2Box(x)) == x );

-axiom (forall x: bool :: { Bool2Box(x) } Box2Bool(Bool2Box(x)) == x );

-axiom (forall x: Ref :: { Ref2Box(x) } Box2Ref(Ref2Box(x)) == x );

-axiom (forall x: Struct :: { Struct2Box(x) } Box2Struct(Struct2Box(x)) == x );

-

-procedure {:inline 1} System.Object.GetType(this: Ref) returns ($result: Ref)

-{

-  $result := $TypeOf($DynamicType(this));

-}

-function $TypeOfInv(Ref): Type;

-axiom (forall t: Type :: {$TypeOf(t)} $TypeOfInv($TypeOf(t)) == t);

-

-function $ThreadDelegate(Ref) : Ref;

-

-procedure {:inline 1} System.Threading.Thread.#ctor$System.Threading.ParameterizedThreadStart(this: Ref, start$in: Ref)

-{

-  assume $ThreadDelegate(this) == start$in;

-}

-procedure {:inline 1} System.Threading.Thread.Start$System.Object(this: Ref, parameter$in: Ref)

-{

-  call {:async} System.Threading.ParameterizedThreadStart.Invoke$System.Object($ThreadDelegate(this), parameter$in);

-}

-procedure {:extern} System.Threading.ParameterizedThreadStart.Invoke$System.Object(this: Ref, obj$in: Ref);

-

-procedure {:inline 1} System.Threading.Thread.#ctor$System.Threading.ThreadStart(this: Ref, start$in: Ref) 

-{

-  assume $ThreadDelegate(this) == start$in;

-}

-procedure {:inline 1} System.Threading.Thread.Start(this: Ref) 

-{

-  call {:async} System.Threading.ThreadStart.Invoke($ThreadDelegate(this));

-}

-procedure {:extern} System.Threading.ThreadStart.Invoke(this: Ref);

+    private readonly string InitialPreludeText = @"";

 

-";

     private Sink sink;

 

     public override bool MakeHeap(Sink sink, out Heap heap, out Bpl.Program/*?*/ program) {

       heap = this;

       program = null;

       this.sink = sink;

-      string prelude = this.InitialPreludeText + this.DelegateEncodingText;

+      string prelude = this.InitialPreludeText + this.CommonText;

       var b = RepresentationFor.ParsePrelude(prelude, this, out program);

       if (b) {

         this.BoxType = new Bpl.CtorType(this.BoxTypeDecl.tok, this.BoxTypeDecl, new Bpl.TypeSeq());

@@ -201,57 +149,8 @@ procedure {:extern} System.Threading.ThreadStart.Invoke(this: Ref);
     /// Prelude text for which access to the ASTs is not needed

     /// </summary>

     private readonly string InitialPreludeText =

-      @"//type Struct = [Field]Box;

-type Struct = Ref;

-type HeapType = [Ref][Field]Box;

-

-var $Alloc: [Ref] bool;

-procedure {:inline 1} Alloc() returns (x: Ref)

-  modifies $Alloc;

-{

-  assume $Alloc[x] == false && x != null;

-  $Alloc[x] := true;

-}

-

-//axiom (forall x : Field :: $DefaultStruct[x] == $DefaultBox);

-//axiom (forall h : HeapType, f : Field :: { Read(h, $DefaultStruct, f) } Read(h, $DefaultStruct, f) == $DefaultBox);

-axiom Box2Int($DefaultBox) == 0;

-axiom Box2Bool($DefaultBox) == false;

-axiom Box2Ref($DefaultBox) == null;

-//axiom Box2Struct($DefaultBox) == $DefaultStruct;

-

-axiom (forall x: int :: { Int2Box(x) } Box2Int(Int2Box(x)) == x );

-axiom (forall x: bool :: { Bool2Box(x) } Box2Bool(Bool2Box(x)) == x );

-axiom (forall x: Ref :: { Ref2Box(x) } Box2Ref(Ref2Box(x)) == x );

-axiom (forall x: Struct :: { Struct2Box(x) } Box2Struct(Struct2Box(x)) == x );

-

-procedure {:inline 1} System.Object.GetType(this: Ref) returns ($result: Ref)

-{

-  $result := $TypeOf($DynamicType(this));

-}

-function $TypeOfInv(Ref): Type;

-axiom (forall t: Type :: {$TypeOf(t)} $TypeOfInv($TypeOf(t)) == t);

-

-function $ThreadDelegate(Ref) : Ref;

-procedure {:inline 1} System.Threading.Thread.#ctor$System.Threading.ParameterizedThreadStart(this: Ref, start$in: Ref)

-{

-  assume $ThreadDelegate(this) == start$in;

-}

-procedure {:inline 1} System.Threading.Thread.Start$System.Object(this: Ref, parameter$in: Ref)

-{

-  call {:async} System.Threading.ParameterizedThreadStart.Invoke$System.Object($ThreadDelegate(this), parameter$in);

-}

-procedure {:extern} System.Threading.ParameterizedThreadStart.Invoke$System.Object(this: Ref, obj$in: Ref);

-

-procedure {:inline 1} System.Threading.Thread.#ctor$System.Threading.ThreadStart(this: Ref, start$in: Ref) 

-{

-  assume $ThreadDelegate(this) == start$in;

-}

-procedure {:inline 1} System.Threading.Thread.Start(this: Ref) 

-{

-  call {:async} System.Threading.ThreadStart.Invoke($ThreadDelegate(this));

-}

-procedure {:extern} System.Threading.ThreadStart.Invoke(this: Ref);

+      @"type HeapType = [Ref][Field]Box;

+

 ";

     private Sink sink;

 

@@ -261,7 +160,7 @@ procedure {:extern} System.Threading.ThreadStart.Invoke(this: Ref);
       this.sink = sink;

       heap = this;

       program = null;

-      string prelude = this.InitialPreludeText + this.DelegateEncodingText;

+      string prelude = this.InitialPreludeText + this.CommonText;

       var b = RepresentationFor.ParsePrelude(prelude, this, out program);

       if (b) {

         this.BoxType = new Bpl.CtorType(this.BoxTypeDecl.tok, this.BoxTypeDecl, new Bpl.TypeSeq());

diff --git a/BCT/BytecodeTranslator/HeapFactory.cs b/BCT/BytecodeTranslator/HeapFactory.cs
index df38ac15..759f7b31 100644
--- a/BCT/BytecodeTranslator/HeapFactory.cs
+++ b/BCT/BytecodeTranslator/HeapFactory.cs
@@ -96,18 +96,6 @@ namespace BytecodeTranslator {
     public Bpl.TypeCtorDecl TypeTypeDecl = null;

     public Bpl.CtorType TypeType;

 

-    private Bpl.Type structType = null;

-    public Bpl.Type StructType {

-      get {

-        if (structType == null) {

-          structType = new Bpl.MapType(Bpl.Token.NoToken, new Bpl.TypeVariableSeq(), new Bpl.TypeSeq(FieldType), BoxType);

-        }

-        return structType;

-      }

-    }

-    [RepresentationFor("$DefaultStruct", "const unique $DefaultStruct : [Field]Box;")]

-    public Bpl.Constant DefaultStruct;

-

     [RepresentationFor("Real", "type Real;")]

     protected Bpl.TypeCtorDecl RealTypeDecl = null;

     public Bpl.CtorType RealType;

@@ -126,9 +114,6 @@ namespace BytecodeTranslator {
     [RepresentationFor("Box2Bool", "function Box2Bool(Box): bool;")]

     public Bpl.Function Box2Bool = null;

 

-    [RepresentationFor("Box2Struct", "function Box2Struct(Box): Struct;")]

-    public Bpl.Function Box2Struct = null;

-

     [RepresentationFor("Box2Ref", "function Box2Ref(Box): Ref;")]

     public Bpl.Function Box2Ref = null;

 

@@ -141,9 +126,6 @@ namespace BytecodeTranslator {
     [RepresentationFor("Bool2Box", "function Bool2Box(bool): Box;")]

     public Bpl.Function Bool2Box = null;

 

-    [RepresentationFor("Struct2Box", "function Struct2Box(Struct): Box;")]

-    public Bpl.Function Struct2Box = null;

-

     [RepresentationFor("Ref2Box", "function Ref2Box(Ref): Box;")]

     public Bpl.Function Ref2Box = null;

 

@@ -159,8 +141,6 @@ namespace BytecodeTranslator {
         conversion = this.Bool2Box;

       else if (boogieType == Bpl.Type.Int)

         conversion = this.Int2Box;

-      else if (boogieType == StructType)

-        conversion = this.Struct2Box;

       else if (boogieType == RefType)

         conversion = this.Ref2Box;

       else if (boogieType == RealType)

@@ -184,8 +164,6 @@ namespace BytecodeTranslator {
         conversion = this.Box2Bool;

       else if (boogieType == Bpl.Type.Int)

         conversion = this.Box2Int;

-      else if (boogieType == StructType)

-        conversion = this.Box2Struct;

       else if (boogieType == RefType)

         conversion = this.Box2Ref;

       else if (boogieType == RealType)

@@ -210,8 +188,6 @@ namespace BytecodeTranslator {
     /// <summary>

     /// Used to represent "boxing" as it is done in the CLR.

     /// </summary>

-    [RepresentationFor("Struct2Ref", "function Struct2Ref(Struct): Ref;")]

-    public Bpl.Function Struct2Ref = null;

     [RepresentationFor("Int2Ref", "function Int2Ref(int): Ref;")]

     public Bpl.Function Int2Ref = null;

     [RepresentationFor("Bool2Ref", "function Bool2Ref(bool): Ref;")]

@@ -221,11 +197,11 @@ namespace BytecodeTranslator {
     #region Real number conversions

     [RepresentationFor("Int2Real", "function Int2Real(int, Type, Type): Real;")]

     public Bpl.Function Int2Real = null;

-    [RepresentationFor("Real2Int", "function Real2Int(Real, Type, Type): Real;")]

+    [RepresentationFor("Real2Int", "function Real2Int(Real, Type, Type): int;")]

     public Bpl.Function Real2Int = null;

     [RepresentationFor("Ref2Real", "function Ref2Real(Ref, Type, Type): Real;")]

     public Bpl.Function Ref2Real = null;

-    [RepresentationFor("Real2Ref", "function Real2Ref(Real, Type, Type): Ref;")]

+    [RepresentationFor("Real2Ref", "function Real2Ref(Real): Ref;")]

     public Bpl.Function Real2Ref = null;

     #endregion

 

@@ -238,6 +214,14 @@ namespace BytecodeTranslator {
     public Bpl.Function RealTimes = null;

     [RepresentationFor("RealDivide", "function RealDivide(Real, Real): Real;")]

     public Bpl.Function RealDivide = null;

+    [RepresentationFor("RealLessThan", "function RealLessThan(Real, Real): bool;")]

+    public Bpl.Function RealLessThan = null;

+    [RepresentationFor("RealLessThanOrEqual", "function RealLessThanOrEqual(Real, Real): bool;")]

+    public Bpl.Function RealLessThanOrEqual = null;

+    [RepresentationFor("RealGreaterThan", "function RealGreaterThan(Real, Real): bool;")]

+    public Bpl.Function RealGreaterThan = null;

+    [RepresentationFor("RealGreaterThanOrEqual", "function RealGreaterThanOrEqual(Real, Real): bool;")]

+    public Bpl.Function RealGreaterThanOrEqual = null;

     #endregion

 

     #region Bitwise operations

@@ -319,8 +303,63 @@ namespace BytecodeTranslator {
     [RepresentationFor("$As", "function $As(Ref, Type): Ref;")]

     public Bpl.Function AsFunction = null;

 

-    protected readonly string DelegateEncodingText =

-      @"procedure DelegateAdd(a: Ref, b: Ref) returns (c: Ref)

+    protected readonly string CommonText =

+      @"var $Alloc: [Ref] bool;

+

+procedure {:inline 1} Alloc() returns (x: Ref)

+  modifies $Alloc;

+{

+  assume $Alloc[x] == false && x != null;

+  $Alloc[x] := true;

+}

+

+function $TypeOfInv(Ref): Type;

+axiom (forall t: Type :: {$TypeOf(t)} $TypeOfInv($TypeOf(t)) == t);

+

+procedure {:inline 1} System.Object.GetType(this: Ref) returns ($result: Ref)

+{

+  $result := $TypeOf($DynamicType(this));

+}

+

+axiom Box2Int($DefaultBox) == 0;

+axiom Box2Bool($DefaultBox) == false;

+axiom Box2Ref($DefaultBox) == null;

+

+axiom (forall x: int :: { Int2Box(x) } Box2Int(Int2Box(x)) == x );

+axiom (forall x: bool :: { Bool2Box(x) } Box2Bool(Bool2Box(x)) == x );

+axiom (forall x: Ref :: { Ref2Box(x) } Box2Ref(Ref2Box(x)) == x );

+

+function $ThreadDelegate(Ref) : Ref;

+

+procedure {:inline 1} System.Threading.Thread.#ctor$System.Threading.ParameterizedThreadStart(this: Ref, start$in: Ref)

+{

+  assume $ThreadDelegate(this) == start$in;

+}

+procedure {:inline 1} System.Threading.Thread.Start$System.Object(this: Ref, parameter$in: Ref)

+{

+  call {:async} Wrapper_System.Threading.ParameterizedThreadStart.Invoke$System.Object($ThreadDelegate(this), parameter$in);

+}

+procedure {:inline 1} Wrapper_System.Threading.ParameterizedThreadStart.Invoke$System.Object(this: Ref, obj$in: Ref) {

+  $Exception := null;

+  call System.Threading.ParameterizedThreadStart.Invoke$System.Object(this, obj$in);

+}

+procedure {:extern} System.Threading.ParameterizedThreadStart.Invoke$System.Object(this: Ref, obj$in: Ref);

+

+procedure {:inline 1} System.Threading.Thread.#ctor$System.Threading.ThreadStart(this: Ref, start$in: Ref) 

+{

+  assume $ThreadDelegate(this) == start$in;

+}

+procedure {:inline 1} System.Threading.Thread.Start(this: Ref) 

+{

+  call {:async} Wrapper_System.Threading.ThreadStart.Invoke($ThreadDelegate(this));

+}

+procedure {:inline 1} Wrapper_System.Threading.ThreadStart.Invoke(this: Ref) {

+  $Exception := null;

+  call System.Threading.ThreadStart.Invoke(this);

+}

+procedure {:extern} System.Threading.ThreadStart.Invoke(this: Ref);

+

+procedure DelegateAdd(a: Ref, b: Ref) returns (c: Ref)

 {

   var m: int;

   var o: Ref;

@@ -444,6 +483,9 @@ procedure DelegateRemoveHelper(oldi: Ref, m: int, o: Ref) returns (i: Ref)
 

     [RepresentationFor("$Receiver", "var $Receiver: [Ref][Ref]Ref;")]

     public Bpl.GlobalVariable DelegateReceiver = null;

+

+    [RepresentationFor("$Exception", "var {:thread_local} $Exception: Ref;")]

+    public Bpl.GlobalVariable ExceptionVariable = null;

   }

 

   public abstract class HeapFactory {

diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs
index b816a439..7d04401b 100644
--- a/BCT/BytecodeTranslator/MetadataTraverser.cs
+++ b/BCT/BytecodeTranslator/MetadataTraverser.cs
@@ -104,7 +104,7 @@ namespace BytecodeTranslator {
       var proc = this.sink.FindOrCreateProcedureForDefaultStructCtor(typeDefinition);

 

       this.sink.BeginMethod(typeDefinition);

-      var stmtTranslator = this.factory.MakeStatementTraverser(this.sink, this.PdbReader, false);

+      var stmtTranslator = this.factory.MakeStatementTraverser(this.sink, this.PdbReader, false, new List<Tuple<ITryCatchFinallyStatement, StatementTraverser.TryCatchFinallyContext>>());

       var stmts = new List<IStatement>();

 

       foreach (var f in typeDefinition.Fields) {

@@ -207,7 +207,7 @@ namespace BytecodeTranslator {
 

       this.sink.BeginMethod(typeDefinition);

 

-      var stmtTranslator = this.factory.MakeStatementTraverser(this.sink, this.PdbReader, false);

+      var stmtTranslator = this.factory.MakeStatementTraverser(this.sink, this.PdbReader, false, new List<Tuple<ITryCatchFinallyStatement, StatementTraverser.TryCatchFinallyContext>>());

       var stmts = new List<IStatement>();

 

       foreach (var f in typeDefinition.Fields) {

@@ -262,12 +262,12 @@ namespace BytecodeTranslator {
         return;

 

 

-      Sink.ProcedureInfo procAndFormalMap;

+      Sink.ProcedureInfo procInfo;

       IMethodDefinition stubMethod = null;

       if (IsStubMethod(method, out stubMethod)) {

-        procAndFormalMap = this.sink.FindOrCreateProcedureAndReturnProcAndFormalMap(stubMethod);

+        procInfo = this.sink.FindOrCreateProcedure(stubMethod);

       } else {

-        procAndFormalMap = this.sink.FindOrCreateProcedureAndReturnProcAndFormalMap(method);

+        procInfo = this.sink.FindOrCreateProcedure(method);

       }

 

       if (method.IsAbstract) { // we're done, just define the procedure

@@ -275,14 +275,12 @@ namespace BytecodeTranslator {
       }

 

       this.sink.BeginMethod(method);

-      var decl = procAndFormalMap.Decl;

+      var decl = procInfo.Decl;

       var proc = decl as Bpl.Procedure;

-      var formalMap = procAndFormalMap.FormalMap;

-      this.sink.RetVariable = procAndFormalMap.ReturnVariable;

+      var formalMap = procInfo.FormalMap;

 

       try {

-

-        StatementTraverser stmtTraverser = this.factory.MakeStatementTraverser(this.sink, this.PdbReader, false);

+        StatementTraverser stmtTraverser = this.factory.MakeStatementTraverser(this.sink, this.PdbReader, false, new List<Tuple<ITryCatchFinallyStatement, StatementTraverser.TryCatchFinallyContext>>());

 

         #region Add assignments from In-Params to local-Params

 

@@ -295,13 +293,6 @@ namespace BytecodeTranslator {
           }

         }

 

-        if (!method.IsStatic && method.ContainingType.ResolvedType.IsStruct) {

-          Bpl.IToken tok = method.Token();

-          stmtTraverser.StmtBuilder.Add(Bpl.Cmd.SimpleAssign(tok,

-            Bpl.Expr.Ident(this.sink.ThisVariable),

-            new Bpl.IdentifierExpr(tok, proc.InParams[0])));

-        }

-

         #endregion

 

         #region For non-deferring ctors and all cctors, initialize all fields to null-equivalent values

@@ -326,20 +317,26 @@ namespace BytecodeTranslator {
               var mdc = c as IMetadataConstant;

               if (mdc != null) {

                 object o;

-                switch (mdc.Type.TypeCode) {

-                  case PrimitiveTypeCode.Boolean:

-                    o = (bool)mdc.Value ? Bpl.Expr.True : Bpl.Expr.False;

-                    break;

-                  case PrimitiveTypeCode.Int32:

-                    var lit = Bpl.Expr.Literal((int)mdc.Value);

-                    lit.Type = Bpl.Type.Int;

-                    o = lit;

-                    break;

-                  case PrimitiveTypeCode.String:

-                    o = mdc.Value;

-                    break;

-                  default:

-                    throw new InvalidCastException("Invalid metadata constant type");

+                if (mdc.Type.IsEnum) {

+                  var lit = Bpl.Expr.Literal((int) mdc.Value);

+                  lit.Type = Bpl.Type.Int;

+                  o = lit;

+                } else {

+                  switch (mdc.Type.TypeCode) {

+                    case PrimitiveTypeCode.Boolean:

+                      o = (bool) mdc.Value ? Bpl.Expr.True : Bpl.Expr.False;

+                      break;

+                    case PrimitiveTypeCode.Int32:

+                      var lit = Bpl.Expr.Literal((int) mdc.Value);

+                      lit.Type = Bpl.Type.Int;

+                      o = lit;

+                      break;

+                    case PrimitiveTypeCode.String:

+                      o = mdc.Value;

+                      break;

+                    default:

+                      throw new InvalidCastException("Invalid metadata constant type");

+                  }

                 }

                 args[argIndex++] = o;

               }

@@ -359,13 +356,11 @@ namespace BytecodeTranslator {
           this.privateTypes.AddRange(helperTypes);

         }

         //method.Body.Dispatch(stmtTraverser);

+        stmtTraverser.GenerateDispatchContinuation();

         #endregion

 

         #region Create Local Vars For Implementation

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

-        if (!method.IsStatic && method.ContainingType.ResolvedType.IsStruct) {

-          vars.Add(this.sink.ThisVariable);

-        }

         foreach (MethodParameter mparam in formalMap.Values) {

           if (!mparam.underlyingParameter.IsByReference)

             vars.Add(mparam.outParameterCopy);

@@ -373,7 +368,9 @@ namespace BytecodeTranslator {
         foreach (Bpl.Variable v in this.sink.LocalVarMap.Values) {

           vars.Add(v);

         }

-

+        vars.Add(procInfo.LocalExcVariable);

+        vars.Add(procInfo.FinallyStackVariable);

+        vars.Add(procInfo.LabelVariable);

         Bpl.VariableSeq vseq = new Bpl.VariableSeq(vars.ToArray());

         #endregion

 

diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
index 50ac68cf..cb0836f2 100644
--- a/BCT/BytecodeTranslator/Program.cs
+++ b/BCT/BytecodeTranslator/Program.cs
@@ -124,6 +124,7 @@ namespace BytecodeTranslator {
           pdbReader = new PdbReader(pdbStream, host);

         }

         module = Decompiler.GetCodeModelFromMetadataModel(host, module, pdbReader) as IModule;

+        host.RegisterAsLatest(module);

         modules.Add(module);

         contractExtractors.Add(module, host.GetContractExtractor(module.UnitIdentity));

         pdbReaders.Add(module, pdbReader);

@@ -182,8 +183,8 @@ namespace BytecodeTranslator {
       MetadataTraverser translator = traverserFactory.MakeMetadataTraverser(sink, contractExtractors, pdbReaders);

       translator.TranslateAssemblies(modules);

 

-      foreach (ITypeDefinition type in sink.delegateTypeToDelegates.Keys) {

-        CreateDispatchMethod(sink, type);

+      foreach (var pair in sink.delegateTypeToDelegates.Values) {

+        CreateDispatchMethod(sink, pair.Item1, pair.Item2);

       }

 

       Microsoft.Boogie.TokenTextWriter writer = new Microsoft.Boogie.TokenTextWriter(primaryModule.Name + ".bpl");

@@ -229,7 +230,7 @@ namespace BytecodeTranslator {
       ifStmtBuilder.Add(new Bpl.ReturnCmd(b.tok));

       return new Bpl.IfCmd(b.tok, b, ifStmtBuilder.Collect(b.tok), null, null);

     }

-    private static void CreateDispatchMethod(Sink sink, ITypeDefinition type) {

+    private static void CreateDispatchMethod(Sink sink, ITypeDefinition type, HashSet<IMethodDefinition> delegates) {

       Contract.Assert(type.IsDelegate);

       IMethodDefinition invokeMethod = null;

       foreach (IMethodDefinition m in type.Methods) {

@@ -240,7 +241,7 @@ namespace BytecodeTranslator {
       }

 

       try {

-        var decl = sink.FindOrCreateProcedure(invokeMethod);

+        var decl = sink.FindOrCreateProcedure(invokeMethod).Decl;

         var proc = decl as Bpl.Procedure;

         var invars = proc.InParams;

         var outvars = proc.OutParams;

@@ -275,7 +276,7 @@ namespace BytecodeTranslator {
         sink.TranslatedProgram.TopLevelDeclarations.Add(dispatchProc);

 

         Bpl.IfCmd ifCmd = BuildIfCmd(Bpl.Expr.True, new Bpl.AssumeCmd(token, Bpl.Expr.False), null);

-        foreach (IMethodDefinition defn in sink.delegateTypeToDelegates[type]) {

+        foreach (IMethodDefinition defn in delegates) {

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

           Bpl.IdentifierExprSeq outs = new Bpl.IdentifierExprSeq();

           if (!defn.IsStatic)

diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs
index 6e6b7b9b..02a173b9 100644
--- a/BCT/BytecodeTranslator/Sink.cs
+++ b/BCT/BytecodeTranslator/Sink.cs
@@ -41,7 +41,7 @@ namespace BytecodeTranslator {
         foreach (var d in this.TranslatedProgram.TopLevelDeclarations) {

           var p = d as Bpl.Procedure;

           if (p != null) {

-            this.initiallyDeclaredProcedures.Add(p.Name, p);

+            this.initiallyDeclaredProcedures.Add(p.Name, new ProcedureInfo(p));

           }

         }

       }

@@ -52,8 +52,36 @@ namespace BytecodeTranslator {
     }

     readonly Heap heap;

 

-    public Bpl.Variable ThisVariable;

-    public Bpl.Variable RetVariable;

+    public Bpl.Formal ThisVariable {

+      get {

+        ProcedureInfo info = FindOrCreateProcedure(this.methodBeingTranslated);

+        return info.ThisVariable;

+      }

+    }

+    public Bpl.Formal ReturnVariable {

+      get {

+        ProcedureInfo info = FindOrCreateProcedure(this.methodBeingTranslated);

+        return info.ReturnVariable;

+      }

+    }

+    public Bpl.LocalVariable LocalExcVariable {

+      get {

+        ProcedureInfo info = FindOrCreateProcedure(this.methodBeingTranslated);

+        return info.LocalExcVariable;

+      }

+    }

+    public Bpl.LocalVariable FinallyStackCounterVariable {

+      get {

+        ProcedureInfo info = FindOrCreateProcedure(this.methodBeingTranslated);

+        return info.FinallyStackVariable;

+      }

+    }

+    public Bpl.LocalVariable LabelVariable {

+      get {

+        ProcedureInfo info = FindOrCreateProcedure(this.methodBeingTranslated);

+        return info.LabelVariable;

+      }

+    }

 

     public readonly string AllocationMethodName = "Alloc";

     public readonly string StaticFieldFunction = "ClassRepr";

@@ -312,49 +340,84 @@ namespace BytecodeTranslator {
     public struct ProcedureInfo {

       private Bpl.DeclWithFormals decl;

       private Dictionary<IParameterDefinition, MethodParameter> formalMap;

-      private Bpl.Variable returnVariable;

+      private Bpl.Formal thisVariable;

+      private Bpl.Formal returnVariable;

+      private Bpl.LocalVariable localExcVariable;

+      private Bpl.LocalVariable finallyStackVariable;

+      private Bpl.LocalVariable labelVariable;

       private List<Bpl.Formal> typeParameters;

       private List<Bpl.Formal> methodParameters;

 

-      public ProcedureInfo(Bpl.DeclWithFormals decl, Dictionary<IParameterDefinition, MethodParameter> formalMap, Bpl.Variable returnVariable) {

+      public ProcedureInfo(Bpl.DeclWithFormals decl) {

         this.decl = decl;

-        this.formalMap = formalMap;

-        this.returnVariable = returnVariable;

+        this.formalMap = null;

+        this.returnVariable = null;

+        this.thisVariable = null;

+        this.localExcVariable = null;

+        this.finallyStackVariable = null;

+        this.labelVariable = null;

         this.typeParameters = null;

         this.methodParameters = null;

       }

-

-      public ProcedureInfo(Bpl.DeclWithFormals decl, Dictionary<IParameterDefinition, MethodParameter> formalMap, Bpl.Variable returnVariable, List<Bpl.Formal> typeParameters, List<Bpl.Formal> methodParameters) {

-        this.decl = decl;

-        this.formalMap = formalMap;

+      public ProcedureInfo(

+        Bpl.DeclWithFormals decl,

+        Dictionary<IParameterDefinition, MethodParameter> formalMap)

+        : this(decl) {

+          this.formalMap = formalMap;

+      }

+      public ProcedureInfo(

+        Bpl.DeclWithFormals decl,

+        Dictionary<IParameterDefinition, MethodParameter> formalMap,

+        Bpl.Formal returnVariable)

+        : this(decl, formalMap) {

         this.returnVariable = returnVariable;

+      }

+      public ProcedureInfo(

+        Bpl.DeclWithFormals decl,

+        Dictionary<IParameterDefinition, MethodParameter> formalMap,

+        Bpl.Formal returnVariable,

+        Bpl.Formal thisVariable,

+        Bpl.LocalVariable localExcVariable,

+        Bpl.LocalVariable finallyStackVariable,

+        Bpl.LocalVariable labelVariable,

+        List<Bpl.Formal> typeParameters,

+        List<Bpl.Formal> methodParameters)

+        : this(decl, formalMap, returnVariable) {

+        this.thisVariable = thisVariable;

+        this.localExcVariable = localExcVariable;

+        this.finallyStackVariable = finallyStackVariable;

+        this.labelVariable = labelVariable;

         this.typeParameters = typeParameters;

         this.methodParameters = methodParameters;

       }

 

       public Bpl.DeclWithFormals Decl { get { return decl; } }

       public Dictionary<IParameterDefinition, MethodParameter> FormalMap { get { return formalMap; } }

-      public Bpl.Variable ReturnVariable { get { return returnVariable; } }

+      public Bpl.Formal ThisVariable { get { return thisVariable; } }

+      public Bpl.Formal ReturnVariable { get { return returnVariable; } }

+      public Bpl.LocalVariable LocalExcVariable { get { return localExcVariable; } }

+      public Bpl.LocalVariable FinallyStackVariable { get { return finallyStackVariable; } }

+      public Bpl.LocalVariable LabelVariable { get { return labelVariable; } }

       public Bpl.Formal TypeParameter(int index) { return typeParameters[index]; }

       public Bpl.Formal MethodParameter(int index) { return methodParameters[index]; } 

     }

 

-    public Bpl.DeclWithFormals FindOrCreateProcedure(IMethodDefinition method) {

-      ProcedureInfo procAndFormalMap;

-

+    public ProcedureInfo FindOrCreateProcedure(IMethodDefinition method) {

+      ProcedureInfo procInfo;

       var key = method.InternedKey;

 

-      if (!this.declaredMethods.TryGetValue(key, out procAndFormalMap)) {

-

+      if (!this.declaredMethods.TryGetValue(key, out procInfo)) {

         string MethodName = TranslationHelper.CreateUniqueMethodName(method);

-

-        Bpl.Procedure p;

-        if (this.initiallyDeclaredProcedures.TryGetValue(MethodName, out p)) return p;

-

-        #region Create in- and out-parameters

-

+        if (this.initiallyDeclaredProcedures.TryGetValue(MethodName, out procInfo)) return procInfo;

+

+        Bpl.Formal thisVariable = null;

+        Bpl.Formal retVariable = null;

+        Bpl.LocalVariable localExcVariable = new Bpl.LocalVariable(Bpl.Token.NoToken, new Bpl.TypedIdent(Bpl.Token.NoToken, "$localExc", this.Heap.RefType));

+        Bpl.LocalVariable finallyStackVariable = new Bpl.LocalVariable(Bpl.Token.NoToken, new Bpl.TypedIdent(Bpl.Token.NoToken, "$finallyStackCounter", Bpl.Type.Int));

+        Bpl.LocalVariable labelVariable = new Bpl.LocalVariable(Bpl.Token.NoToken, new Bpl.TypedIdent(Bpl.Token.NoToken, "$label", Bpl.Type.Int));

+        

         int in_count = 0;

-        int out_count = 0;

+        int out_count = 0; 

         MethodParameter mp;

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

         foreach (IParameterDefinition formal in method.Parameters) {

@@ -365,31 +428,17 @@ namespace BytecodeTranslator {
           formalMap.Add(formal, mp);

         }

 

-        #region Look for Returnvalue

-

-        Bpl.Variable savedRetVariable = this.RetVariable;

-

         if (method.Type.TypeCode != PrimitiveTypeCode.Void) {

           Bpl.Type rettype = CciTypeToBoogie(method.Type);

           out_count++;

-          this.RetVariable = new Bpl.Formal(method.Token(),

-              new Bpl.TypedIdent(method.Type.Token(),

-                  "$result", rettype), false);

-        } else {

-          this.RetVariable = null;

+          retVariable = new Bpl.Formal(method.Token(), new Bpl.TypedIdent(method.Type.Token(), "$result", rettype), false);

         }

 

-        #endregion

-

-        Bpl.Formal/*?*/ self = null;

-        #region Create 'this' parameter

         if (!method.IsStatic) {

           var selfType = CciTypeToBoogie(method.ContainingType);

           in_count++;

-          var self_name = method.ContainingTypeDefinition.IsStruct ? "this$in" : "this";

-          self = new Bpl.Formal(method.Token(), new Bpl.TypedIdent(method.Type.Token(), self_name, selfType), true);

+          thisVariable = new Bpl.Formal(method.Token(), new Bpl.TypedIdent(method.Type.Token(), "$this", selfType), true);

         }

-        #endregion

 

         List<Bpl.Formal> typeParameters = new List<Bpl.Formal>();

         ITypeDefinition containingType = method.ContainingType.ResolvedType;

@@ -419,10 +468,8 @@ namespace BytecodeTranslator {
         int i = 0;

         int j = 0;

 

-        #region Add 'this' parameter as first in parameter

-        if (self != null)

-          invars[i++] = self;

-        #endregion

+        if (thisVariable != null)

+          invars[i++] = thisVariable;

 

         foreach (MethodParameter mparam in formalMap.Values) {

           if (mparam.inParameterCopy != null) {

@@ -434,10 +481,6 @@ namespace BytecodeTranslator {
           }

         }

 

-        #region add the returnvalue to out if there is one

-        if (this.RetVariable != null) outvars[j] = this.RetVariable;

-        #endregion

-

         if (method.IsStatic) {

           foreach (Bpl.Formal f in typeParameters) {

             invars[i++] = f;

@@ -446,7 +489,8 @@ namespace BytecodeTranslator {
         foreach (Bpl.Formal f in methodParameters) {

           invars[i++] = f;

         }

-        #endregion

+

+        if (retVariable != null) outvars[j++] = retVariable;

 

         var tok = method.Token();

         Bpl.RequiresSeq boogiePrecondition = new Bpl.RequiresSeq();

@@ -458,7 +502,7 @@ namespace BytecodeTranslator {
           var func = new Bpl.Function(tok,

             MethodName,

             new Bpl.VariableSeq(invars),

-            this.RetVariable);

+            retVariable);

           decl = func;

         } else {

           var proc = new Bpl.Procedure(tok,

@@ -484,8 +528,8 @@ namespace BytecodeTranslator {
         } else {

           this.TranslatedProgram.TopLevelDeclarations.Add(decl);

         }

-        procAndFormalMap = new ProcedureInfo(decl, formalMap, this.RetVariable, typeParameters, methodParameters);

-        this.declaredMethods.Add(key, procAndFormalMap);

+        procInfo = new ProcedureInfo(decl, formalMap, retVariable, thisVariable, localExcVariable, finallyStackVariable, labelVariable, typeParameters, methodParameters);

+        this.declaredMethods.Add(key, procInfo);

 

         // Can't visit the method's contracts until the formalMap and procedure are added to the

         // table because information in them might be needed (e.g., if a parameter is mentioned

@@ -500,7 +544,7 @@ namespace BytecodeTranslator {
           try {

 

             foreach (IPrecondition pre in contract.Preconditions) {

-              var stmtTraverser = this.factory.MakeStatementTraverser(this, null, true);

+              var stmtTraverser = this.factory.MakeStatementTraverser(this, null, true, new List<Tuple<ITryCatchFinallyStatement, StatementTraverser.TryCatchFinallyContext>>());

               ExpressionTraverser exptravers = this.factory.MakeExpressionTraverser(this, stmtTraverser, true);

               exptravers.Visit(pre.Condition); // TODO

               // Todo: Deal with Descriptions

@@ -509,7 +553,7 @@ namespace BytecodeTranslator {
             }

 

             foreach (IPostcondition post in contract.Postconditions) {

-              var stmtTraverser = this.factory.MakeStatementTraverser(this, null, true);

+              var stmtTraverser = this.factory.MakeStatementTraverser(this, null, true, new List<Tuple<ITryCatchFinallyStatement, StatementTraverser.TryCatchFinallyContext>>());

               ExpressionTraverser exptravers = this.factory.MakeExpressionTraverser(this, stmtTraverser, true);

               exptravers.Visit(post.Condition);

               // Todo: Deal with Descriptions

@@ -554,10 +598,8 @@ namespace BytecodeTranslator {
           }

         }

         #endregion

-

-        this.RetVariable = savedRetVariable;

       }

-      return procAndFormalMap.Decl;

+      return procInfo;

     }

 

     private Dictionary<uint, ProcedureInfo> declaredStructDefaultCtors = new Dictionary<uint, ProcedureInfo>();

@@ -580,7 +622,7 @@ namespace BytecodeTranslator {
         var typename = TranslationHelper.TurnStringIntoValidIdentifier(TypeHelper.GetTypeName(structType));

         var tok = structType.Token();

         var selfType = this.CciTypeToBoogie(structType); //new Bpl.MapType(Bpl.Token.NoToken, new Bpl.TypeVariableSeq(), new Bpl.TypeSeq(Heap.FieldType), Heap.BoxType);

-        var selfIn = new Bpl.Formal(tok, new Bpl.TypedIdent(tok, "this", selfType), false);

+        var selfIn = new Bpl.Formal(tok, new Bpl.TypedIdent(tok, "this", selfType), true);

         var invars = new Bpl.Formal[]{ selfIn };

         var proc = new Bpl.Procedure(Bpl.Token.NoToken, typename + ".#default_ctor",

           new Bpl.TypeVariableSeq(),

@@ -591,7 +633,7 @@ namespace BytecodeTranslator {
           new Bpl.EnsuresSeq()

           );

         this.TranslatedProgram.TopLevelDeclarations.Add(proc);

-        procAndFormalMap = new ProcedureInfo(proc, new Dictionary<IParameterDefinition, MethodParameter>(), this.RetVariable);

+        procAndFormalMap = new ProcedureInfo(proc, new Dictionary<IParameterDefinition, MethodParameter>());

         this.declaredStructDefaultCtors.Add(key, procAndFormalMap);

       }

       return procAndFormalMap.Decl;

@@ -617,8 +659,8 @@ namespace BytecodeTranslator {
         var typename = TranslationHelper.TurnStringIntoValidIdentifier(TypeHelper.GetTypeName(structType));

         var tok = structType.Token();

         var selfType = this.CciTypeToBoogie(structType); //new Bpl.MapType(Bpl.Token.NoToken, new Bpl.TypeVariableSeq(), new Bpl.TypeSeq(Heap.FieldType), Heap.BoxType);

-        var selfIn = new Bpl.Formal(tok, new Bpl.TypedIdent(tok, "this", selfType), false);

-        var otherIn = new Bpl.Formal(tok, new Bpl.TypedIdent(tok, "other", selfType), false);

+        var selfIn = new Bpl.Formal(tok, new Bpl.TypedIdent(tok, "this", selfType), true);

+        var otherIn = new Bpl.Formal(tok, new Bpl.TypedIdent(tok, "other", selfType), true);

         var invars = new Bpl.Formal[] { selfIn, otherIn, };

         var outvars = new Bpl.Formal[0];

         var selfInExpr = Bpl.Expr.Ident(selfIn);

@@ -635,7 +677,7 @@ namespace BytecodeTranslator {
           new Bpl.EnsuresSeq(ens)

           );

         this.TranslatedProgram.TopLevelDeclarations.Add(proc);

-        procAndFormalMap = new ProcedureInfo(proc, new Dictionary<IParameterDefinition, MethodParameter>(), this.RetVariable);

+        procAndFormalMap = new ProcedureInfo(proc, new Dictionary<IParameterDefinition, MethodParameter>());

         this.declaredStructCopyCtors.Add(key, procAndFormalMap);

       }

       return procAndFormalMap.Decl;

@@ -676,11 +718,6 @@ namespace BytecodeTranslator {
       return false;

     }

 

-    public ProcedureInfo FindOrCreateProcedureAndReturnProcAndFormalMap(IMethodDefinition method) {

-      this.FindOrCreateProcedure(method);

-      var key = method.InternedKey;

-      return this.declaredMethods[key];

-    }

     public static IMethodReference Unspecialize(IMethodReference method) {

       IMethodReference result = method;

       var gmir = result as IGenericMethodInstanceReference;

@@ -753,7 +790,7 @@ namespace BytecodeTranslator {
           containingType = containingType.ContainingTypeDefinition as INestedTypeDefinition;

         }

 

-        ProcedureInfo info = FindOrCreateProcedureAndReturnProcAndFormalMap(methodBeingTranslated);

+        ProcedureInfo info = FindOrCreateProcedure(methodBeingTranslated);

         if (methodBeingTranslated.IsStatic) {

           return Bpl.Expr.Ident(info.TypeParameter(index));

         }

@@ -765,8 +802,8 @@ namespace BytecodeTranslator {
 

       IGenericMethodParameter gmp = type as IGenericMethodParameter;

       if (gmp != null) {

-        ProcedureInfo info = FindOrCreateProcedureAndReturnProcAndFormalMap(methodBeingTranslated);

-        return Bpl.Expr.Ident(info.TypeParameter(gmp.Index));

+        ProcedureInfo info = FindOrCreateProcedure(methodBeingTranslated);

+        return Bpl.Expr.Ident(info.MethodParameter(gmp.Index));

       }

 

       ITypeReference uninstantiatedGenericType = GetUninstantiatedGenericType(type);

@@ -864,21 +901,62 @@ namespace BytecodeTranslator {
     /// The values in this table are the procedures

     /// defined in the program created by the heap in the Sink's ctor.

     /// </summary>

-    private Dictionary<string, Bpl.Procedure> initiallyDeclaredProcedures = new Dictionary<string, Bpl.Procedure>();

+    public Dictionary<string, ProcedureInfo> initiallyDeclaredProcedures = new Dictionary<string, ProcedureInfo>();

 

     public void BeginMethod(ITypeReference containingType) {

       this.localVarMap = new Dictionary<ILocalDefinition, Bpl.LocalVariable>();

       this.localCounter = 0;

-      this.ThisVariable = new Bpl.LocalVariable(Bpl.Token.NoToken, new Bpl.TypedIdent(Bpl.Token.NoToken, "this", this.Heap.RefType));

       this.methodBeingTranslated = null;

     }

 

+    public Dictionary<IName, int> cciLabels;

+    public int FindOrCreateCciLabelIdentifier(IName label) {

+      int v;

+      if (!cciLabels.TryGetValue(label, out v)) {

+        v = cciLabels.Count;

+        cciLabels[label] = v;

+      }

+      return v;

+    }

+    Dictionary<ITryCatchFinallyStatement, int> tryCatchFinallyIdentifiers;

+    public string FindOrCreateCatchLabel(ITryCatchFinallyStatement stmt) {

+      int id;

+      if (!tryCatchFinallyIdentifiers.TryGetValue(stmt, out id)) {

+        id = tryCatchFinallyIdentifiers.Count;

+        tryCatchFinallyIdentifiers[stmt] = id;

+      }

+      return "catch" + id;

+    }

+    public string FindOrCreateFinallyLabel(ITryCatchFinallyStatement stmt) {

+      int id;

+      if (!tryCatchFinallyIdentifiers.TryGetValue(stmt, out id)) {

+        id = tryCatchFinallyIdentifiers.Count;

+        tryCatchFinallyIdentifiers[stmt] = id;

+      }

+      return "finally" + id;

+    }

+    public string FindOrCreateContinuationLabel(ITryCatchFinallyStatement stmt) {

+      int id;

+      if (!tryCatchFinallyIdentifiers.TryGetValue(stmt, out id)) {

+        id = tryCatchFinallyIdentifiers.Count;

+        tryCatchFinallyIdentifiers[stmt] = id;

+      }

+      return "continuation" + id;

+    }

+    MostNestedTryStatementTraverser mostNestedTryStatementTraverser;

+    public ITryCatchFinallyStatement MostNestedTryStatement(IName label) {

+      return mostNestedTryStatementTraverser.MostNestedTryStatement(label);

+    }

     IMethodDefinition methodBeingTranslated;

     public void BeginMethod(IMethodDefinition method) {

       this.BeginMethod(method.ContainingType);

       this.methodBeingTranslated = method;

+      this.cciLabels = new Dictionary<IName, int>();

+      this.tryCatchFinallyIdentifiers = new Dictionary<ITryCatchFinallyStatement, int>();

+      mostNestedTryStatementTraverser = new MostNestedTryStatementTraverser();

+      mostNestedTryStatementTraverser.Visit(method.Body);

     }

-

+    

     public void BeginAssembly(IAssembly assembly) {

       this.assemblyBeingTranslated = assembly;

     }

@@ -888,18 +966,22 @@ namespace BytecodeTranslator {
     }

     private IAssembly/*?*/ assemblyBeingTranslated;

 

-    public Dictionary<ITypeDefinition, HashSet<IMethodDefinition>> delegateTypeToDelegates = new Dictionary<ITypeDefinition, HashSet<IMethodDefinition>>();

+    public Dictionary<uint, Tuple<ITypeDefinition, HashSet<IMethodDefinition>>> delegateTypeToDelegates = 

+      new Dictionary<uint, Tuple<ITypeDefinition, HashSet<IMethodDefinition>>>();

 

     public void AddDelegate(ITypeDefinition type, IMethodDefinition defn)

     {

-      if (!delegateTypeToDelegates.ContainsKey(type))

-        delegateTypeToDelegates[type] = new HashSet<IMethodDefinition>();

-      delegateTypeToDelegates[type].Add(defn);

+      uint key = type.InternedKey;

+      if (!delegateTypeToDelegates.ContainsKey(key))

+        delegateTypeToDelegates[key] = new Tuple<ITypeDefinition, HashSet<IMethodDefinition>>(type, new HashSet<IMethodDefinition>());

+      FindOrCreateProcedure(defn);

+      delegateTypeToDelegates[key].Item2.Add(defn);

     }

 

     public void AddDelegateType(ITypeDefinition type) {

-      if (!delegateTypeToDelegates.ContainsKey(type))

-        delegateTypeToDelegates[type] = new HashSet<IMethodDefinition>();

+      uint key = type.InternedKey;

+      if (!delegateTypeToDelegates.ContainsKey(key))

+        delegateTypeToDelegates[key] = new Tuple<ITypeDefinition, HashSet<IMethodDefinition>>(type, new HashSet<IMethodDefinition>());

     }

 

     private Dictionary<IMethodDefinition, Bpl.Constant> delegateMethods = new Dictionary<IMethodDefinition, Bpl.Constant>();

diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs
index f03894a2..09b0b13b 100644
--- a/BCT/BytecodeTranslator/StatementTraverser.cs
+++ b/BCT/BytecodeTranslator/StatementTraverser.cs
@@ -20,6 +20,27 @@ using System.Diagnostics.Contracts;
 

 namespace BytecodeTranslator

 {

+  public class MostNestedTryStatementTraverser : BaseCodeTraverser {

+    Dictionary<IName, ITryCatchFinallyStatement> mostNestedTryStatement = new Dictionary<IName, ITryCatchFinallyStatement>();

+    ITryCatchFinallyStatement currStatement = null;

+    public override void Visit(ILabeledStatement labeledStatement) {

+      if (currStatement != null)

+        mostNestedTryStatement.Add(labeledStatement.Label, currStatement);

+      base.Visit(labeledStatement);

+    }

+    public override void Visit(ITryCatchFinallyStatement tryCatchFinallyStatement) {

+      ITryCatchFinallyStatement savedStatement = currStatement;

+      currStatement = tryCatchFinallyStatement;

+      base.Visit(tryCatchFinallyStatement);

+      currStatement = savedStatement;

+    }

+    public ITryCatchFinallyStatement MostNestedTryStatement(IName label) {

+      if (!mostNestedTryStatement.ContainsKey(label))

+        return null;

+      return mostNestedTryStatement[label];

+    }

+  }

+

   public class StatementTraverser : BaseCodeTraverser {

 

     public readonly TraverserFactory factory;

@@ -33,11 +54,12 @@ namespace BytecodeTranslator
     internal readonly Stack<IExpression> operandStack = new Stack<IExpression>();

 

     #region Constructors

-    public StatementTraverser(Sink sink, PdbReader/*?*/ pdbReader, bool contractContext) {

+    public StatementTraverser(Sink sink, PdbReader/*?*/ pdbReader, bool contractContext, List<Tuple<ITryCatchFinallyStatement,TryCatchFinallyContext>> nestedTryCatchFinallyStatements) {

       this.sink = sink;

       this.factory = sink.Factory;

       PdbReader = pdbReader;

       this.contractContext = contractContext;

+      this.nestedTryCatchFinallyStatements = nestedTryCatchFinallyStatements;

     }

     #endregion

 

@@ -65,6 +87,18 @@ namespace BytecodeTranslator
       return newTypes;

     }

 

+    public void GenerateDispatchContinuation() {

+      // Iterate over all labels in sink.cciLabels and sink.boogieLabels and generate dispatch based on sink.LabelVariable

+      this.StmtBuilder.AddLabelCmd("DispatchContinuation");

+      Bpl.IfCmd elseIfCmd = new Bpl.IfCmd(Bpl.Token.NoToken, Bpl.Expr.Literal(true), TranslationHelper.BuildStmtList(new Bpl.AssumeCmd(Bpl.Token.NoToken, Bpl.Expr.Literal(false))), null, null);

+      Bpl.IdentifierExpr labelExpr = Bpl.Expr.Ident(this.sink.LabelVariable);

+      foreach (IName name in sink.cciLabels.Keys) {

+        Bpl.GotoCmd gotoCmd = new Bpl.GotoCmd(Bpl.Token.NoToken, new Bpl.StringSeq(name.Value));

+        Bpl.Expr targetExpr = Bpl.Expr.Literal(sink.cciLabels[name]);

+        elseIfCmd = new Bpl.IfCmd(Bpl.Token.NoToken, Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq, labelExpr, targetExpr), TranslationHelper.BuildStmtList(gotoCmd), elseIfCmd, null);

+      }

+      this.StmtBuilder.Add(elseIfCmd);

+    }

     #endregion

 

     //public override void Visit(ISourceMethodBody methodBody) {

@@ -114,15 +148,33 @@ namespace BytecodeTranslator
     #region Basic Statements

 

     public override void Visit(IAssertStatement assertStatement) {

-      StmtBuilder.Add(

-        new Bpl.AssertCmd(assertStatement.Token(), ExpressionFor(assertStatement.Condition))

-        );

+      Bpl.Expr conditionExpr = ExpressionFor(assertStatement.Condition);

+      Bpl.Type conditionType = this.sink.CciTypeToBoogie(assertStatement.Condition.Type);

+      if (conditionType == this.sink.Heap.RefType) {

+        conditionExpr = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, conditionExpr, Bpl.Expr.Ident(this.sink.Heap.NullRef));

+      }

+      else if (conditionType == Bpl.Type.Int) {

+        conditionExpr = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, conditionExpr, Bpl.Expr.Literal(0));

+      }

+      else {

+        System.Diagnostics.Debug.Assert(conditionType == Bpl.Type.Bool);

+      }

+      StmtBuilder.Add(new Bpl.AssertCmd(assertStatement.Token(), conditionExpr));

     }

 

     public override void Visit(IAssumeStatement assumeStatement) {

-      StmtBuilder.Add(

-        new Bpl.AssumeCmd(assumeStatement.Token(), ExpressionFor(assumeStatement.Condition))

-        );

+      Bpl.Expr conditionExpr = ExpressionFor(assumeStatement.Condition);

+      Bpl.Type conditionType = this.sink.CciTypeToBoogie(assumeStatement.Condition.Type);

+      if (conditionType == this.sink.Heap.RefType) {

+        conditionExpr = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, conditionExpr, Bpl.Expr.Ident(this.sink.Heap.NullRef));

+      }

+      else if (conditionType == Bpl.Type.Int) {

+        conditionExpr = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, conditionExpr, Bpl.Expr.Literal(0));

+      }

+      else {

+        System.Diagnostics.Debug.Assert(conditionType == Bpl.Type.Bool);

+      }

+      StmtBuilder.Add(new Bpl.AssumeCmd(assumeStatement.Token(), conditionExpr));

     }

 

     /// <summary>

@@ -131,16 +183,28 @@ namespace BytecodeTranslator
     /// <remarks>(mschaef) Works, but still a stub</remarks>

     /// <param name="conditionalStatement"></param>

     public override void Visit(IConditionalStatement conditionalStatement) {

-      StatementTraverser thenTraverser = this.factory.MakeStatementTraverser(this.sink, this.PdbReader, this.contractContext);

-      StatementTraverser elseTraverser = this.factory.MakeStatementTraverser(this.sink, this.PdbReader, this.contractContext);

+      StatementTraverser thenTraverser = this.factory.MakeStatementTraverser(this.sink, this.PdbReader, this.contractContext, this.nestedTryCatchFinallyStatements);

+      StatementTraverser elseTraverser = this.factory.MakeStatementTraverser(this.sink, this.PdbReader, this.contractContext, this.nestedTryCatchFinallyStatements);

 

       ExpressionTraverser condTraverser = this.factory.MakeExpressionTraverser(this.sink, this, this.contractContext);

       condTraverser.Visit(conditionalStatement.Condition);

       thenTraverser.Visit(conditionalStatement.TrueBranch);

       elseTraverser.Visit(conditionalStatement.FalseBranch);

 

+      Bpl.Expr conditionExpr = condTraverser.TranslatedExpressions.Pop();

+      Bpl.Type conditionType = this.sink.CciTypeToBoogie(conditionalStatement.Condition.Type);

+      if (conditionType == this.sink.Heap.RefType) {

+        conditionExpr = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, conditionExpr, Bpl.Expr.Ident(this.sink.Heap.NullRef));

+      }

+      else if (conditionType == Bpl.Type.Int) {

+        conditionExpr = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, conditionExpr, Bpl.Expr.Literal(0));

+      }

+      else {

+        System.Diagnostics.Debug.Assert(conditionType == Bpl.Type.Bool);

+      }

+

       Bpl.IfCmd ifcmd = new Bpl.IfCmd(conditionalStatement.Token(),

-          condTraverser.TranslatedExpressions.Pop(),

+          conditionExpr,

           thenTraverser.StmtBuilder.Collect(conditionalStatement.TrueBranch.Token()),

           null,

           elseTraverser.StmtBuilder.Collect(conditionalStatement.FalseBranch.Token())

@@ -229,12 +293,12 @@ namespace BytecodeTranslator
         ExpressionTraverser etrav = this.factory.MakeExpressionTraverser(this.sink, this, this.contractContext);

         etrav.Visit(returnStatement.Expression);

 

-        if (this.sink.RetVariable == null || etrav.TranslatedExpressions.Count < 1) {

+        if (this.sink.ReturnVariable == null || etrav.TranslatedExpressions.Count < 1) {

           throw new TranslationException(String.Format("{0} returns a value that is not supported by the function", returnStatement.ToString()));

         }

 

         StmtBuilder.Add(Bpl.Cmd.SimpleAssign(tok,

-            new Bpl.IdentifierExpr(tok, this.sink.RetVariable), etrav.TranslatedExpressions.Pop()));

+            new Bpl.IdentifierExpr(tok, this.sink.ReturnVariable), etrav.TranslatedExpressions.Pop()));

       }

       StmtBuilder.Add(new Bpl.ReturnCmd(returnStatement.Token()));

     }

@@ -248,11 +312,27 @@ namespace BytecodeTranslator
     /// <remarks> STUB </remarks>

     /// <param name="gotoStatement"></param>

     public override void Visit(IGotoStatement gotoStatement) {

-      String[] target = new String[1] { gotoStatement.TargetStatement.Label.Value };

-

-      Bpl.GotoCmd gotocmd = new Microsoft.Boogie.GotoCmd(gotoStatement.Token(), new Bpl.StringSeq(target));

-

-      StmtBuilder.Add(gotocmd);

+      IName target = gotoStatement.TargetStatement.Label;

+      ITryCatchFinallyStatement targetContext = this.sink.MostNestedTryStatement(target);

+      int count = 0;

+      while (count < this.nestedTryCatchFinallyStatements.Count) {

+        int index = this.nestedTryCatchFinallyStatements.Count - count - 1;

+        ITryCatchFinallyStatement nestedContext = this.nestedTryCatchFinallyStatements[index].Item1;

+        if (targetContext == nestedContext)

+          break;

+        count++;

+      }

+      System.Diagnostics.Debug.Assert((count == nestedTryCatchFinallyStatements.Count) == (targetContext == null));

+      if (count > 0) {

+        int id = this.sink.FindOrCreateCciLabelIdentifier(target);

+        StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.LabelVariable), Bpl.Expr.Literal(id)));

+        StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.FinallyStackCounterVariable), Bpl.Expr.Literal(count-1)));

+        string finallyLabel = this.sink.FindOrCreateFinallyLabel(this.nestedTryCatchFinallyStatements[this.nestedTryCatchFinallyStatements.Count - 1].Item1);

+        StmtBuilder.Add(new Bpl.GotoCmd(gotoStatement.Token(), new Bpl.StringSeq(finallyLabel)));

+      }

+      else {

+        StmtBuilder.Add(new Bpl.GotoCmd(gotoStatement.Token(), new Bpl.StringSeq(target.Value)));

+      }

     }

 

     /// <summary>

@@ -277,6 +357,135 @@ namespace BytecodeTranslator
 

     #endregion

 

+    public enum TryCatchFinallyContext { InTry, InCatch, InFinally };

+    List<Tuple<ITryCatchFinallyStatement, TryCatchFinallyContext>> nestedTryCatchFinallyStatements;

+    

+    private void RaiseExceptionHelper(Bpl.StmtListBuilder builder) {

+      int count = nestedTryCatchFinallyStatements.Count;

+      if (count == 0) {

+        builder.Add(new Bpl.ReturnCmd(Bpl.Token.NoToken));

+      }

+      else {

+        Tuple<ITryCatchFinallyStatement, TryCatchFinallyContext> topOfStack = nestedTryCatchFinallyStatements[count - 1];

+        string exceptionTarget; 

+        if (topOfStack.Item2 == TryCatchFinallyContext.InTry) {

+          exceptionTarget = this.sink.FindOrCreateCatchLabel(topOfStack.Item1);

+        }

+        else if (topOfStack.Item2 == TryCatchFinallyContext.InCatch) {

+          builder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.LabelVariable), Bpl.Expr.Literal(-1)));

+          exceptionTarget = this.sink.FindOrCreateFinallyLabel(topOfStack.Item1);

+        }

+        else {

+          exceptionTarget = this.sink.FindOrCreateContinuationLabel(topOfStack.Item1);

+        }

+        builder.Add(new Bpl.GotoCmd(Bpl.Token.NoToken, new Bpl.StringSeq(exceptionTarget)));

+      }

+    }

+

+    public void RaiseException() {

+      RaiseExceptionHelper(StmtBuilder);

+    }

+    

+    public void RaiseException(Bpl.Expr e) {

+      Bpl.StmtListBuilder builder = new Bpl.StmtListBuilder();

+      RaiseExceptionHelper(builder);

+      Bpl.IfCmd ifCmd = new Bpl.IfCmd(Bpl.Token.NoToken, e, builder.Collect(Bpl.Token.NoToken), null, null);

+      StmtBuilder.Add(ifCmd);

+    }

+

+    public override void Visit(ITryCatchFinallyStatement tryCatchFinallyStatement) {

+      nestedTryCatchFinallyStatements.Add(new Tuple<ITryCatchFinallyStatement, TryCatchFinallyContext>(tryCatchFinallyStatement, TryCatchFinallyContext.InTry));

+      this.Visit(tryCatchFinallyStatement.TryBody);

+      StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.LabelVariable), Bpl.Expr.Literal(-1)));

+      StmtBuilder.Add(new Bpl.GotoCmd(Bpl.Token.NoToken, new Bpl.StringSeq(this.sink.FindOrCreateFinallyLabel(tryCatchFinallyStatement))));

+      nestedTryCatchFinallyStatements.RemoveAt(nestedTryCatchFinallyStatements.Count - 1);

+

+      StmtBuilder.AddLabelCmd(this.sink.FindOrCreateCatchLabel(tryCatchFinallyStatement));

+      StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.LocalExcVariable), Bpl.Expr.Ident(this.sink.Heap.ExceptionVariable)));

+      StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.Heap.ExceptionVariable), Bpl.Expr.Ident(this.sink.Heap.NullRef)));

+      List<Bpl.StmtList> catchStatements = new List<Bpl.StmtList>();

+      List<Bpl.Expr> typeReferences = new List<Bpl.Expr>();

+      this.nestedTryCatchFinallyStatements.Add(new Tuple<ITryCatchFinallyStatement, TryCatchFinallyContext>(tryCatchFinallyStatement, TryCatchFinallyContext.InCatch));

+      foreach (ICatchClause catchClause in tryCatchFinallyStatement.CatchClauses) {

+        typeReferences.Insert(0, this.sink.FindOrCreateType(catchClause.ExceptionType));

+        StatementTraverser catchTraverser = this.factory.MakeStatementTraverser(this.sink, this.PdbReader, this.contractContext, this.nestedTryCatchFinallyStatements);

+        if (catchClause.ExceptionContainer != Dummy.LocalVariable) {

+          Bpl.Variable catchClauseVariable = this.sink.FindOrCreateLocalVariable(catchClause.ExceptionContainer);

+          catchTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(catchClauseVariable), Bpl.Expr.Ident(this.sink.LocalExcVariable)));

+        }

+        catchTraverser.Visit(catchClause.Body);

+        catchTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.LabelVariable), Bpl.Expr.Literal(-1)));

+        catchTraverser.StmtBuilder.Add(new Bpl.GotoCmd(Bpl.Token.NoToken, new Bpl.StringSeq(this.sink.FindOrCreateFinallyLabel(tryCatchFinallyStatement))));

+        catchStatements.Insert(0, catchTraverser.StmtBuilder.Collect(catchClause.Token()));

+      }

+      Bpl.IfCmd elseIfCmd = new Bpl.IfCmd(Bpl.Token.NoToken, Bpl.Expr.Literal(false), TranslationHelper.BuildStmtList(new Bpl.ReturnCmd(Bpl.Token.NoToken)), null, null);

+      Bpl.Expr dynTypeOfOperand = this.sink.Heap.DynamicType(Bpl.Expr.Ident(this.sink.LocalExcVariable));

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

+        Bpl.Expr expr = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq, dynTypeOfOperand, typeReferences[i]);

+        elseIfCmd = new Bpl.IfCmd(Bpl.Token.NoToken, expr, catchStatements[i], elseIfCmd, null);

+      }

+      this.StmtBuilder.Add(elseIfCmd);

+      this.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.Heap.ExceptionVariable), Bpl.Expr.Ident(this.sink.LocalExcVariable)));

+      RaiseException();

+      nestedTryCatchFinallyStatements.RemoveAt(nestedTryCatchFinallyStatements.Count - 1);

+

+      this.StmtBuilder.AddLabelCmd(this.sink.FindOrCreateFinallyLabel(tryCatchFinallyStatement));

+      if (tryCatchFinallyStatement.FinallyBody != null) {

+        nestedTryCatchFinallyStatements.Add(new Tuple<ITryCatchFinallyStatement, TryCatchFinallyContext>(tryCatchFinallyStatement, TryCatchFinallyContext.InFinally));

+        Bpl.Variable savedExcVariable = this.sink.CreateFreshLocal(this.sink.Heap.RefType);

+        Bpl.Variable savedLabelVariable = this.sink.CreateFreshLocal(Bpl.Type.Int);

+        Bpl.Variable savedFinallyStackCounterVariable = this.sink.CreateFreshLocal(Bpl.Type.Int);

+        StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(savedExcVariable), Bpl.Expr.Ident(this.sink.Heap.ExceptionVariable)));

+        StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(savedLabelVariable), Bpl.Expr.Ident(this.sink.LabelVariable)));

+        StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(savedFinallyStackCounterVariable), Bpl.Expr.Ident(this.sink.FinallyStackCounterVariable)));

+        Visit(tryCatchFinallyStatement.FinallyBody);

+        StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.Heap.ExceptionVariable), Bpl.Expr.Ident(savedExcVariable)));

+        StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.LabelVariable), Bpl.Expr.Ident(savedLabelVariable)));

+        StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.FinallyStackCounterVariable), Bpl.Expr.Ident(savedFinallyStackCounterVariable)));

+        nestedTryCatchFinallyStatements.RemoveAt(nestedTryCatchFinallyStatements.Count - 1);

+      }

+      Bpl.GotoCmd dispatchCmd = new Bpl.GotoCmd(Bpl.Token.NoToken, new Bpl.StringSeq("DispatchContinuation"));

+      Bpl.GotoCmd continuationCmd = new Bpl.GotoCmd(Bpl.Token.NoToken, new Bpl.StringSeq(this.sink.FindOrCreateContinuationLabel(tryCatchFinallyStatement)));

+      Bpl.IfCmd ifCmd = new Bpl.IfCmd(

+        Bpl.Token.NoToken,

+        Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq, Bpl.Expr.Ident(this.sink.LabelVariable), Bpl.Expr.Literal(-1)),

+        TranslationHelper.BuildStmtList(continuationCmd),

+        new Bpl.IfCmd(

+          Bpl.Token.NoToken,

+          Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq, Bpl.Expr.Ident(this.sink.FinallyStackCounterVariable), Bpl.Expr.Literal(0)),

+          TranslationHelper.BuildStmtList(dispatchCmd), 

+          null, 

+          null),

+        null);

+      this.StmtBuilder.Add(ifCmd);

+      int count = this.nestedTryCatchFinallyStatements.Count;

+      if (count == 0) {

+        this.StmtBuilder.Add(new Bpl.AssertCmd(Bpl.Token.NoToken, Bpl.Expr.Literal(false)));

+      }

+      else {

+        Bpl.IdentifierExpr fsv = Bpl.Expr.Ident(this.sink.FinallyStackCounterVariable);

+        Bpl.AssignCmd decrementCmd = TranslationHelper.BuildAssignCmd(fsv, Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Sub, fsv, Bpl.Expr.Literal(1)));

+        this.StmtBuilder.Add(decrementCmd);

+        string parentFinallyLabel = this.sink.FindOrCreateFinallyLabel(this.nestedTryCatchFinallyStatements[count - 1].Item1);

+        Bpl.GotoCmd parentCmd = new Bpl.GotoCmd(Bpl.Token.NoToken, new Bpl.StringSeq(parentFinallyLabel));

+        this.StmtBuilder.Add(parentCmd);

+      }

+      StmtBuilder.AddLabelCmd(this.sink.FindOrCreateContinuationLabel(tryCatchFinallyStatement));

+      Bpl.Expr raiseExpr = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, Bpl.Expr.Ident(this.sink.Heap.ExceptionVariable), Bpl.Expr.Ident(this.sink.Heap.NullRef));

+      RaiseException(raiseExpr);

+    }

+

+    public override void Visit(IThrowStatement throwStatement) {

+      ExpressionTraverser exceptionTraverser = this.factory.MakeExpressionTraverser(this.sink, this, this.contractContext);

+      exceptionTraverser.Visit(throwStatement.Exception);

+      StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.Heap.ExceptionVariable), exceptionTraverser.TranslatedExpressions.Pop()));

+      RaiseException();

+    }

+

+    public override void Visit(IRethrowStatement rethrowStatement) {

+      StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.Heap.ExceptionVariable), Bpl.Expr.Ident(this.sink.LocalExcVariable)));

+      RaiseException();

+    }

   }

 

 }

diff --git a/BCT/BytecodeTranslator/TranslationHelper.cs b/BCT/BytecodeTranslator/TranslationHelper.cs
index cf856024..726a1ea6 100644
--- a/BCT/BytecodeTranslator/TranslationHelper.cs
+++ b/BCT/BytecodeTranslator/TranslationHelper.cs
@@ -41,7 +41,7 @@ namespace BytecodeTranslator {
 

       var parameterToken = parameterDefinition.Token();

       var typeToken = parameterDefinition.Type.Token();

-      var parameterName = parameterDefinition.Name.Value;

+      var parameterName = TranslationHelper.TurnStringIntoValidIdentifier(parameterDefinition.Name.Value);

 

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

       if (parameterDefinition.IsByReference) {

@@ -61,6 +61,25 @@ namespace BytecodeTranslator {
     /// from Cci to Boogie

     /// </summary>

   static class TranslationHelper {

+    public static Bpl.StmtList BuildStmtList(Bpl.Cmd cmd, Bpl.TransferCmd tcmd) {

+      Bpl.StmtListBuilder builder = new Bpl.StmtListBuilder();

+      builder.Add(cmd);

+      builder.Add(tcmd);

+      return builder.Collect(Bpl.Token.NoToken);

+    }

+

+    public static Bpl.StmtList BuildStmtList(Bpl.TransferCmd tcmd) {

+      Bpl.StmtListBuilder builder = new Bpl.StmtListBuilder();

+      builder.Add(tcmd);

+      return builder.Collect(Bpl.Token.NoToken);

+    }

+

+    public static Bpl.StmtList BuildStmtList(params Bpl.Cmd[] cmds) {

+      Bpl.StmtListBuilder builder = new Bpl.StmtListBuilder();

+      foreach (Bpl.Cmd cmd in cmds)

+        builder.Add(cmd);

+      return builder.Collect(Bpl.Token.NoToken);

+    }

 

     public static Bpl.AssignCmd BuildAssignCmd(Bpl.IdentifierExpr lhs, Bpl.Expr rhs)

     {

@@ -82,6 +101,16 @@ namespace BytecodeTranslator {
       return "$tmp" + (tmpVarCounter++).ToString();

     }

 

+    internal static int catchClauseCounter = 0;

+    public static string GenerateCatchClauseName() {

+      return "catch" + (catchClauseCounter++).ToString();

+    }

+

+    internal static int finallyClauseCounter = 0;

+    public static string GenerateFinallyClauseName() {

+      return "finally" + (finallyClauseCounter++).ToString();

+    }

+

     public static string CreateUniqueMethodName(IMethodReference method) {

       var containingTypeName = TypeHelper.GetTypeName(method.ContainingType, NameFormattingOptions.None);

       var s = MemberHelper.GetMethodSignature(method, NameFormattingOptions.DocumentationId);

@@ -121,6 +150,9 @@ namespace BytecodeTranslator {
       s = s.Replace('%', '$');

       s = s.Replace('&', '$');

       s = s.Replace('"', '$');

+      s = s.Replace('[', '$');

+      s = s.Replace(']', '$');

+      s = s.Replace('|', '$');

       return s;

     }

 

diff --git a/BCT/BytecodeTranslator/TraverserFactory.cs b/BCT/BytecodeTranslator/TraverserFactory.cs
index 78c818bd..9fb51527 100644
--- a/BCT/BytecodeTranslator/TraverserFactory.cs
+++ b/BCT/BytecodeTranslator/TraverserFactory.cs
@@ -24,8 +24,8 @@ namespace BytecodeTranslator {
     {

       return new MetadataTraverser(sink, sourceLocationProviders);

     }

-    public virtual StatementTraverser MakeStatementTraverser(Sink sink, PdbReader/*?*/ pdbReader, bool contractContext) {

-      return new StatementTraverser(sink, pdbReader, contractContext);

+    public virtual StatementTraverser MakeStatementTraverser(Sink sink, PdbReader/*?*/ pdbReader, bool contractContext, List<Tuple<ITryCatchFinallyStatement,StatementTraverser.TryCatchFinallyContext>> nestedTryCatchFinallyStatements) {

+      return new StatementTraverser(sink, pdbReader, contractContext, nestedTryCatchFinallyStatements);

     }

     public virtual ExpressionTraverser MakeExpressionTraverser(Sink sink, StatementTraverser/*?*/ statementTraverser, bool contractContext) {

       return new ExpressionTraverser(sink, statementTraverser, contractContext);

diff --git a/BCT/Samples/Exceptions/ExceptionsExample.cs b/BCT/Samples/Exceptions/ExceptionsExample.cs
index 176d0339..5efb69b7 100644
--- a/BCT/Samples/Exceptions/ExceptionsExample.cs
+++ b/BCT/Samples/Exceptions/ExceptionsExample.cs
@@ -27,7 +27,7 @@ class PoirotMain
         {

             x = 34;

         }

-        Contract.Assert(x == 34);

+        Contract.Assert(x == 35);

     }

 }

 

diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs
index 3c2b9a42..1376245a 100644
--- a/Source/Core/DeadVarElim.cs
+++ b/Source/Core/DeadVarElim.cs
@@ -411,38 +411,28 @@ namespace Microsoft.Boogie {
         // I must first iterate over all the targets and remove the live ones.

         // After the removals are done, I must add the variables referred on 

         // the right side of the removed targets

+

+        AssignCmd simpleAssignCmd = assignCmd.AsSimpleAssignCmd;

         HashSet<int> indexSet = new HashSet<int>();

         int index = 0;

-        foreach (AssignLhs/*!*/ lhs in assignCmd.Lhss) {

+        foreach (AssignLhs/*!*/ lhs in simpleAssignCmd.Lhss) {

           Contract.Assert(lhs != null);

-          Variable var = lhs.DeepAssignedVariable;

+          SimpleAssignLhs salhs = lhs as SimpleAssignLhs;

+          Contract.Assert(salhs != null);

+          Variable var = salhs.DeepAssignedVariable;

           if (var != null && liveSet.Contains(var)) {

             indexSet.Add(index);

-            if (lhs is SimpleAssignLhs) {

-              // we should only remove non-map target variables because there is an implicit

-              // read of a map variable in an assignment to it

-              liveSet.Remove(var);

-            }

+            liveSet.Remove(var);

           }

           index++;

         }

         index = 0;

-        foreach (Expr/*!*/ expr in assignCmd.Rhss) {

+        foreach (Expr/*!*/ expr in simpleAssignCmd.Rhss) {

           Contract.Assert(expr != null);

           if (indexSet.Contains(index)) {

             VariableCollector/*!*/ collector = new VariableCollector();

             collector.Visit(expr);

             liveSet.UnionWith(collector.usedVars);

-            AssignLhs lhs = assignCmd.Lhss[index];

-            if (lhs is MapAssignLhs) {

-              // If the target is a map, then all indices are also read

-              MapAssignLhs malhs = (MapAssignLhs)lhs;

-              foreach (Expr e in malhs.Indexes) {

-                VariableCollector/*!*/ c = new VariableCollector();

-                c.Visit(e);

-                liveSet.UnionWith(c.usedVars);

-              }

-            }

           }

           index++;

         }

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index 8527e53c..130852f7 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -718,8 +718,11 @@ namespace Microsoft.Boogie {
 

       List<object> vals = new List<object>();

       foreach (int i in args) {

-        object o = cce.NonNull(partitionToValue[i]);

-        if (o is bool) {

+        object o = partitionToValue[i];

+        if (o == null) {

+          // uninterpreted value

+          vals.Add(string.Format("UI({0})", i.ToString()));

+        } else if (o is bool) {

           vals.Add(o);

         } else if (o is BigNum) {

           vals.Add(o);

diff --git a/Test/livevars/Answer b/Test/livevars/Answer
index 1a0327f6..958fc852 100644
--- a/Test/livevars/Answer
+++ b/Test/livevars/Answer
@@ -411,3 +411,7 @@ Execution trace:
     stack_overflow.bpl(97935,3): inline$storm_thread_completion$0$Return#1

 

 Boogie program verifier finished with 0 verified, 1 error

+

+Boogie program verifier finished with 1 verified, 0 errors

+

+Boogie program verifier finished with 1 verified, 0 errors

diff --git a/Test/livevars/NestedOneDimensionalMap.bpl b/Test/livevars/NestedOneDimensionalMap.bpl
new file mode 100644
index 00000000..411316ac
--- /dev/null
+++ b/Test/livevars/NestedOneDimensionalMap.bpl
@@ -0,0 +1,29 @@
+var k: int;

+var AllMaps__1: [int][int]int;

+

+procedure PoirotMain.Main_trace_1_trace_1()

+modifies k, AllMaps__1;

+{

+  var $tmp4: int;

+  var local_0: int;

+

+  lab0:

+    k := 1;

+    goto lab1, lab2;

+

+

+lab1:

+    assume k == 0;

+    goto lab3;

+

+lab2:

+    assume k == 1;

+    $tmp4 := local_0;

+    goto lab3;

+

+lab3:    

+    AllMaps__1[$tmp4][0] := 1;   

+    assert AllMaps__1[local_0][0] == 1;

+}

+

+

diff --git a/Test/livevars/TwoDimensionalMap.bpl b/Test/livevars/TwoDimensionalMap.bpl
new file mode 100644
index 00000000..25e24b23
--- /dev/null
+++ b/Test/livevars/TwoDimensionalMap.bpl
@@ -0,0 +1,29 @@
+var k: int;

+var AllMaps__1: [int,int]int;

+

+procedure PoirotMain.Main_trace_1_trace_1()

+modifies k, AllMaps__1;

+{

+  var $tmp4: int;

+  var local_0: int;

+

+  lab0:

+    k := 1;

+    goto lab1, lab2;

+

+

+lab1:

+    assume k == 0;

+    goto lab3;

+

+lab2:

+    assume k == 1;

+    $tmp4 := local_0;

+    goto lab3;

+

+lab3:    

+    AllMaps__1[$tmp4,0] := 1;   

+    assert AllMaps__1[local_0,0] == 1;

+}

+

+

diff --git a/Test/livevars/runtest.bat b/Test/livevars/runtest.bat
index 3269a354..dbd3cb8c 100644
--- a/Test/livevars/runtest.bat
+++ b/Test/livevars/runtest.bat
@@ -8,4 +8,5 @@ rem set BGEXE=mono ..\..\Binaries\Boogie.exe
 %BGEXE% %* /noinfer /useArrayTheory daytona_bug2_ioctl_example_1.bpl

 %BGEXE% %* /noinfer /useArrayTheory daytona_bug2_ioctl_example_2.bpl

 %BGEXE% %* /noinfer /useArrayTheory stack_overflow.bpl

-

+%BGEXE% %* /noinfer /useArrayTheory NestedOneDimensionalMap.bpl

+%BGEXE% %* /noinfer /useArrayTheory TwoDimensionalMap.bpl