Fixed two bugs related to structs: now a struct that is declared without an

initial value is getting allocated. Also, deferring ctor calls within a struct
ctor do *not* result in an attempt to allocate a new struct and assign it to
"this".
Restart the temporary variable counter on entry to each method. (This makes
the regressions less noisy because a change in the number of temporaries
created for one method will not change the names of the temporaries in other
methods.)

5 files changed, 245 insertions, 309 deletions

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index 5df4b293..137d5776 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -520,7 +520,12 @@ namespace BytecodeTranslator
           }

         }

 

-        if (resolvedMethod.IsConstructor && resolvedMethod.ContainingTypeDefinition.IsStruct) {

+        var deferringCtorCall = resolvedMethod.IsConstructor && methodCall.ThisArgument is IThisReference;

+        // REVIEW!! Ask Herman: is the above test enough? The following test is used in FindCtorCall.IsDeferringCtor,

+        // but it doesn't work when the type is a struct S because then "this" has a type of "&S".

+          //&& TypeHelper.TypesAreEquivalent(resolvedMethod.ContainingType, methodCall.ThisArgument.Type);

+

+        if (resolvedMethod.IsConstructor && resolvedMethod.ContainingTypeDefinition.IsStruct && !deferringCtorCall) {

           handleStructConstructorCall(methodCall, methodCallToken, inexpr, outvars, thisExpr, proc);

           return;

         }

diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs
index fb7c1929..faa48773 100644
--- a/BCT/BytecodeTranslator/Sink.cs
+++ b/BCT/BytecodeTranslator/Sink.cs
@@ -18,6 +18,7 @@ using System.Diagnostics.Contracts;
 

 using Bpl = Microsoft.Boogie;

 using BytecodeTranslator.TranslationPlugins;

+using System.IO;

 

 

 namespace BytecodeTranslator {

@@ -217,9 +218,9 @@ namespace BytecodeTranslator {
       MethodParameter mp;

       ProcedureInfo procAndFormalMap;

       var sig = param.ContainingSignature;

-      // BUGBUG: If param's signature is not a method reference, then it doesn't have an interned

-      // key. The declaredMethods table needs to use ISignature for its keys.

-      var key = ((IMethodReference)sig).InternedKey;

+      // BUGBUG: If param's signature is not a method reference, then it can't be used as a key.

+      // The declaredMethods table needs to use ISignature for its keys.

+      var key = ((IMethodReference)sig);

       this.declaredMethods.TryGetValue(key, out procAndFormalMap);

       var formalMap = procAndFormalMap.FormalMap;

       formalMap.TryGetValue(param, out mp);

@@ -233,8 +234,7 @@ namespace BytecodeTranslator {
       var specializedField = field as ISpecializedFieldReference;

       if (specializedField != null)

         field = specializedField.UnspecializedVersion;

-      var key = field.InternedKey;

-      if (!this.declaredFields.TryGetValue(key, out v)) {

+      if (!this.declaredFields.TryGetValue(field, out v)) {

         v = this.Heap.CreateFieldVariable(field);

 

         var isExtern = this.assemblyBeingTranslated != null &&

@@ -244,16 +244,26 @@ namespace BytecodeTranslator {
           v.Attributes = attrib;

         }

 

-        this.declaredFields.Add(key, v);

+        this.declaredFields.Add(field, v);

         this.TranslatedProgram.TopLevelDeclarations.Add(v);

       }

       return v;

     }

 

+    class FieldComparer : IEqualityComparer<IFieldReference> {

+      public bool Equals(IFieldReference x, IFieldReference y) {

+        return x.InternedKey == y.InternedKey;

+      }

+

+      public int GetHashCode(IFieldReference obj) {

+        return (int)obj.InternedKey;

+      }

+    }

+

     /// <summary>

-    /// The keys to the table are the interned key of the field.

+    /// The keys to the table are the fields themselves, but the equality of keys is via their interned keys.

     /// </summary>

-    private Dictionary<uint, Bpl.Variable> declaredFields = new Dictionary<uint, Bpl.Variable>();

+    private Dictionary<IFieldReference, Bpl.Variable> declaredFields = new Dictionary<IFieldReference, Bpl.Variable>(new FieldComparer());

 

     public Bpl.Variable FindOrCreateEventVariable(IEventDefinition e) {

       Bpl.Variable v;

@@ -483,7 +493,7 @@ namespace BytecodeTranslator {
 

     public ProcedureInfo FindOrCreateProcedure(IMethodDefinition method) {

       ProcedureInfo procInfo;

-      var key = method.InternedKey;

+      var key = method;

 

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

         string MethodName = TranslationHelper.CreateUniqueMethodName(method);

@@ -692,8 +702,6 @@ namespace BytecodeTranslator {
       var key = structType.InternedKey;

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

         var typename = TranslationHelper.TurnStringIntoValidIdentifier(TypeHelper.GetTypeName(structType));

-        // The type can be generic and then there can be name clashes. So append the key to make it unique.

-        typename += key.ToString();

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

@@ -1049,12 +1057,24 @@ namespace BytecodeTranslator {
     private Dictionary<uint, Bpl.Function> declaredTypeFunctions = new Dictionary<uint, Bpl.Function>();

     private List<Bpl.Function> childFunctions = new List<Bpl.Function>();

 

+

+    class MethodComparer : IEqualityComparer<IMethodReference> {

+      public bool Equals(IMethodReference x, IMethodReference y) {

+        return x.InternedKey == y.InternedKey;

+      }

+

+      public int GetHashCode(IMethodReference obj) {

+        return (int)obj.InternedKey;

+      }

+    }

+

     /// <summary>

-    /// The keys to the table are the interned keys of the methods.

+    /// The keys to the table are the methods. (Equality on keys is determined by their InternedKey.)

     /// The values are pairs: first element is the procedure,

     /// second element is the formal map for the procedure

     /// </summary>

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

+    private Dictionary<IMethodReference, ProcedureInfo> declaredMethods = new Dictionary<IMethodReference, ProcedureInfo>(new MethodComparer());

+

     /// <summary>

     /// The values in this table are the procedures

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

@@ -1132,6 +1152,7 @@ namespace BytecodeTranslator {
     }

 

     public void BeginMethod(IMethodDefinition method) {

+      TranslationHelper.tmpVarCounter = 0; 

       this.BeginMethod(method.ContainingType);

       this.methodBeingTranslated = method;

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

@@ -1215,5 +1236,22 @@ namespace BytecodeTranslator {
     //  return !this.whiteList;

     //}

 

+

+    internal void CreateIdentifierCorrespondenceTable(string baseFileName) {

+      using (var writer = new StreamWriter(baseFileName + "_names.txt")) {

+        foreach (var pair in this.declaredMethods) {

+          var m = pair.Key;

+          var mName = MemberHelper.GetMethodSignature(m, NameFormattingOptions.DocumentationId);

+          var proc = pair.Value;

+          writer.WriteLine("{0}\t\t\t{1}", mName, proc.Decl.Name);

+        }

+        foreach (var pair in this.declaredFields) {

+          var f = pair.Key;

+          var fName = MemberHelper.GetMemberSignature(f, NameFormattingOptions.DocumentationId);

+          var variable = pair.Value;

+          writer.WriteLine("{0}\t\t\t{1}", fName, variable.Name);

+        }

+      }

+    }

   }

 }
\ No newline at end of file
diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs
index 40bc14b3..15f59a13 100644
--- a/BCT/BytecodeTranslator/StatementTraverser.cs
+++ b/BCT/BytecodeTranslator/StatementTraverser.cs
@@ -289,22 +289,27 @@ namespace BytecodeTranslator
 

     /// <summary>

     /// If the local declaration has an initial value, then generate the

-    /// statement "loc := e" from it. Otherwise ignore it.

+    /// statement "loc := e" from it. 

+    /// Special case: if "loc" is a struct, then treat it as a call to 

+    /// the default ctor.

+    /// Otherwise ignore it.

     /// </summary>

     public override void Visit(ILocalDeclarationStatement localDeclarationStatement) {

       var initVal = localDeclarationStatement.InitialValue;

-      if (initVal == null) return;

+      var typ = localDeclarationStatement.LocalVariable.Type;

+      var isStruct = TranslationHelper.IsStruct(typ);

+      if (initVal == null && !isStruct)

+        return;

       var boogieLocal = this.sink.FindOrCreateLocalVariable(localDeclarationStatement.LocalVariable);

       var boogieLocalExpr = Bpl.Expr.Ident(boogieLocal);

       var tok = localDeclarationStatement.Token();

-      var e = ExpressionFor(initVal);

+      Bpl.Expr e = null;

+      

 

-      var typ = initVal.Type;

-      var structCopy = TranslationHelper.IsStruct(typ) && !(initVal is IDefaultValue);

+      var structCopy = isStruct && initVal != null && !(initVal is IDefaultValue);

       // then a struct value of type S is being assigned: "lhs := s"

       // model this as the statement "call lhs := S..#copy_ctor(s)" that does the bit-wise copying

-      Bpl.DeclWithFormals proc = null;

-      if (structCopy) {

+      if (isStruct) {

         var defaultValue = new DefaultValue() {

           DefaultValueType = typ,

           Locations = new List<ILocation>(localDeclarationStatement.Locations),

@@ -312,9 +317,13 @@ namespace BytecodeTranslator
         };

         var e2 = ExpressionFor(defaultValue);

         StmtBuilder.Add(Bpl.Cmd.SimpleAssign(tok, boogieLocalExpr, e2));

-        proc = this.sink.FindOrCreateProcedureForStructCopy(typ);

-        StmtBuilder.Add(new Bpl.CallCmd(tok, proc.Name, new List<Bpl.Expr> { e, boogieLocalExpr, }, new List<Bpl.IdentifierExpr>()));

+        if (structCopy) {

+          var proc = this.sink.FindOrCreateProcedureForStructCopy(typ);

+          e = ExpressionFor(initVal);

+          StmtBuilder.Add(new Bpl.CallCmd(tok, proc.Name, new List<Bpl.Expr> { e, boogieLocalExpr, }, new List<Bpl.IdentifierExpr>()));

+        }

       } else {

+        e = ExpressionFor(initVal);

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

       }

       return;

diff --git a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
index e2e7b3ff..b03c319f 100644
--- a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
@@ -141,7 +141,21 @@ axiom (forall m: int, o: Ref, t: Type :: { $DelegateCons(m, o, t) } $DelegateRec
 

 axiom (forall m: int, o: Ref, t: Type :: { $DelegateCons(m, o, t) } $DelegateTypeParameters($DelegateCons(m, o, t)) == t);

 

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

+axiom (forall d: Delegate :: { MultisetEmpty[d] } MultisetEmpty[d] == 0);

+

+axiom (forall x: Delegate :: { MultisetSingleton(x) } MultisetSingleton(x)[x] == 1);

+

+axiom (forall x: Delegate, d: Delegate :: { MultisetSingleton(x)[d] } MultisetSingleton(x)[d] == (if x == d then 1 else 0));

+

+axiom (forall a: DelegateMultiset, b: DelegateMultiset, d: Delegate :: { MultisetPlus(a, b)[d] } MultisetPlus(a, b)[d] == a[d] + b[d]);

+

+axiom (forall a: DelegateMultiset, b: DelegateMultiset, d: Delegate :: { MultisetMinus(a, b)[d] } MultisetMinus(a, b)[d] == (if a[d] > b[d] then a[d] - b[d] else 0));

+

+axiom (forall a: DelegateMultiset, d: Delegate :: { MultisetPlus(a, MultisetSingleton(d)) } MultisetPlus(a, MultisetSingleton(d))[d] == a[d] + 1);

+

+axiom (forall a: DelegateMultiset, d: Delegate :: { MultisetMinus(a, MultisetSingleton(d)) } MultisetMinus(a, MultisetSingleton(d))[d] == (if a[d] > 0 then a[d] - 1 else 0));

+

+procedure {:inline 1} DelegateAdd(a: Ref, b: Ref) returns (c: Ref);

 

 

 

@@ -152,25 +166,21 @@ implementation DelegateAdd(a: Ref, b: Ref) returns (c: Ref)
     if (a == null)

     {

         c := b;

-        return;

     }

     else if (b == null)

     {

         c := a;

-        return;

     }

-

-    call d := GetFirstElement(b);

-    call c := Alloc();

-    $Head[c] := $Head[a];

-    $Next[c] := $Next[a];

-    $Delegate[c] := $Delegate[a];

-    call c := DelegateAddHelper(c, d);

+    else

+    {

+        call c := Alloc();

+        assume $Delegate(c) == MultisetPlus($Delegate(a), $Delegate(b));

+    }

 }

 

 

 

-procedure DelegateRemove(a: Ref, b: Ref) returns (c: Ref);

+procedure {:inline 1} DelegateRemove(a: Ref, b: Ref) returns (c: Ref);

 

 

 

@@ -181,113 +191,32 @@ implementation DelegateRemove(a: Ref, b: Ref) returns (c: Ref)
     if (a == null)

     {

         c := null;

-        return;

     }

     else if (b == null)

     {

         c := a;

-        return;

     }

-

-    call d := GetFirstElement(b);

-    call c := Alloc();

-    $Head[c] := $Head[a];

-    $Next[c] := $Next[a];

-    $Delegate[c] := $Delegate[a];

-    call c := DelegateRemoveHelper(c, d);

-}

-

-

-

-procedure GetFirstElement(i: Ref) returns (d: Delegate);

-

-

-

-implementation GetFirstElement(i: Ref) returns (d: Delegate)

-{

-  var first: Ref;

-

-    first := $Next[i][$Head[i]];

-    d := $Delegate[i][first];

-}

-

-

-

-procedure DelegateAddHelper(oldi: Ref, d: Delegate) returns (i: Ref);

-

-

-

-implementation DelegateAddHelper(oldi: Ref, d: Delegate) returns (i: Ref)

-{

-  var x: Ref;

-  var h: Ref;

-

-    if (oldi == null)

+    else if (MultisetMinus($Delegate(a), $Delegate(b)) == MultisetEmpty)

     {

-        call i := Alloc();

-        call x := Alloc();

-        $Head[i] := x;

-        $Next[i] := $Next[i][x := x];

+        c := null;

     }

     else

     {

-        i := oldi;

+        call c := Alloc();

+        assume $Delegate(c) == MultisetMinus($Delegate(a), $Delegate(b));

     }

-

-    h := $Head[i];

-    $Delegate[i] := $Delegate[i][h := d];

-    call x := Alloc();

-    $Next[i] := $Next[i][x := $Next[i][h]];

-    $Next[i] := $Next[i][h := x];

-    $Head[i] := x;

 }

 

 

 

-procedure DelegateRemoveHelper(oldi: Ref, d: Delegate) returns (i: Ref);

+procedure {:inline 1} DelegateCreate(d: Delegate) returns (c: Ref);

 

 

 

-implementation DelegateRemoveHelper(oldi: Ref, d: Delegate) returns (i: Ref)

+implementation DelegateCreate(d: Delegate) returns (c: Ref)

 {

-  var prev: Ref;

-  var iter: Ref;

-  var niter: Ref;

-

-    i := oldi;

-    if (i == null)

-    {

-        return;

-    }

-

-    prev := null;

-    iter := $Head[i];

-    while (true)

-    {

-        niter := $Next[i][iter];

-        if (niter == $Head[i])

-        {

-            break;

-        }

-

-        if ($Delegate[i][niter] == d)

-        {

-            prev := iter;

-        }

-

-        iter := niter;

-    }

-

-    if (prev == null)

-    {

-        return;

-    }

-

-    $Next[i] := $Next[i][prev := $Next[i][$Next[i][prev]]];

-    if ($Next[i][$Head[i]] == $Head[i])

-    {

-        i := null;

-    }

+    call c := Alloc();

+    assume $Delegate(c) == MultisetSingleton(d);

 }

 

 

@@ -395,6 +324,16 @@ function $ArrayLength(Ref) : int;
 

 type Delegate;

 

+type DelegateMultiset = [Delegate]int;

+

+const unique MultisetEmpty: DelegateMultiset;

+

+function MultisetSingleton(Delegate) : DelegateMultiset;

+

+function MultisetPlus(DelegateMultiset, DelegateMultiset) : DelegateMultiset;

+

+function MultisetMinus(DelegateMultiset, DelegateMultiset) : DelegateMultiset;

+

 type Field;

 

 type Box;

@@ -444,6 +383,8 @@ function RealTimes(Real, Real) : Real;
 

 function RealDivide(Real, Real) : Real;

 

+function RealModulus(Real, Real) : Real;

+

 function RealLessThan(Real, Real) : bool;

 

 function RealLessThanOrEqual(Real, Real) : bool;

@@ -476,11 +417,7 @@ function $DirectSubtype(Type, Type) : bool;
 

 function $DisjointSubtree(Type, Type) : bool;

 

-var $Head: [Ref]Ref;

-

-var $Next: [Ref][Ref]Ref;

-

-var $Delegate: [Ref][Ref]Delegate;

+function $Delegate(Ref) : DelegateMultiset;

 

 function $DelegateCons(int, Ref, Type) : Delegate;

 

@@ -708,7 +645,7 @@ procedure RegressionTestInput.CreateStruct.Create($this: Ref) returns ($result:
 

 

 

-procedure RegressionTestInput.S298.#default_ctor(this: Ref);

+procedure RegressionTestInput.S.#default_ctor(this: Ref);

 

 

 

@@ -730,16 +667,21 @@ const unique F$RegressionTestInput.S.b: Field;
 

 implementation RegressionTestInput.CreateStruct.Create($this: Ref) returns ($result: Ref)

 {

-  var $tmp0: Ref;

   var s: Ref;

+  var $tmp0: Ref;

+  var $tmp1: Ref;

   var $localExc: Ref;

   var $label: int;

 

-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 141} true;

     call $tmp0 := Alloc();

-    call RegressionTestInput.S298.#default_ctor($tmp0);

+    call RegressionTestInput.S.#default_ctor($tmp0);

     assume $DynamicType($tmp0) == RegressionTestInput.S$type;

     s := $tmp0;

+    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 141} true;

+    call $tmp1 := Alloc();

+    call RegressionTestInput.S.#default_ctor($tmp1);

+    assume $DynamicType($tmp1) == RegressionTestInput.S$type;

+    s := $tmp1;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 142} true;

     assert Box2Int(Read($Heap, s, F$RegressionTestInput.S.x)) == 0;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 143} true;

@@ -820,24 +762,24 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main1();
 implementation RegressionTestInput.ClassWithArrayTypes.Main1()

 {

   var s: Ref;

-  var $tmp1: Ref;

+  var $tmp0: Ref;

   var t: Ref;

-  var $tmp2: Ref;

+  var $tmp1: Ref;

   var $localExc: Ref;

   var $label: int;

 

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 86} true;

-    call $tmp1 := Alloc();

-    assume $ArrayLength($tmp1) == 1 * 5;

-    s := $tmp1;

+    call $tmp0 := Alloc();

+    assume $ArrayLength($tmp0) == 1 * 5;

+    s := $tmp0;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 87} true;

     $ArrayContents := $ArrayContents[s := $ArrayContents[s][0 := Int2Box(2)]];

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 88} true;

     assert Box2Int($ArrayContents[s][0]) == 2;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 90} true;

-    call $tmp2 := Alloc();

-    assume $ArrayLength($tmp2) == 1 * 4;

-    t := $tmp2;

+    call $tmp1 := Alloc();

+    assume $ArrayLength($tmp1) == 1 * 4;

+    t := $tmp1;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 91} true;

     $ArrayContents := $ArrayContents[t := $ArrayContents[t][0 := Int2Box(1)]];

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 92} true;

@@ -856,24 +798,24 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main2();
 

 implementation RegressionTestInput.ClassWithArrayTypes.Main2()

 {

-  var $tmp3: Ref;

+  var $tmp0: Ref;

   var t: Ref;

-  var $tmp4: Ref;

+  var $tmp1: Ref;

   var $localExc: Ref;

   var $label: int;

 

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 100} true;

-    call $tmp3 := Alloc();

-    assume $ArrayLength($tmp3) == 1 * 5;

-    F$RegressionTestInput.ClassWithArrayTypes.s := $tmp3;

+    call $tmp0 := Alloc();

+    assume $ArrayLength($tmp0) == 1 * 5;

+    F$RegressionTestInput.ClassWithArrayTypes.s := $tmp0;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 101} true;

     $ArrayContents := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s][0 := Int2Box(2)]];

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 102} true;

     assert Box2Int($ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s][0]) == 2;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 104} true;

-    call $tmp4 := Alloc();

-    assume $ArrayLength($tmp4) == 1 * 4;

-    t := $tmp4;

+    call $tmp1 := Alloc();

+    assume $ArrayLength($tmp1) == 1 * 4;

+    t := $tmp1;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 105} true;

     $ArrayContents := $ArrayContents[t := $ArrayContents[t][0 := Int2Box(1)]];

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 106} true;

@@ -1303,11 +1245,11 @@ implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int32($this:
 {

   var x: int;

   var CS$0$0000: Box;

-  var $tmp5: Ref;

+  var $tmp0: Ref;

   var __temp_2: Box;

   var __temp_3: Box;

-  var $tmp6: Box;

-  var $tmp7: Box;

+  var $tmp1: Box;

+  var $tmp2: Box;

   var y: Box;

   var $localExc: Ref;

   var $label: int;

@@ -1322,23 +1264,23 @@ implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int32($this:
 

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 188} true;

     CS$0$0000 := $DefaultBox;

-    call $tmp5 := Alloc();

-    $Heap := Write($Heap, $tmp5, $BoxField, Box2Box(CS$0$0000));

-    if ($tmp5 != null)

+    call $tmp0 := Alloc();

+    $Heap := Write($Heap, $tmp0, $BoxField, Box2Box(CS$0$0000));

+    if ($tmp0 != null)

     {

         CS$0$0000 := $DefaultBox;

         __temp_2 := CS$0$0000;

     }

     else

     {

-        call $tmp7 := System.Activator.CreateInstance``1(Child0($DynamicType($this)));

-        $tmp6 := Box2Box($tmp7);

+        call $tmp2 := System.Activator.CreateInstance``1(Child0($DynamicType($this)));

+        $tmp1 := Box2Box($tmp2);

         if ($Exception != null)

         {

             return;

         }

 

-        __temp_3 := $tmp6;

+        __temp_3 := $tmp1;

         __temp_2 := __temp_3;

     }

 

@@ -1378,7 +1320,7 @@ implementation T$RegressionTestInput.NestedGeneric.#cctor()
 

 

 

-implementation {:inline 1} RegressionTestInput.S298.#default_ctor(this: Ref)

+implementation {:inline 1} RegressionTestInput.S.#default_ctor(this: Ref)

 {

 }

 

@@ -1557,18 +1499,18 @@ procedure RegressionTestInput.Class0.NonVoid($this: Ref) returns ($result: int);
 

 implementation RegressionTestInput.Class0.NonVoid($this: Ref) returns ($result: int)

 {

-  var $tmp8: int;

+  var $tmp0: int;

   var $localExc: Ref;

   var $label: int;

 

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 34} true;

-    call $tmp8 := RegressionTestInput.Class0.StaticMethod$System.Int32(3);

+    call $tmp0 := RegressionTestInput.Class0.StaticMethod$System.Int32(3);

     if ($Exception != null)

     {

         return;

     }

 

-    $result := 3 + F$RegressionTestInput.Class0.StaticInt + $tmp8;

+    $result := 3 + F$RegressionTestInput.Class0.StaticInt + $tmp0;

     return;

 }

 

@@ -1661,19 +1603,19 @@ procedure RegressionTestInput.Class0.CallAsyncMethod$System.Int32($this: Ref, y$
 implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int32($this: Ref, y$in: int) returns ($result: int)

 {

   var y: int;

-  var $tmp9: int;

+  var $tmp0: int;

   var $localExc: Ref;

   var $label: int;

 

     y := y$in;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 60} true;

-    call {:async} $tmp9 := RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32($this, y);

+    call {:async} $tmp0 := RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32($this, y);

     if ($Exception != null)

     {

         return;

     }

 

-    $result := $tmp9;

+    $result := $tmp0;

     return;

 }

 

@@ -1782,12 +1724,12 @@ procedure RegressionTestInput.ClassWithBoolTypes.Main();
 

 implementation RegressionTestInput.ClassWithBoolTypes.Main()

 {

-  var $tmp10: bool;

+  var $tmp0: bool;

   var $localExc: Ref;

   var $label: int;

 

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 78} true;

-    call $tmp10 := RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(3, 4);

+    call $tmp0 := RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(3, 4);

     if ($Exception != null)

     {

         return;

diff --git a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
index 103d26bd..e52668d3 100644
--- a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
@@ -139,7 +139,21 @@ axiom (forall m: int, o: Ref, t: Type :: { $DelegateCons(m, o, t) } $DelegateRec
 

 axiom (forall m: int, o: Ref, t: Type :: { $DelegateCons(m, o, t) } $DelegateTypeParameters($DelegateCons(m, o, t)) == t);

 

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

+axiom (forall d: Delegate :: { MultisetEmpty[d] } MultisetEmpty[d] == 0);

+

+axiom (forall x: Delegate :: { MultisetSingleton(x) } MultisetSingleton(x)[x] == 1);

+

+axiom (forall x: Delegate, d: Delegate :: { MultisetSingleton(x)[d] } MultisetSingleton(x)[d] == (if x == d then 1 else 0));

+

+axiom (forall a: DelegateMultiset, b: DelegateMultiset, d: Delegate :: { MultisetPlus(a, b)[d] } MultisetPlus(a, b)[d] == a[d] + b[d]);

+

+axiom (forall a: DelegateMultiset, b: DelegateMultiset, d: Delegate :: { MultisetMinus(a, b)[d] } MultisetMinus(a, b)[d] == (if a[d] > b[d] then a[d] - b[d] else 0));

+

+axiom (forall a: DelegateMultiset, d: Delegate :: { MultisetPlus(a, MultisetSingleton(d)) } MultisetPlus(a, MultisetSingleton(d))[d] == a[d] + 1);

+

+axiom (forall a: DelegateMultiset, d: Delegate :: { MultisetMinus(a, MultisetSingleton(d)) } MultisetMinus(a, MultisetSingleton(d))[d] == (if a[d] > 0 then a[d] - 1 else 0));

+

+procedure {:inline 1} DelegateAdd(a: Ref, b: Ref) returns (c: Ref);

 

 

 

@@ -150,25 +164,21 @@ implementation DelegateAdd(a: Ref, b: Ref) returns (c: Ref)
     if (a == null)

     {

         c := b;

-        return;

     }

     else if (b == null)

     {

         c := a;

-        return;

     }

-

-    call d := GetFirstElement(b);

-    call c := Alloc();

-    $Head[c] := $Head[a];

-    $Next[c] := $Next[a];

-    $Delegate[c] := $Delegate[a];

-    call c := DelegateAddHelper(c, d);

+    else

+    {

+        call c := Alloc();

+        assume $Delegate(c) == MultisetPlus($Delegate(a), $Delegate(b));

+    }

 }

 

 

 

-procedure DelegateRemove(a: Ref, b: Ref) returns (c: Ref);

+procedure {:inline 1} DelegateRemove(a: Ref, b: Ref) returns (c: Ref);

 

 

 

@@ -179,113 +189,32 @@ implementation DelegateRemove(a: Ref, b: Ref) returns (c: Ref)
     if (a == null)

     {

         c := null;

-        return;

     }

     else if (b == null)

     {

         c := a;

-        return;

     }

-

-    call d := GetFirstElement(b);

-    call c := Alloc();

-    $Head[c] := $Head[a];

-    $Next[c] := $Next[a];

-    $Delegate[c] := $Delegate[a];

-    call c := DelegateRemoveHelper(c, d);

-}

-

-

-

-procedure GetFirstElement(i: Ref) returns (d: Delegate);

-

-

-

-implementation GetFirstElement(i: Ref) returns (d: Delegate)

-{

-  var first: Ref;

-

-    first := $Next[i][$Head[i]];

-    d := $Delegate[i][first];

-}

-

-

-

-procedure DelegateAddHelper(oldi: Ref, d: Delegate) returns (i: Ref);

-

-

-

-implementation DelegateAddHelper(oldi: Ref, d: Delegate) returns (i: Ref)

-{

-  var x: Ref;

-  var h: Ref;

-

-    if (oldi == null)

+    else if (MultisetMinus($Delegate(a), $Delegate(b)) == MultisetEmpty)

     {

-        call i := Alloc();

-        call x := Alloc();

-        $Head[i] := x;

-        $Next[i] := $Next[i][x := x];

+        c := null;

     }

     else

     {

-        i := oldi;

+        call c := Alloc();

+        assume $Delegate(c) == MultisetMinus($Delegate(a), $Delegate(b));

     }

-

-    h := $Head[i];

-    $Delegate[i] := $Delegate[i][h := d];

-    call x := Alloc();

-    $Next[i] := $Next[i][x := $Next[i][h]];

-    $Next[i] := $Next[i][h := x];

-    $Head[i] := x;

 }

 

 

 

-procedure DelegateRemoveHelper(oldi: Ref, d: Delegate) returns (i: Ref);

+procedure {:inline 1} DelegateCreate(d: Delegate) returns (c: Ref);

 

 

 

-implementation DelegateRemoveHelper(oldi: Ref, d: Delegate) returns (i: Ref)

+implementation DelegateCreate(d: Delegate) returns (c: Ref)

 {

-  var prev: Ref;

-  var iter: Ref;

-  var niter: Ref;

-

-    i := oldi;

-    if (i == null)

-    {

-        return;

-    }

-

-    prev := null;

-    iter := $Head[i];

-    while (true)

-    {

-        niter := $Next[i][iter];

-        if (niter == $Head[i])

-        {

-            break;

-        }

-

-        if ($Delegate[i][niter] == d)

-        {

-            prev := iter;

-        }

-

-        iter := niter;

-    }

-

-    if (prev == null)

-    {

-        return;

-    }

-

-    $Next[i] := $Next[i][prev := $Next[i][$Next[i][prev]]];

-    if ($Next[i][$Head[i]] == $Head[i])

-    {

-        i := null;

-    }

+    call c := Alloc();

+    assume $Delegate(c) == MultisetSingleton(d);

 }

 

 

@@ -381,6 +310,16 @@ function $ArrayLength(Ref) : int;
 

 type Delegate;

 

+type DelegateMultiset = [Delegate]int;

+

+const unique MultisetEmpty: DelegateMultiset;

+

+function MultisetSingleton(Delegate) : DelegateMultiset;

+

+function MultisetPlus(DelegateMultiset, DelegateMultiset) : DelegateMultiset;

+

+function MultisetMinus(DelegateMultiset, DelegateMultiset) : DelegateMultiset;

+

 type Field;

 

 type Box;

@@ -430,6 +369,8 @@ function RealTimes(Real, Real) : Real;
 

 function RealDivide(Real, Real) : Real;

 

+function RealModulus(Real, Real) : Real;

+

 function RealLessThan(Real, Real) : bool;

 

 function RealLessThanOrEqual(Real, Real) : bool;

@@ -462,11 +403,7 @@ function $DirectSubtype(Type, Type) : bool;
 

 function $DisjointSubtree(Type, Type) : bool;

 

-var $Head: [Ref]Ref;

-

-var $Next: [Ref][Ref]Ref;

-

-var $Delegate: [Ref][Ref]Delegate;

+function $Delegate(Ref) : DelegateMultiset;

 

 function $DelegateCons(int, Ref, Type) : Delegate;

 

@@ -694,7 +631,7 @@ procedure RegressionTestInput.CreateStruct.Create($this: Ref) returns ($result:
 

 

 

-procedure RegressionTestInput.S298.#default_ctor(this: Ref);

+procedure RegressionTestInput.S.#default_ctor(this: Ref);

 

 

 

@@ -716,16 +653,21 @@ var F$RegressionTestInput.S.b: [Ref]bool;
 

 implementation RegressionTestInput.CreateStruct.Create($this: Ref) returns ($result: Ref)

 {

-  var $tmp0: Ref;

   var s: Ref;

+  var $tmp0: Ref;

+  var $tmp1: Ref;

   var $localExc: Ref;

   var $label: int;

 

-    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 141} true;

     call $tmp0 := Alloc();

-    call RegressionTestInput.S298.#default_ctor($tmp0);

+    call RegressionTestInput.S.#default_ctor($tmp0);

     assume $DynamicType($tmp0) == RegressionTestInput.S$type;

     s := $tmp0;

+    assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 141} true;

+    call $tmp1 := Alloc();

+    call RegressionTestInput.S.#default_ctor($tmp1);

+    assume $DynamicType($tmp1) == RegressionTestInput.S$type;

+    s := $tmp1;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 142} true;

     assert F$RegressionTestInput.S.x[s] == 0;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 143} true;

@@ -806,24 +748,24 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main1();
 implementation RegressionTestInput.ClassWithArrayTypes.Main1()

 {

   var s: Ref;

-  var $tmp1: Ref;

+  var $tmp0: Ref;

   var t: Ref;

-  var $tmp2: Ref;

+  var $tmp1: Ref;

   var $localExc: Ref;

   var $label: int;

 

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 86} true;

-    call $tmp1 := Alloc();

-    assume $ArrayLength($tmp1) == 1 * 5;

-    s := $tmp1;

+    call $tmp0 := Alloc();

+    assume $ArrayLength($tmp0) == 1 * 5;

+    s := $tmp0;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 87} true;

     $ArrayContents := $ArrayContents[s := $ArrayContents[s][0 := Int2Box(2)]];

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 88} true;

     assert Box2Int($ArrayContents[s][0]) == 2;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 90} true;

-    call $tmp2 := Alloc();

-    assume $ArrayLength($tmp2) == 1 * 4;

-    t := $tmp2;

+    call $tmp1 := Alloc();

+    assume $ArrayLength($tmp1) == 1 * 4;

+    t := $tmp1;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 91} true;

     $ArrayContents := $ArrayContents[t := $ArrayContents[t][0 := Int2Box(1)]];

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 92} true;

@@ -842,24 +784,24 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main2();
 

 implementation RegressionTestInput.ClassWithArrayTypes.Main2()

 {

-  var $tmp3: Ref;

+  var $tmp0: Ref;

   var t: Ref;

-  var $tmp4: Ref;

+  var $tmp1: Ref;

   var $localExc: Ref;

   var $label: int;

 

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 100} true;

-    call $tmp3 := Alloc();

-    assume $ArrayLength($tmp3) == 1 * 5;

-    F$RegressionTestInput.ClassWithArrayTypes.s := $tmp3;

+    call $tmp0 := Alloc();

+    assume $ArrayLength($tmp0) == 1 * 5;

+    F$RegressionTestInput.ClassWithArrayTypes.s := $tmp0;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 101} true;

     $ArrayContents := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s][0 := Int2Box(2)]];

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 102} true;

     assert Box2Int($ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s][0]) == 2;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 104} true;

-    call $tmp4 := Alloc();

-    assume $ArrayLength($tmp4) == 1 * 4;

-    t := $tmp4;

+    call $tmp1 := Alloc();

+    assume $ArrayLength($tmp1) == 1 * 4;

+    t := $tmp1;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 105} true;

     $ArrayContents := $ArrayContents[t := $ArrayContents[t][0 := Int2Box(1)]];

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 106} true;

@@ -1289,11 +1231,11 @@ implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int32($this:
 {

   var x: int;

   var CS$0$0000: Box;

-  var $tmp5: Ref;

+  var $tmp0: Ref;

   var __temp_2: Box;

   var __temp_3: Box;

-  var $tmp6: Box;

-  var $tmp7: Box;

+  var $tmp1: Box;

+  var $tmp2: Box;

   var y: Box;

   var $localExc: Ref;

   var $label: int;

@@ -1308,23 +1250,23 @@ implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int32($this:
 

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 188} true;

     CS$0$0000 := $DefaultBox;

-    call $tmp5 := Alloc();

-    $BoxField[$tmp5] := Box2Box(CS$0$0000);

-    if ($tmp5 != null)

+    call $tmp0 := Alloc();

+    $BoxField[$tmp0] := Box2Box(CS$0$0000);

+    if ($tmp0 != null)

     {

         CS$0$0000 := $DefaultBox;

         __temp_2 := CS$0$0000;

     }

     else

     {

-        call $tmp7 := System.Activator.CreateInstance``1(Child0($DynamicType($this)));

-        $tmp6 := Box2Box($tmp7);

+        call $tmp2 := System.Activator.CreateInstance``1(Child0($DynamicType($this)));

+        $tmp1 := Box2Box($tmp2);

         if ($Exception != null)

         {

             return;

         }

 

-        __temp_3 := $tmp6;

+        __temp_3 := $tmp1;

         __temp_2 := __temp_3;

     }

 

@@ -1364,7 +1306,7 @@ implementation T$RegressionTestInput.NestedGeneric.#cctor()
 

 

 

-implementation {:inline 1} RegressionTestInput.S298.#default_ctor(this: Ref)

+implementation {:inline 1} RegressionTestInput.S.#default_ctor(this: Ref)

 {

 }

 

@@ -1543,18 +1485,18 @@ procedure RegressionTestInput.Class0.NonVoid($this: Ref) returns ($result: int);
 

 implementation RegressionTestInput.Class0.NonVoid($this: Ref) returns ($result: int)

 {

-  var $tmp8: int;

+  var $tmp0: int;

   var $localExc: Ref;

   var $label: int;

 

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 34} true;

-    call $tmp8 := RegressionTestInput.Class0.StaticMethod$System.Int32(3);

+    call $tmp0 := RegressionTestInput.Class0.StaticMethod$System.Int32(3);

     if ($Exception != null)

     {

         return;

     }

 

-    $result := 3 + F$RegressionTestInput.Class0.StaticInt + $tmp8;

+    $result := 3 + F$RegressionTestInput.Class0.StaticInt + $tmp0;

     return;

 }

 

@@ -1647,19 +1589,19 @@ procedure RegressionTestInput.Class0.CallAsyncMethod$System.Int32($this: Ref, y$
 implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int32($this: Ref, y$in: int) returns ($result: int)

 {

   var y: int;

-  var $tmp9: int;

+  var $tmp0: int;

   var $localExc: Ref;

   var $label: int;

 

     y := y$in;

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 60} true;

-    call {:async} $tmp9 := RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32($this, y);

+    call {:async} $tmp0 := RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32($this, y);

     if ($Exception != null)

     {

         return;

     }

 

-    $result := $tmp9;

+    $result := $tmp0;

     return;

 }

 

@@ -1768,12 +1710,12 @@ procedure RegressionTestInput.ClassWithBoolTypes.Main();
 

 implementation RegressionTestInput.ClassWithBoolTypes.Main()

 {

-  var $tmp10: bool;

+  var $tmp0: bool;

   var $localExc: Ref;

   var $label: int;

 

     assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 78} true;

-    call $tmp10 := RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(3, 4);

+    call $tmp0 := RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(3, 4);

     if ($Exception != null)

     {

         return;