From 5da13c0983715868089f49ca38855816e5faa3c7 Mon Sep 17 00:00:00 2001 From: Mike Barnett Date: Wed, 3 Aug 2011 13:18:53 -0700 Subject: Increase the name mangling to avoid name clashes in the Boogie program. In IL, members of a type can have the same name. --- BCT/BytecodeTranslator/ExpressionTraverser.cs | 2 +- BCT/BytecodeTranslator/Heap.cs | 3 + BCT/BytecodeTranslator/HeapFactory.cs | 6 + BCT/BytecodeTranslator/Program.cs | 5 +- BCT/BytecodeTranslator/Sink.cs | 8 +- BCT/BytecodeTranslator/TranslationHelper.cs | 1 + .../TranslationTest/GeneralHeapInput.txt | 394 ++++++++++----------- .../TranslationTest/SplitFieldsHeapInput.txt | 314 ++++++++-------- 8 files changed, 375 insertions(+), 358 deletions(-) diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs index eb4b3672..ea171b25 100644 --- a/BCT/BytecodeTranslator/ExpressionTraverser.cs +++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs @@ -949,7 +949,7 @@ namespace BytecodeTranslator var a = this.sink.CreateFreshLocal(creationAST.Type); sink.AddDelegate(type.ResolvedType, methodToCall.ResolvedMethod); - Bpl.Constant constant = sink.FindOrAddDelegateMethodConstant(methodToCall.ResolvedMethod); + Bpl.Constant constant = sink.FindOrCreateDelegateMethodConstant(methodToCall.ResolvedMethod); Bpl.Expr methodExpr = Bpl.Expr.Ident(constant); Bpl.Expr instanceExpr = TranslatedExpressions.Pop(); diff --git a/BCT/BytecodeTranslator/Heap.cs b/BCT/BytecodeTranslator/Heap.cs index 664db230..751d8baa 100644 --- a/BCT/BytecodeTranslator/Heap.cs +++ b/BCT/BytecodeTranslator/Heap.cs @@ -207,6 +207,9 @@ namespace BytecodeTranslator { Bpl.Variable v; string fieldname = TypeHelper.GetTypeName(field.ContainingType) + "." + field.Name.Value; fieldname = TranslationHelper.TurnStringIntoValidIdentifier(fieldname); + // Need to append something to the name to avoid name clashes with other members (of a different + // type) that have the same name. + fieldname += "$field"; Bpl.IToken tok = field.Token(); if (field.IsStatic) { diff --git a/BCT/BytecodeTranslator/HeapFactory.cs b/BCT/BytecodeTranslator/HeapFactory.cs index 1f9518b5..d1c6ec84 100644 --- a/BCT/BytecodeTranslator/HeapFactory.cs +++ b/BCT/BytecodeTranslator/HeapFactory.cs @@ -238,6 +238,10 @@ namespace BytecodeTranslator { { string typename = TypeHelper.GetTypeName(type); typename = TranslationHelper.TurnStringIntoValidIdentifier(typename); + // Need to append something to the name to avoid name clashes with other members (of a different + // type) that have the same name. + typename += "$type"; + Bpl.IToken tok = type.Token(); Bpl.TypedIdent tident = new Bpl.TypedIdent(tok, typename, this.TypeType); Bpl.Constant v = new Bpl.Constant(tok, tident, true /*unique*/, parents, false, null); @@ -248,6 +252,8 @@ namespace BytecodeTranslator { System.Diagnostics.Debug.Assert(parameterCount > 0); string typename = TypeHelper.GetTypeName(type); typename = TranslationHelper.TurnStringIntoValidIdentifier(typename); + // Need to append something to the name to avoid name clashes. + typename += "$type"; Bpl.IToken tok = type.Token(); Bpl.VariableSeq inputs = new Bpl.VariableSeq(); for (int i = 0; i < parameterCount; i++) { diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs index be363277..18d735af 100644 --- a/BCT/BytecodeTranslator/Program.cs +++ b/BCT/BytecodeTranslator/Program.cs @@ -432,9 +432,10 @@ namespace BytecodeTranslator { for (index = 0; index < dispatchProcOutvars.Length; index++) { outs.Add(Bpl.Expr.Ident(dispatchProcOutvars[index])); } - Bpl.Constant c = sink.FindOrAddDelegateMethodConstant(defn); + Bpl.Constant c = sink.FindOrCreateDelegateMethodConstant(defn); + var procInfo = sink.FindOrCreateProcedure(defn); Bpl.Expr bexpr = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq, Bpl.Expr.Ident(method), Bpl.Expr.Ident(c)); - Bpl.CallCmd callCmd = new Bpl.CallCmd(token, c.Name, ins, outs); + Bpl.CallCmd callCmd = new Bpl.CallCmd(token, procInfo.Decl.Name, ins, outs); ifCmd = BuildIfCmd(bexpr, callCmd, ifCmd); } Bpl.StmtListBuilder ifStmtBuilder = new Bpl.StmtListBuilder(); diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs index 5a4de710..b2c1177e 100644 --- a/BCT/BytecodeTranslator/Sink.cs +++ b/BCT/BytecodeTranslator/Sink.cs @@ -425,6 +425,10 @@ namespace BytecodeTranslator { if (!this.declaredMethods.TryGetValue(key, out procInfo)) { string MethodName = TranslationHelper.CreateUniqueMethodName(method); + // The method can be generic (or have a parameter whose type is a type parameter of the method's + // containing class) and then there can be name clashes. + MethodName += key.ToString(); + if (this.initiallyDeclaredProcedures.TryGetValue(MethodName, out procInfo)) return procInfo; Bpl.Formal thisVariable = null; @@ -636,6 +640,8 @@ 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); @@ -1105,7 +1111,7 @@ namespace BytecodeTranslator { private Dictionary delegateMethods = new Dictionary(); internal IContractAwareHost host; - public Bpl.Constant FindOrAddDelegateMethodConstant(IMethodDefinition defn) + public Bpl.Constant FindOrCreateDelegateMethodConstant(IMethodDefinition defn) { if (delegateMethods.ContainsKey(defn)) return delegateMethods[defn]; diff --git a/BCT/BytecodeTranslator/TranslationHelper.cs b/BCT/BytecodeTranslator/TranslationHelper.cs index ad264c48..a17165ee 100644 --- a/BCT/BytecodeTranslator/TranslationHelper.cs +++ b/BCT/BytecodeTranslator/TranslationHelper.cs @@ -127,6 +127,7 @@ namespace BytecodeTranslator { s = s.Replace("[0:,0:,0:,0:,0:]", "5DArray"); s = s.Replace('!', '$'); s = s.Replace('*', '$'); + s = s.Replace('+', '$'); s = s.Replace('(', '$'); s = s.Replace(')', '$'); s = s.Replace(',', '$'); diff --git a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt index d33b6a17..a0f72ae1 100644 --- a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt @@ -480,23 +480,23 @@ var $Receiver: [Ref][Ref]Ref; var {:thread_local} $Exception: Ref; -const unique RegressionTestInput.RealNumbers: Type; +const unique RegressionTestInput.RealNumbers$type: Type; -const {:extern} unique System.Object: Type; +const {:extern} unique System.Object$type: Type; -axiom $Subtype(RegressionTestInput.RealNumbers, System.Object); +axiom $Subtype(RegressionTestInput.RealNumbers$type, System.Object$type); -axiom $DisjointSubtree(RegressionTestInput.RealNumbers, System.Object); +axiom $DisjointSubtree(RegressionTestInput.RealNumbers$type, System.Object$type); -procedure RegressionTestInput.RealNumbers.WriteDouble$System.Double($this: Ref, d$in: Real); +procedure RegressionTestInput.RealNumbers.WriteDouble$System.Double3($this: Ref, d$in: Real); -procedure {:extern} System.Console.WriteLine$System.Double(value$in: Real); +procedure {:extern} System.Console.WriteLine$System.Double43(value$in: Real); -implementation RegressionTestInput.RealNumbers.WriteDouble$System.Double($this: Ref, d$in: Real) +implementation RegressionTestInput.RealNumbers.WriteDouble$System.Double3($this: Ref, d$in: Real) { var d: Real; var $localExc: Ref; @@ -504,7 +504,7 @@ implementation RegressionTestInput.RealNumbers.WriteDouble$System.Double($this: d := d$in; assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 162} true; - call System.Console.WriteLine$System.Double(d); + call System.Console.WriteLine$System.Double43(d); if ($Exception != null) { return; @@ -516,11 +516,11 @@ implementation RegressionTestInput.RealNumbers.WriteDouble$System.Double($this: -procedure RegressionTestInput.RealNumbers.ObjectToDouble$System.Object($this: Ref, o$in: Ref); +procedure RegressionTestInput.RealNumbers.ObjectToDouble$System.Object4($this: Ref, o$in: Ref); -implementation RegressionTestInput.RealNumbers.ObjectToDouble$System.Object($this: Ref, o$in: Ref) +implementation RegressionTestInput.RealNumbers.ObjectToDouble$System.Object4($this: Ref, o$in: Ref) { var o: Ref; var $localExc: Ref; @@ -528,7 +528,7 @@ implementation RegressionTestInput.RealNumbers.ObjectToDouble$System.Object($thi o := o$in; assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 165} true; - call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, Box2Real(Read($Heap, o, $BoxField))); + call RegressionTestInput.RealNumbers.WriteDouble$System.Double3($this, Box2Real(Read($Heap, o, $BoxField))); if ($Exception != null) { return; @@ -540,7 +540,7 @@ implementation RegressionTestInput.RealNumbers.ObjectToDouble$System.Object($thi -procedure RegressionTestInput.RealNumbers.RealOperations($this: Ref); +procedure RegressionTestInput.RealNumbers.RealOperations5($this: Ref); @@ -548,7 +548,7 @@ const unique $real_literal_3_0: Real; const unique $real_literal_4_0: Real; -implementation RegressionTestInput.RealNumbers.RealOperations($this: Ref) +implementation RegressionTestInput.RealNumbers.RealOperations5($this: Ref) { var d: Real; var d2: Real; @@ -560,28 +560,28 @@ implementation RegressionTestInput.RealNumbers.RealOperations($this: Ref) assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 169} true; d2 := $real_literal_4_0; assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 170} true; - call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealPlus(d, d2)); + call RegressionTestInput.RealNumbers.WriteDouble$System.Double3($this, RealPlus(d, d2)); if ($Exception != null) { return; } assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 171} true; - call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealMinus(d, d2)); + call RegressionTestInput.RealNumbers.WriteDouble$System.Double3($this, RealMinus(d, d2)); if ($Exception != null) { return; } assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 172} true; - call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealTimes(d, d2)); + call RegressionTestInput.RealNumbers.WriteDouble$System.Double3($this, RealTimes(d, d2)); if ($Exception != null) { return; } assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 173} true; - call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealDivide(d, d2)); + call RegressionTestInput.RealNumbers.WriteDouble$System.Double3($this, RealDivide(d, d2)); if ($Exception != null) { return; @@ -593,20 +593,20 @@ implementation RegressionTestInput.RealNumbers.RealOperations($this: Ref) -procedure RegressionTestInput.RealNumbers.#ctor($this: Ref); +procedure RegressionTestInput.RealNumbers.#ctor6($this: Ref); -procedure {:extern} System.Object.#ctor($this: Ref); +procedure {:extern} System.Object.#ctor44($this: Ref); -implementation RegressionTestInput.RealNumbers.#ctor($this: Ref) +implementation RegressionTestInput.RealNumbers.#ctor6($this: Ref) { var $localExc: Ref; var $label: int; - call System.Object.#ctor($this); + call System.Object.#ctor44($this); if ($Exception != null) { return; @@ -627,45 +627,45 @@ implementation RegressionTestInput.RealNumbers.#cctor() -const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap: Type; +const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap$type: Type; -axiom $Subtype(RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap, System.Object); +axiom $Subtype(RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap$type, System.Object$type); -axiom $DisjointSubtree(RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap, System.Object); +axiom $DisjointSubtree(RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap$type, System.Object$type); -const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x: Field; +const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x$field: Field; -const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y: Field; +const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y$field: Field; -procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M($this: Ref); +procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M7($this: Ref); -implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M($this: Ref) +implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M7($this: Ref) { var $localExc: Ref; var $label: int; assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 130} true; - $Heap := Write($Heap, $this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y, Int2Box(Box2Int(Read($Heap, $this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x)))); + $Heap := Write($Heap, $this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y$field, Int2Box(Box2Int(Read($Heap, $this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x$field)))); assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 131} true; return; } -procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor($this: Ref); +procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor8($this: Ref); -implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor($this: Ref) +implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor8($this: Ref) { var $localExc: Ref; var $label: int; - $Heap := Write($Heap, $this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x, Int2Box(0)); - $Heap := Write($Heap, $this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y, Int2Box(0)); - call System.Object.#ctor($this); + $Heap := Write($Heap, $this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x$field, Int2Box(0)); + $Heap := Write($Heap, $this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y$field, Int2Box(0)); + call System.Object.#ctor44($this); if ($Exception != null) { return; @@ -686,37 +686,37 @@ implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor() -const unique RegressionTestInput.CreateStruct: Type; +const unique RegressionTestInput.CreateStruct$type: Type; -axiom $Subtype(RegressionTestInput.CreateStruct, System.Object); +axiom $Subtype(RegressionTestInput.CreateStruct$type, System.Object$type); -axiom $DisjointSubtree(RegressionTestInput.CreateStruct, System.Object); +axiom $DisjointSubtree(RegressionTestInput.CreateStruct$type, System.Object$type); -procedure RegressionTestInput.CreateStruct.Create($this: Ref) returns ($result: Ref); +procedure RegressionTestInput.CreateStruct.Create9($this: Ref) returns ($result: Ref); -procedure RegressionTestInput.S.#default_ctor(this: Ref); +procedure RegressionTestInput.S298.#default_ctor(this: Ref); -const unique RegressionTestInput.S: Type; +const unique RegressionTestInput.S$type: Type; -const {:extern} unique System.ValueType: Type; +const {:extern} unique System.ValueType$type: Type; -axiom $Subtype(System.ValueType, System.Object); +axiom $Subtype(System.ValueType$type, System.Object$type); -axiom $DisjointSubtree(System.ValueType, System.Object); +axiom $DisjointSubtree(System.ValueType$type, System.Object$type); -axiom $Subtype(RegressionTestInput.S, System.ValueType); +axiom $Subtype(RegressionTestInput.S$type, System.ValueType$type); -axiom $DisjointSubtree(RegressionTestInput.S, System.ValueType); +axiom $DisjointSubtree(RegressionTestInput.S$type, System.ValueType$type); -const unique RegressionTestInput.S.x: Field; +const unique RegressionTestInput.S.x$field: Field; -const unique RegressionTestInput.S.b: Field; +const unique RegressionTestInput.S.b$field: Field; -implementation RegressionTestInput.CreateStruct.Create($this: Ref) returns ($result: Ref) +implementation RegressionTestInput.CreateStruct.Create9($this: Ref) returns ($result: Ref) { var $tmp0: Ref; var s: Ref; @@ -725,13 +725,13 @@ implementation RegressionTestInput.CreateStruct.Create($this: Ref) returns ($res assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 141} true; call $tmp0 := Alloc(); - call RegressionTestInput.S.#default_ctor($tmp0); - assume $DynamicType($tmp0) == RegressionTestInput.S; + call RegressionTestInput.S298.#default_ctor($tmp0); + assume $DynamicType($tmp0) == RegressionTestInput.S$type; s := $tmp0; assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 142} true; - assert Box2Int(Read($Heap, s, RegressionTestInput.S.x)) == 0; + assert Box2Int(Read($Heap, s, RegressionTestInput.S.x$field)) == 0; assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 143} true; - assert !Box2Bool(Read($Heap, s, RegressionTestInput.S.b)); + assert !Box2Bool(Read($Heap, s, RegressionTestInput.S.b$field)); assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 145} true; $result := s; return; @@ -739,11 +739,11 @@ implementation RegressionTestInput.CreateStruct.Create($this: Ref) returns ($res -procedure RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInput.S($this: Ref, s$in: Ref) returns ($result: Ref); +procedure RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInput.S10($this: Ref, s$in: Ref) returns ($result: Ref); -implementation RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInput.S($this: Ref, s$in: Ref) returns ($result: Ref) +implementation RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInput.S10($this: Ref, s$in: Ref) returns ($result: Ref) { var s: Ref; var $localExc: Ref; @@ -751,9 +751,9 @@ implementation RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTes s := s$in; assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 147} true; - $Heap := Write($Heap, s, RegressionTestInput.S.x, Int2Box(3)); + $Heap := Write($Heap, s, RegressionTestInput.S.x$field, Int2Box(3)); assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 148} true; - assert Box2Int(Read($Heap, s, RegressionTestInput.S.x)) == 3; + assert Box2Int(Read($Heap, s, RegressionTestInput.S.x$field)) == 3; assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 150} true; $result := s; return; @@ -761,16 +761,16 @@ implementation RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTes -procedure RegressionTestInput.CreateStruct.#ctor($this: Ref); +procedure RegressionTestInput.CreateStruct.#ctor11($this: Ref); -implementation RegressionTestInput.CreateStruct.#ctor($this: Ref) +implementation RegressionTestInput.CreateStruct.#ctor11($this: Ref) { var $localExc: Ref; var $label: int; - call System.Object.#ctor($this); + call System.Object.#ctor44($this); if ($Exception != null) { return; @@ -791,21 +791,21 @@ implementation RegressionTestInput.CreateStruct.#cctor() -const unique RegressionTestInput.ClassWithArrayTypes: Type; +const unique RegressionTestInput.ClassWithArrayTypes$type: Type; -axiom $Subtype(RegressionTestInput.ClassWithArrayTypes, System.Object); +axiom $Subtype(RegressionTestInput.ClassWithArrayTypes$type, System.Object$type); -axiom $DisjointSubtree(RegressionTestInput.ClassWithArrayTypes, System.Object); +axiom $DisjointSubtree(RegressionTestInput.ClassWithArrayTypes$type, System.Object$type); -var RegressionTestInput.ClassWithArrayTypes.s: Ref; +var RegressionTestInput.ClassWithArrayTypes.s$field: Ref; -const unique RegressionTestInput.ClassWithArrayTypes.a: Field; +const unique RegressionTestInput.ClassWithArrayTypes.a$field: Field; -procedure RegressionTestInput.ClassWithArrayTypes.Main1(); +procedure RegressionTestInput.ClassWithArrayTypes.Main112(); -implementation RegressionTestInput.ClassWithArrayTypes.Main1() +implementation RegressionTestInput.ClassWithArrayTypes.Main112() { var s: Ref; var $tmp1: Ref; @@ -838,11 +838,11 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main1() -procedure RegressionTestInput.ClassWithArrayTypes.Main2(); +procedure RegressionTestInput.ClassWithArrayTypes.Main213(); -implementation RegressionTestInput.ClassWithArrayTypes.Main2() +implementation RegressionTestInput.ClassWithArrayTypes.Main213() { var $tmp3: Ref; var t: Ref; @@ -853,11 +853,11 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main2() assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 100} true; call $tmp3 := Alloc(); assume $ArrayLength($tmp3) == 1 * 5; - RegressionTestInput.ClassWithArrayTypes.s := $tmp3; + RegressionTestInput.ClassWithArrayTypes.s$field := $tmp3; assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 101} true; - $ArrayContents := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0 := Int2Box(2)]]; + $ArrayContents := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s$field := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s$field][0 := Int2Box(2)]]; assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 102} true; - assert Box2Int($ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0]) == 2; + assert Box2Int($ArrayContents[RegressionTestInput.ClassWithArrayTypes.s$field][0]) == 2; assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 104} true; call $tmp4 := Alloc(); assume $ArrayLength($tmp4) == 1 * 4; @@ -867,18 +867,18 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main2() assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 106} true; assert Box2Int($ArrayContents[t][0]) == 1; assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 108} true; - assert Box2Int($ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0]) == 2; + assert Box2Int($ArrayContents[RegressionTestInput.ClassWithArrayTypes.s$field][0]) == 2; assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 109} true; return; } -procedure RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32($this: Ref, x$in: int); +procedure RegressionTestInput.ClassWithArrayTypes.Main3$System.Int3214($this: Ref, x$in: int); -implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32($this: Ref, x$in: int) +implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int3214($this: Ref, x$in: int) { var x: int; var _loc0: Ref; @@ -888,12 +888,12 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32($this: x := x$in; assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 114} true; - $ArrayContents := $ArrayContents[Box2Ref(Read($Heap, $this, RegressionTestInput.ClassWithArrayTypes.a)) := $ArrayContents[Box2Ref(Read($Heap, $this, RegressionTestInput.ClassWithArrayTypes.a))][x := Int2Box(42)]]; + $ArrayContents := $ArrayContents[Box2Ref(Read($Heap, $this, RegressionTestInput.ClassWithArrayTypes.a$field)) := $ArrayContents[Box2Ref(Read($Heap, $this, RegressionTestInput.ClassWithArrayTypes.a$field))][x := Int2Box(42)]]; assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 115} true; - $ArrayContents := $ArrayContents[Box2Ref(Read($Heap, $this, RegressionTestInput.ClassWithArrayTypes.a)) := $ArrayContents[Box2Ref(Read($Heap, $this, RegressionTestInput.ClassWithArrayTypes.a))][x + 1 := Int2Box(43)]]; + $ArrayContents := $ArrayContents[Box2Ref(Read($Heap, $this, RegressionTestInput.ClassWithArrayTypes.a$field)) := $ArrayContents[Box2Ref(Read($Heap, $this, RegressionTestInput.ClassWithArrayTypes.a$field))][x + 1 := Int2Box(43)]]; assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 116} true; - _loc0 := Box2Ref(Read($Heap, $this, RegressionTestInput.ClassWithArrayTypes.a)); - _loc1 := Box2Ref(Read($Heap, $this, RegressionTestInput.ClassWithArrayTypes.a)); + _loc0 := Box2Ref(Read($Heap, $this, RegressionTestInput.ClassWithArrayTypes.a$field)); + _loc1 := Box2Ref(Read($Heap, $this, RegressionTestInput.ClassWithArrayTypes.a$field)); assert Box2Int($ArrayContents[_loc0][x + 1]) == Box2Int($ArrayContents[_loc1][x]) + 1; assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 117} true; return; @@ -901,11 +901,11 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32($this: -procedure RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array($this: Ref, xs$in: Ref); +procedure RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array15($this: Ref, xs$in: Ref); -implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array($this: Ref, xs$in: Ref) +implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array15($this: Ref, xs$in: Ref) { var xs: Ref; var $localExc: Ref; @@ -922,7 +922,7 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array($ if (!(if xs != null then $ArrayLength(xs) <= 0 else true)) { assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 121} true; - $ArrayContents := $ArrayContents[Box2Ref(Read($Heap, $this, RegressionTestInput.ClassWithArrayTypes.a)) := $ArrayContents[Box2Ref(Read($Heap, $this, RegressionTestInput.ClassWithArrayTypes.a))][0 := Int2Box(Box2Int($ArrayContents[xs][0]))]]; + $ArrayContents := $ArrayContents[Box2Ref(Read($Heap, $this, RegressionTestInput.ClassWithArrayTypes.a$field)) := $ArrayContents[Box2Ref(Read($Heap, $this, RegressionTestInput.ClassWithArrayTypes.a$field))][0 := Int2Box(Box2Int($ArrayContents[xs][0]))]]; } else { @@ -934,17 +934,17 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array($ -procedure RegressionTestInput.ClassWithArrayTypes.#ctor($this: Ref); +procedure RegressionTestInput.ClassWithArrayTypes.#ctor16($this: Ref); -implementation RegressionTestInput.ClassWithArrayTypes.#ctor($this: Ref) +implementation RegressionTestInput.ClassWithArrayTypes.#ctor16($this: Ref) { var $localExc: Ref; var $label: int; - $Heap := Write($Heap, $this, RegressionTestInput.ClassWithArrayTypes.a, Ref2Box(null)); - call System.Object.#ctor($this); + $Heap := Write($Heap, $this, RegressionTestInput.ClassWithArrayTypes.a$field, Ref2Box(null)); + call System.Object.#ctor44($this); if ($Exception != null) { return; @@ -961,22 +961,22 @@ procedure RegressionTestInput.ClassWithArrayTypes.#cctor(); implementation RegressionTestInput.ClassWithArrayTypes.#cctor() { - RegressionTestInput.ClassWithArrayTypes.s := null; + RegressionTestInput.ClassWithArrayTypes.s$field := null; } -const unique RegressionTestInput.BitwiseOperations: Type; +const unique RegressionTestInput.BitwiseOperations$type: Type; -axiom $Subtype(RegressionTestInput.BitwiseOperations, System.Object); +axiom $Subtype(RegressionTestInput.BitwiseOperations$type, System.Object$type); -axiom $DisjointSubtree(RegressionTestInput.BitwiseOperations, System.Object); +axiom $DisjointSubtree(RegressionTestInput.BitwiseOperations$type, System.Object$type); -procedure RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int) returns ($result: int); +procedure RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$System.Int3217($this: Ref, x$in: int, y$in: int) returns ($result: int); -implementation RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int) returns ($result: int) +implementation RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$System.Int3217($this: Ref, x$in: int, y$in: int) returns ($result: int) { var x: int; var y: int; @@ -992,11 +992,11 @@ implementation RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$Sys -procedure RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int) returns ($result: int); +procedure RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$System.Int3218($this: Ref, x$in: int, y$in: int) returns ($result: int); -implementation RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int) returns ($result: int) +implementation RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$System.Int3218($this: Ref, x$in: int, y$in: int) returns ($result: int) { var x: int; var y: int; @@ -1012,11 +1012,11 @@ implementation RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$Syst -procedure RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int) returns ($result: int); +procedure RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$System.Int3219($this: Ref, x$in: int, y$in: int) returns ($result: int); -implementation RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int) returns ($result: int) +implementation RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$System.Int3219($this: Ref, x$in: int, y$in: int) returns ($result: int) { var x: int; var y: int; @@ -1032,11 +1032,11 @@ implementation RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$Sy -procedure RegressionTestInput.BitwiseOperations.BitwiseNegation$System.Int32($this: Ref, x$in: int) returns ($result: int); +procedure RegressionTestInput.BitwiseOperations.BitwiseNegation$System.Int3220($this: Ref, x$in: int) returns ($result: int); -implementation RegressionTestInput.BitwiseOperations.BitwiseNegation$System.Int32($this: Ref, x$in: int) returns ($result: int) +implementation RegressionTestInput.BitwiseOperations.BitwiseNegation$System.Int3220($this: Ref, x$in: int) returns ($result: int) { var x: int; var $localExc: Ref; @@ -1050,16 +1050,16 @@ implementation RegressionTestInput.BitwiseOperations.BitwiseNegation$System.Int3 -procedure RegressionTestInput.BitwiseOperations.#ctor($this: Ref); +procedure RegressionTestInput.BitwiseOperations.#ctor21($this: Ref); -implementation RegressionTestInput.BitwiseOperations.#ctor($this: Ref) +implementation RegressionTestInput.BitwiseOperations.#ctor21($this: Ref) { var $localExc: Ref; var $label: int; - call System.Object.#ctor($this); + call System.Object.#ctor44($this); if ($Exception != null) { return; @@ -1080,36 +1080,36 @@ implementation RegressionTestInput.BitwiseOperations.#cctor() -const unique RegressionTestInput.AsyncAttribute: Type; +const unique RegressionTestInput.AsyncAttribute$type: Type; -const {:extern} unique System.Attribute: Type; +const {:extern} unique System.Attribute$type: Type; -axiom $Subtype(System.Attribute, System.Object); +axiom $Subtype(System.Attribute$type, System.Object$type); -axiom $DisjointSubtree(System.Attribute, System.Object); +axiom $DisjointSubtree(System.Attribute$type, System.Object$type); -const {:extern} unique System.Runtime.InteropServices._Attribute: Type; +const {:extern} unique System.Runtime.InteropServices._Attribute$type: Type; -axiom $Subtype(System.Attribute, System.Runtime.InteropServices._Attribute); +axiom $Subtype(System.Attribute$type, System.Runtime.InteropServices._Attribute$type); -axiom $Subtype(RegressionTestInput.AsyncAttribute, System.Attribute); +axiom $Subtype(RegressionTestInput.AsyncAttribute$type, System.Attribute$type); -axiom $DisjointSubtree(RegressionTestInput.AsyncAttribute, System.Attribute); +axiom $DisjointSubtree(RegressionTestInput.AsyncAttribute$type, System.Attribute$type); -procedure RegressionTestInput.AsyncAttribute.#ctor($this: Ref); +procedure RegressionTestInput.AsyncAttribute.#ctor22($this: Ref); -procedure {:extern} System.Attribute.#ctor($this: Ref); +procedure {:extern} System.Attribute.#ctor45($this: Ref); -implementation RegressionTestInput.AsyncAttribute.#ctor($this: Ref) +implementation RegressionTestInput.AsyncAttribute.#ctor22($this: Ref) { var $localExc: Ref; var $label: int; - call System.Attribute.#ctor($this); + call System.Attribute.#ctor45($this); if ($Exception != null) { return; @@ -1130,17 +1130,17 @@ implementation RegressionTestInput.AsyncAttribute.#cctor() -const unique RegressionTestInput.RefParameters: Type; +const unique RegressionTestInput.RefParameters$type: Type; -axiom $Subtype(RegressionTestInput.RefParameters, System.Object); +axiom $Subtype(RegressionTestInput.RefParameters$type, System.Object$type); -axiom $DisjointSubtree(RegressionTestInput.RefParameters, System.Object); +axiom $DisjointSubtree(RegressionTestInput.RefParameters$type, System.Object$type); -procedure RegressionTestInput.RefParameters.M$System.Int32$(x$in: int) returns (x$out: int); +procedure RegressionTestInput.RefParameters.M$System.Int32$23(x$in: int) returns (x$out: int); -implementation RegressionTestInput.RefParameters.M$System.Int32$(x$in: int) returns (x$out: int) +implementation RegressionTestInput.RefParameters.M$System.Int32$23(x$in: int) returns (x$out: int) { var $localExc: Ref; var $label: int; @@ -1154,16 +1154,16 @@ implementation RegressionTestInput.RefParameters.M$System.Int32$(x$in: int) retu -procedure RegressionTestInput.RefParameters.#ctor($this: Ref); +procedure RegressionTestInput.RefParameters.#ctor24($this: Ref); -implementation RegressionTestInput.RefParameters.#ctor($this: Ref) +implementation RegressionTestInput.RefParameters.#ctor24($this: Ref) { var $localExc: Ref; var $label: int; - call System.Object.#ctor($this); + call System.Object.#ctor44($this); if ($Exception != null) { return; @@ -1184,22 +1184,22 @@ implementation RegressionTestInput.RefParameters.#cctor() -const unique RegressionTestInput.NestedGeneric: Type; +const unique RegressionTestInput.NestedGeneric$type: Type; -axiom $Subtype(RegressionTestInput.NestedGeneric, System.Object); +axiom $Subtype(RegressionTestInput.NestedGeneric$type, System.Object$type); -axiom $DisjointSubtree(RegressionTestInput.NestedGeneric, System.Object); +axiom $DisjointSubtree(RegressionTestInput.NestedGeneric$type, System.Object$type); -procedure RegressionTestInput.NestedGeneric.#ctor($this: Ref); +procedure RegressionTestInput.NestedGeneric.#ctor27($this: Ref); -implementation RegressionTestInput.NestedGeneric.#ctor($this: Ref) +implementation RegressionTestInput.NestedGeneric.#ctor27($this: Ref) { var $localExc: Ref; var $label: int; - call System.Object.#ctor($this); + call System.Object.#ctor44($this); if ($Exception != null) { return; @@ -1210,22 +1210,22 @@ implementation RegressionTestInput.NestedGeneric.#ctor($this: Ref) -const unique RegressionTestInput.NestedGeneric.C: Type; +const unique RegressionTestInput.NestedGeneric.C$type: Type; -axiom $Subtype(RegressionTestInput.NestedGeneric.C, System.Object); +axiom $Subtype(RegressionTestInput.NestedGeneric.C$type, System.Object$type); -axiom $DisjointSubtree(RegressionTestInput.NestedGeneric.C, System.Object); +axiom $DisjointSubtree(RegressionTestInput.NestedGeneric.C$type, System.Object$type); -procedure RegressionTestInput.NestedGeneric.C.#ctor($this: Ref); +procedure RegressionTestInput.NestedGeneric.C.#ctor26($this: Ref); -implementation RegressionTestInput.NestedGeneric.C.#ctor($this: Ref) +implementation RegressionTestInput.NestedGeneric.C.#ctor26($this: Ref) { var $localExc: Ref; var $label: int; - call System.Object.#ctor($this); + call System.Object.#ctor44($this); if ($Exception != null) { return; @@ -1236,21 +1236,21 @@ implementation RegressionTestInput.NestedGeneric.C.#ctor($this: Ref) -function RegressionTestInput.NestedGeneric.C.G(arg0: Type) : Type; +function RegressionTestInput.NestedGeneric.C.G$type(arg0: Type) : Type; function Child0(in: Type) : Type; -axiom (forall arg0: Type :: { RegressionTestInput.NestedGeneric.C.G(arg0) } Child0(RegressionTestInput.NestedGeneric.C.G(arg0)) == arg0); +axiom (forall arg0: Type :: { RegressionTestInput.NestedGeneric.C.G$type(arg0) } Child0(RegressionTestInput.NestedGeneric.C.G$type(arg0)) == arg0); -procedure RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int32($this: Ref, x$in: int); +procedure RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int3225($this: Ref, x$in: int); -procedure {:extern} System.Activator.CreateInstance``1(T: Type) returns ($result: Box); +procedure {:extern} System.Activator.CreateInstance``12(T: Type) returns ($result: Box); -implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int32($this: Ref, x$in: int) +implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int3225($this: Ref, x$in: int) { var x: int; var CS$0$0000: Box; @@ -1265,7 +1265,7 @@ implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int32($this: x := x$in; assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 187} true; - call System.Object.#ctor($this); + call System.Object.#ctor44($this); if ($Exception != null) { return; @@ -1282,7 +1282,7 @@ implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int32($this: } else { - call $tmp7 := System.Activator.CreateInstance``1(Child0($DynamicType($this))); + call $tmp7 := System.Activator.CreateInstance``12(Child0($DynamicType($this))); $tmp6 := Box2Box($tmp7); if ($Exception != null) { @@ -1329,7 +1329,7 @@ implementation RegressionTestInput.NestedGeneric.#cctor() -implementation {:inline 1} RegressionTestInput.S.#default_ctor(this: Ref) +implementation {:inline 1} RegressionTestInput.S298.#default_ctor(this: Ref) { } @@ -1343,25 +1343,25 @@ procedure RegressionTestInput.S.#copy_ctor(this: Ref, other: Ref); implementation {:inline 1} RegressionTestInput.S.#copy_ctor(this: Ref, other: Ref) { - $Heap := Write($Heap, other, RegressionTestInput.S.x, Int2Box(Box2Int(Read($Heap, this, RegressionTestInput.S.x)))); - $Heap := Write($Heap, other, RegressionTestInput.S.b, Bool2Box(Box2Bool(Read($Heap, this, RegressionTestInput.S.b)))); + $Heap := Write($Heap, other, RegressionTestInput.S.x$field, Int2Box(Box2Int(Read($Heap, this, RegressionTestInput.S.x$field)))); + $Heap := Write($Heap, other, RegressionTestInput.S.b$field, Bool2Box(Box2Bool(Read($Heap, this, RegressionTestInput.S.b$field)))); } -const unique RegressionTestInput.Class0: Type; +const unique RegressionTestInput.Class0$type: Type; -axiom $Subtype(RegressionTestInput.Class0, System.Object); +axiom $Subtype(RegressionTestInput.Class0$type, System.Object$type); -axiom $DisjointSubtree(RegressionTestInput.Class0, System.Object); +axiom $DisjointSubtree(RegressionTestInput.Class0$type, System.Object$type); -var RegressionTestInput.Class0.StaticInt: int; +var RegressionTestInput.Class0.StaticInt$field: int; -procedure RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) returns ($result: int); +procedure RegressionTestInput.Class0.StaticMethod$System.Int3228(x$in: int) returns ($result: int); -implementation RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) returns ($result: int) +implementation RegressionTestInput.Class0.StaticMethod$System.Int3228(x$in: int) returns ($result: int) { var x: int; var $localExc: Ref; @@ -1375,11 +1375,11 @@ implementation RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) r -procedure RegressionTestInput.Class0.M$System.Int32($this: Ref, x$in: int); +procedure RegressionTestInput.Class0.M$System.Int3229($this: Ref, x$in: int); -implementation RegressionTestInput.Class0.M$System.Int32($this: Ref, x$in: int) +implementation RegressionTestInput.Class0.M$System.Int3229($this: Ref, x$in: int) { var x: int; var __temp_1: int; @@ -1401,20 +1401,20 @@ implementation RegressionTestInput.Class0.M$System.Int32($this: Ref, x$in: int) assert (if x == 3 then y <= 8 else false); assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 23} true; - RegressionTestInput.Class0.StaticInt := y; + RegressionTestInput.Class0.StaticInt$field := y; assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 24} true; - assert y == RegressionTestInput.Class0.StaticInt; + assert y == RegressionTestInput.Class0.StaticInt$field; assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 25} true; return; } -procedure RegressionTestInput.Class0.M$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int); +procedure RegressionTestInput.Class0.M$System.Int32$System.Int3230($this: Ref, x$in: int, y$in: int); -implementation RegressionTestInput.Class0.M$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int) +implementation RegressionTestInput.Class0.M$System.Int32$System.Int3230($this: Ref, x$in: int, y$in: int) { var x: int; var y: int; @@ -1429,11 +1429,11 @@ implementation RegressionTestInput.Class0.M$System.Int32$System.Int32($this: Ref -procedure RegressionTestInput.Class0.M$System.Boolean($this: Ref, b$in: bool); +procedure RegressionTestInput.Class0.M$System.Boolean31($this: Ref, b$in: bool); -implementation RegressionTestInput.Class0.M$System.Boolean($this: Ref, b$in: bool) +implementation RegressionTestInput.Class0.M$System.Boolean31($this: Ref, b$in: bool) { var b: bool; var $localExc: Ref; @@ -1446,11 +1446,11 @@ implementation RegressionTestInput.Class0.M$System.Boolean($this: Ref, b$in: boo -procedure RegressionTestInput.Class0.M$RegressionTestInput.Class0($this: Ref, c$in: Ref); +procedure RegressionTestInput.Class0.M$RegressionTestInput.Class032($this: Ref, c$in: Ref); -implementation RegressionTestInput.Class0.M$RegressionTestInput.Class0($this: Ref, c$in: Ref) +implementation RegressionTestInput.Class0.M$RegressionTestInput.Class032($this: Ref, c$in: Ref) { var c: Ref; var $localExc: Ref; @@ -1463,41 +1463,41 @@ implementation RegressionTestInput.Class0.M$RegressionTestInput.Class0($this: Re -procedure RegressionTestInput.Class0.NonVoid($this: Ref) returns ($result: int); +procedure RegressionTestInput.Class0.NonVoid33($this: Ref) returns ($result: int); -implementation RegressionTestInput.Class0.NonVoid($this: Ref) returns ($result: int) +implementation RegressionTestInput.Class0.NonVoid33($this: Ref) returns ($result: int) { var $tmp8: 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 $tmp8 := RegressionTestInput.Class0.StaticMethod$System.Int3228(3); if ($Exception != null) { return; } - $result := 3 + RegressionTestInput.Class0.StaticInt + $tmp8; + $result := 3 + RegressionTestInput.Class0.StaticInt$field + $tmp8; return; } -procedure RegressionTestInput.Class0.OutParam$System.Int32$($this: Ref, x$in: int) returns (x$out: int, $result: int); +procedure RegressionTestInput.Class0.OutParam$System.Int32$34($this: Ref, x$in: int) returns (x$out: int, $result: int); -implementation RegressionTestInput.Class0.OutParam$System.Int32$($this: Ref, x$in: int) returns (x$out: int, $result: int) +implementation RegressionTestInput.Class0.OutParam$System.Int32$34($this: Ref, x$in: int) returns (x$out: int, $result: int) { var $localExc: Ref; var $label: int; x$out := x$in; assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 37} true; - x$out := 3 + RegressionTestInput.Class0.StaticInt; + x$out := 3 + RegressionTestInput.Class0.StaticInt$field; assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 39} true; $result := x$out; return; @@ -1505,11 +1505,11 @@ implementation RegressionTestInput.Class0.OutParam$System.Int32$($this: Ref, x$i -procedure RegressionTestInput.Class0.RefParam$System.Int32$($this: Ref, x$in: int) returns (x$out: int, $result: int); +procedure RegressionTestInput.Class0.RefParam$System.Int32$35($this: Ref, x$in: int) returns (x$out: int, $result: int); -implementation RegressionTestInput.Class0.RefParam$System.Int32$($this: Ref, x$in: int) returns (x$out: int, $result: int) +implementation RegressionTestInput.Class0.RefParam$System.Int32$35($this: Ref, x$in: int) returns (x$out: int, $result: int) { var $localExc: Ref; var $label: int; @@ -1518,7 +1518,7 @@ implementation RegressionTestInput.Class0.RefParam$System.Int32$($this: Ref, x$i assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 42} true; x$out := x$out + 1; assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 43} true; - RegressionTestInput.Class0.StaticInt := x$out; + RegressionTestInput.Class0.StaticInt$field := x$out; assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 45} true; $result := x$out; return; @@ -1526,11 +1526,11 @@ implementation RegressionTestInput.Class0.RefParam$System.Int32$($this: Ref, x$i -procedure RegressionTestInput.Class0.AssignToInParam$System.Int32($this: Ref, x$in: int) returns ($result: int); +procedure RegressionTestInput.Class0.AssignToInParam$System.Int3236($this: Ref, x$in: int) returns ($result: int); -implementation RegressionTestInput.Class0.AssignToInParam$System.Int32($this: Ref, x$in: int) returns ($result: int) +implementation RegressionTestInput.Class0.AssignToInParam$System.Int3236($this: Ref, x$in: int) returns ($result: int) { var x: int; var $localExc: Ref; @@ -1540,7 +1540,7 @@ implementation RegressionTestInput.Class0.AssignToInParam$System.Int32($this: Re assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 48} true; x := x + 1; assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 49} true; - RegressionTestInput.Class0.StaticInt := x; + RegressionTestInput.Class0.StaticInt$field := x; assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 51} true; $result := x; return; @@ -1548,11 +1548,11 @@ implementation RegressionTestInput.Class0.AssignToInParam$System.Int32($this: Re -procedure {:RegressionTestInput.Async} RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32($this: Ref, x$in: int) returns ($result: int); +procedure {:RegressionTestInput.Async} RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int3237($this: Ref, x$in: int) returns ($result: int); -implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32($this: Ref, x$in: int) returns ($result: int) +implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int3237($this: Ref, x$in: int) returns ($result: int) { var x: int; var $localExc: Ref; @@ -1566,11 +1566,11 @@ implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMetho -procedure RegressionTestInput.Class0.CallAsyncMethod$System.Int32($this: Ref, y$in: int) returns ($result: int); +procedure RegressionTestInput.Class0.CallAsyncMethod$System.Int3238($this: Ref, y$in: int) returns ($result: int); -implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int32($this: Ref, y$in: int) returns ($result: int) +implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int3238($this: Ref, y$in: int) returns ($result: int) { var y: int; var $tmp9: int; @@ -1579,7 +1579,7 @@ implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int32($this: Re 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} $tmp9 := RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int3237($this, y); if ($Exception != null) { return; @@ -1591,16 +1591,16 @@ implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int32($this: Re -procedure RegressionTestInput.Class0.#ctor($this: Ref); +procedure RegressionTestInput.Class0.#ctor39($this: Ref); -implementation RegressionTestInput.Class0.#ctor($this: Ref) +implementation RegressionTestInput.Class0.#ctor39($this: Ref) { var $localExc: Ref; var $label: int; - call System.Object.#ctor($this); + call System.Object.#ctor44($this); if ($Exception != null) { return; @@ -1617,26 +1617,26 @@ procedure RegressionTestInput.Class0.#cctor(); implementation RegressionTestInput.Class0.#cctor() { - RegressionTestInput.Class0.StaticInt := 0; + RegressionTestInput.Class0.StaticInt$field := 0; } -const unique RegressionTestInput.ClassWithBoolTypes: Type; +const unique RegressionTestInput.ClassWithBoolTypes$type: Type; -axiom $Subtype(RegressionTestInput.ClassWithBoolTypes, System.Object); +axiom $Subtype(RegressionTestInput.ClassWithBoolTypes$type, System.Object$type); -axiom $DisjointSubtree(RegressionTestInput.ClassWithBoolTypes, System.Object); +axiom $DisjointSubtree(RegressionTestInput.ClassWithBoolTypes$type, System.Object$type); -var RegressionTestInput.ClassWithBoolTypes.staticB: bool; +var RegressionTestInput.ClassWithBoolTypes.staticB$field: bool; -const unique RegressionTestInput.ClassWithBoolTypes.b: Field; +const unique RegressionTestInput.ClassWithBoolTypes.b$field: Field; -procedure RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(x$in: int, y$in: int) returns ($result: bool); +procedure RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3240(x$in: int, y$in: int) returns ($result: bool); -implementation RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(x$in: int, y$in: int) returns ($result: bool) +implementation RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3240(x$in: int, y$in: int) returns ($result: bool) { var x: int; var y: int; @@ -1652,32 +1652,32 @@ implementation RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3 -procedure RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean($this: Ref, z$in: bool); +procedure RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean41($this: Ref, z$in: bool); -implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean($this: Ref, z$in: bool) +implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean41($this: Ref, z$in: bool) { var z: bool; var $localExc: Ref; var $label: int; z := z$in; - $Heap := Write($Heap, $this, RegressionTestInput.ClassWithBoolTypes.b, Bool2Box(false)); + $Heap := Write($Heap, $this, RegressionTestInput.ClassWithBoolTypes.b$field, Bool2Box(false)); assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 72} true; - call System.Object.#ctor($this); + call System.Object.#ctor44($this); if ($Exception != null) { return; } assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 73} true; - $Heap := Write($Heap, $this, RegressionTestInput.ClassWithBoolTypes.b, Bool2Box(z)); + $Heap := Write($Heap, $this, RegressionTestInput.ClassWithBoolTypes.b$field, Bool2Box(z)); assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 74} true; if (z) { assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 74} true; - RegressionTestInput.ClassWithBoolTypes.staticB := z; + RegressionTestInput.ClassWithBoolTypes.staticB$field := z; } else { @@ -1688,18 +1688,18 @@ implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean($this -procedure RegressionTestInput.ClassWithBoolTypes.Main(); +procedure RegressionTestInput.ClassWithBoolTypes.Main42(); -implementation RegressionTestInput.ClassWithBoolTypes.Main() +implementation RegressionTestInput.ClassWithBoolTypes.Main42() { var $tmp10: 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 $tmp10 := RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3240(3, 4); if ($Exception != null) { return; @@ -1717,7 +1717,7 @@ procedure RegressionTestInput.ClassWithBoolTypes.#cctor(); implementation RegressionTestInput.ClassWithBoolTypes.#cctor() { - RegressionTestInput.ClassWithBoolTypes.staticB := false; + RegressionTestInput.ClassWithBoolTypes.staticB$field := false; } diff --git a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt index 2f6b0041..d2b5950a 100644 --- a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt @@ -466,23 +466,23 @@ var $Receiver: [Ref][Ref]Ref; var {:thread_local} $Exception: Ref; -const unique RegressionTestInput.RealNumbers: Type; +const unique RegressionTestInput.RealNumbers$type: Type; -const {:extern} unique System.Object: Type; +const {:extern} unique System.Object$type: Type; -axiom $Subtype(RegressionTestInput.RealNumbers, System.Object); +axiom $Subtype(RegressionTestInput.RealNumbers$type, System.Object$type); -axiom $DisjointSubtree(RegressionTestInput.RealNumbers, System.Object); +axiom $DisjointSubtree(RegressionTestInput.RealNumbers$type, System.Object$type); -procedure RegressionTestInput.RealNumbers.WriteDouble$System.Double($this: Ref, d$in: Real); +procedure RegressionTestInput.RealNumbers.WriteDouble$System.Double3($this: Ref, d$in: Real); -procedure {:extern} System.Console.WriteLine$System.Double(value$in: Real); +procedure {:extern} System.Console.WriteLine$System.Double43(value$in: Real); -implementation RegressionTestInput.RealNumbers.WriteDouble$System.Double($this: Ref, d$in: Real) +implementation RegressionTestInput.RealNumbers.WriteDouble$System.Double3($this: Ref, d$in: Real) { var d: Real; var $localExc: Ref; @@ -490,7 +490,7 @@ implementation RegressionTestInput.RealNumbers.WriteDouble$System.Double($this: d := d$in; assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 162} true; - call System.Console.WriteLine$System.Double(d); + call System.Console.WriteLine$System.Double43(d); if ($Exception != null) { return; @@ -502,11 +502,11 @@ implementation RegressionTestInput.RealNumbers.WriteDouble$System.Double($this: -procedure RegressionTestInput.RealNumbers.ObjectToDouble$System.Object($this: Ref, o$in: Ref); +procedure RegressionTestInput.RealNumbers.ObjectToDouble$System.Object4($this: Ref, o$in: Ref); -implementation RegressionTestInput.RealNumbers.ObjectToDouble$System.Object($this: Ref, o$in: Ref) +implementation RegressionTestInput.RealNumbers.ObjectToDouble$System.Object4($this: Ref, o$in: Ref) { var o: Ref; var $localExc: Ref; @@ -514,7 +514,7 @@ implementation RegressionTestInput.RealNumbers.ObjectToDouble$System.Object($thi o := o$in; assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 165} true; - call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, Box2Real($BoxField[o])); + call RegressionTestInput.RealNumbers.WriteDouble$System.Double3($this, Box2Real($BoxField[o])); if ($Exception != null) { return; @@ -526,7 +526,7 @@ implementation RegressionTestInput.RealNumbers.ObjectToDouble$System.Object($thi -procedure RegressionTestInput.RealNumbers.RealOperations($this: Ref); +procedure RegressionTestInput.RealNumbers.RealOperations5($this: Ref); @@ -534,7 +534,7 @@ const unique $real_literal_3_0: Real; const unique $real_literal_4_0: Real; -implementation RegressionTestInput.RealNumbers.RealOperations($this: Ref) +implementation RegressionTestInput.RealNumbers.RealOperations5($this: Ref) { var d: Real; var d2: Real; @@ -546,28 +546,28 @@ implementation RegressionTestInput.RealNumbers.RealOperations($this: Ref) assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 169} true; d2 := $real_literal_4_0; assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 170} true; - call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealPlus(d, d2)); + call RegressionTestInput.RealNumbers.WriteDouble$System.Double3($this, RealPlus(d, d2)); if ($Exception != null) { return; } assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 171} true; - call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealMinus(d, d2)); + call RegressionTestInput.RealNumbers.WriteDouble$System.Double3($this, RealMinus(d, d2)); if ($Exception != null) { return; } assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 172} true; - call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealTimes(d, d2)); + call RegressionTestInput.RealNumbers.WriteDouble$System.Double3($this, RealTimes(d, d2)); if ($Exception != null) { return; } assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 173} true; - call RegressionTestInput.RealNumbers.WriteDouble$System.Double($this, RealDivide(d, d2)); + call RegressionTestInput.RealNumbers.WriteDouble$System.Double3($this, RealDivide(d, d2)); if ($Exception != null) { return; @@ -579,20 +579,20 @@ implementation RegressionTestInput.RealNumbers.RealOperations($this: Ref) -procedure RegressionTestInput.RealNumbers.#ctor($this: Ref); +procedure RegressionTestInput.RealNumbers.#ctor6($this: Ref); -procedure {:extern} System.Object.#ctor($this: Ref); +procedure {:extern} System.Object.#ctor44($this: Ref); -implementation RegressionTestInput.RealNumbers.#ctor($this: Ref) +implementation RegressionTestInput.RealNumbers.#ctor6($this: Ref) { var $localExc: Ref; var $label: int; - call System.Object.#ctor($this); + call System.Object.#ctor44($this); if ($Exception != null) { return; @@ -613,21 +613,21 @@ implementation RegressionTestInput.RealNumbers.#cctor() -const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap: Type; +const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap$type: Type; -axiom $Subtype(RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap, System.Object); +axiom $Subtype(RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap$type, System.Object$type); -axiom $DisjointSubtree(RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap, System.Object); +axiom $DisjointSubtree(RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap$type, System.Object$type); var RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x: [Ref]int; var RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y: [Ref]int; -procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M($this: Ref); +procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M7($this: Ref); -implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M($this: Ref) +implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M7($this: Ref) { var $localExc: Ref; var $label: int; @@ -640,18 +640,18 @@ implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M($this: -procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor($this: Ref); +procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor8($this: Ref); -implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor($this: Ref) +implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor8($this: Ref) { var $localExc: Ref; var $label: int; RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x[$this] := 0; RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y[$this] := 0; - call System.Object.#ctor($this); + call System.Object.#ctor44($this); if ($Exception != null) { return; @@ -672,37 +672,37 @@ implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor() -const unique RegressionTestInput.CreateStruct: Type; +const unique RegressionTestInput.CreateStruct$type: Type; -axiom $Subtype(RegressionTestInput.CreateStruct, System.Object); +axiom $Subtype(RegressionTestInput.CreateStruct$type, System.Object$type); -axiom $DisjointSubtree(RegressionTestInput.CreateStruct, System.Object); +axiom $DisjointSubtree(RegressionTestInput.CreateStruct$type, System.Object$type); -procedure RegressionTestInput.CreateStruct.Create($this: Ref) returns ($result: Ref); +procedure RegressionTestInput.CreateStruct.Create9($this: Ref) returns ($result: Ref); -procedure RegressionTestInput.S.#default_ctor(this: Ref); +procedure RegressionTestInput.S298.#default_ctor(this: Ref); -const unique RegressionTestInput.S: Type; +const unique RegressionTestInput.S$type: Type; -const {:extern} unique System.ValueType: Type; +const {:extern} unique System.ValueType$type: Type; -axiom $Subtype(System.ValueType, System.Object); +axiom $Subtype(System.ValueType$type, System.Object$type); -axiom $DisjointSubtree(System.ValueType, System.Object); +axiom $DisjointSubtree(System.ValueType$type, System.Object$type); -axiom $Subtype(RegressionTestInput.S, System.ValueType); +axiom $Subtype(RegressionTestInput.S$type, System.ValueType$type); -axiom $DisjointSubtree(RegressionTestInput.S, System.ValueType); +axiom $DisjointSubtree(RegressionTestInput.S$type, System.ValueType$type); var RegressionTestInput.S.x: [Ref]int; var RegressionTestInput.S.b: [Ref]bool; -implementation RegressionTestInput.CreateStruct.Create($this: Ref) returns ($result: Ref) +implementation RegressionTestInput.CreateStruct.Create9($this: Ref) returns ($result: Ref) { var $tmp0: Ref; var s: Ref; @@ -711,8 +711,8 @@ implementation RegressionTestInput.CreateStruct.Create($this: Ref) returns ($res assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 141} true; call $tmp0 := Alloc(); - call RegressionTestInput.S.#default_ctor($tmp0); - assume $DynamicType($tmp0) == RegressionTestInput.S; + call RegressionTestInput.S298.#default_ctor($tmp0); + assume $DynamicType($tmp0) == RegressionTestInput.S$type; s := $tmp0; assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 142} true; assert RegressionTestInput.S.x[s] == 0; @@ -725,11 +725,11 @@ implementation RegressionTestInput.CreateStruct.Create($this: Ref) returns ($res -procedure RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInput.S($this: Ref, s$in: Ref) returns ($result: Ref); +procedure RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInput.S10($this: Ref, s$in: Ref) returns ($result: Ref); -implementation RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInput.S($this: Ref, s$in: Ref) returns ($result: Ref) +implementation RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInput.S10($this: Ref, s$in: Ref) returns ($result: Ref) { var s: Ref; var $localExc: Ref; @@ -747,16 +747,16 @@ implementation RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTes -procedure RegressionTestInput.CreateStruct.#ctor($this: Ref); +procedure RegressionTestInput.CreateStruct.#ctor11($this: Ref); -implementation RegressionTestInput.CreateStruct.#ctor($this: Ref) +implementation RegressionTestInput.CreateStruct.#ctor11($this: Ref) { var $localExc: Ref; var $label: int; - call System.Object.#ctor($this); + call System.Object.#ctor44($this); if ($Exception != null) { return; @@ -777,21 +777,21 @@ implementation RegressionTestInput.CreateStruct.#cctor() -const unique RegressionTestInput.ClassWithArrayTypes: Type; +const unique RegressionTestInput.ClassWithArrayTypes$type: Type; -axiom $Subtype(RegressionTestInput.ClassWithArrayTypes, System.Object); +axiom $Subtype(RegressionTestInput.ClassWithArrayTypes$type, System.Object$type); -axiom $DisjointSubtree(RegressionTestInput.ClassWithArrayTypes, System.Object); +axiom $DisjointSubtree(RegressionTestInput.ClassWithArrayTypes$type, System.Object$type); var RegressionTestInput.ClassWithArrayTypes.s: Ref; var RegressionTestInput.ClassWithArrayTypes.a: [Ref]Ref; -procedure RegressionTestInput.ClassWithArrayTypes.Main1(); +procedure RegressionTestInput.ClassWithArrayTypes.Main112(); -implementation RegressionTestInput.ClassWithArrayTypes.Main1() +implementation RegressionTestInput.ClassWithArrayTypes.Main112() { var s: Ref; var $tmp1: Ref; @@ -824,11 +824,11 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main1() -procedure RegressionTestInput.ClassWithArrayTypes.Main2(); +procedure RegressionTestInput.ClassWithArrayTypes.Main213(); -implementation RegressionTestInput.ClassWithArrayTypes.Main2() +implementation RegressionTestInput.ClassWithArrayTypes.Main213() { var $tmp3: Ref; var t: Ref; @@ -860,11 +860,11 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main2() -procedure RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32($this: Ref, x$in: int); +procedure RegressionTestInput.ClassWithArrayTypes.Main3$System.Int3214($this: Ref, x$in: int); -implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32($this: Ref, x$in: int) +implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int3214($this: Ref, x$in: int) { var x: int; var _loc0: Ref; @@ -887,11 +887,11 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32($this: -procedure RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array($this: Ref, xs$in: Ref); +procedure RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array15($this: Ref, xs$in: Ref); -implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array($this: Ref, xs$in: Ref) +implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array15($this: Ref, xs$in: Ref) { var xs: Ref; var $localExc: Ref; @@ -920,17 +920,17 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array($ -procedure RegressionTestInput.ClassWithArrayTypes.#ctor($this: Ref); +procedure RegressionTestInput.ClassWithArrayTypes.#ctor16($this: Ref); -implementation RegressionTestInput.ClassWithArrayTypes.#ctor($this: Ref) +implementation RegressionTestInput.ClassWithArrayTypes.#ctor16($this: Ref) { var $localExc: Ref; var $label: int; RegressionTestInput.ClassWithArrayTypes.a[$this] := null; - call System.Object.#ctor($this); + call System.Object.#ctor44($this); if ($Exception != null) { return; @@ -952,17 +952,17 @@ implementation RegressionTestInput.ClassWithArrayTypes.#cctor() -const unique RegressionTestInput.BitwiseOperations: Type; +const unique RegressionTestInput.BitwiseOperations$type: Type; -axiom $Subtype(RegressionTestInput.BitwiseOperations, System.Object); +axiom $Subtype(RegressionTestInput.BitwiseOperations$type, System.Object$type); -axiom $DisjointSubtree(RegressionTestInput.BitwiseOperations, System.Object); +axiom $DisjointSubtree(RegressionTestInput.BitwiseOperations$type, System.Object$type); -procedure RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int) returns ($result: int); +procedure RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$System.Int3217($this: Ref, x$in: int, y$in: int) returns ($result: int); -implementation RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int) returns ($result: int) +implementation RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$System.Int3217($this: Ref, x$in: int, y$in: int) returns ($result: int) { var x: int; var y: int; @@ -978,11 +978,11 @@ implementation RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$Sys -procedure RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int) returns ($result: int); +procedure RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$System.Int3218($this: Ref, x$in: int, y$in: int) returns ($result: int); -implementation RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int) returns ($result: int) +implementation RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$System.Int3218($this: Ref, x$in: int, y$in: int) returns ($result: int) { var x: int; var y: int; @@ -998,11 +998,11 @@ implementation RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$Syst -procedure RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int) returns ($result: int); +procedure RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$System.Int3219($this: Ref, x$in: int, y$in: int) returns ($result: int); -implementation RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int) returns ($result: int) +implementation RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$System.Int3219($this: Ref, x$in: int, y$in: int) returns ($result: int) { var x: int; var y: int; @@ -1018,11 +1018,11 @@ implementation RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$Sy -procedure RegressionTestInput.BitwiseOperations.BitwiseNegation$System.Int32($this: Ref, x$in: int) returns ($result: int); +procedure RegressionTestInput.BitwiseOperations.BitwiseNegation$System.Int3220($this: Ref, x$in: int) returns ($result: int); -implementation RegressionTestInput.BitwiseOperations.BitwiseNegation$System.Int32($this: Ref, x$in: int) returns ($result: int) +implementation RegressionTestInput.BitwiseOperations.BitwiseNegation$System.Int3220($this: Ref, x$in: int) returns ($result: int) { var x: int; var $localExc: Ref; @@ -1036,16 +1036,16 @@ implementation RegressionTestInput.BitwiseOperations.BitwiseNegation$System.Int3 -procedure RegressionTestInput.BitwiseOperations.#ctor($this: Ref); +procedure RegressionTestInput.BitwiseOperations.#ctor21($this: Ref); -implementation RegressionTestInput.BitwiseOperations.#ctor($this: Ref) +implementation RegressionTestInput.BitwiseOperations.#ctor21($this: Ref) { var $localExc: Ref; var $label: int; - call System.Object.#ctor($this); + call System.Object.#ctor44($this); if ($Exception != null) { return; @@ -1066,36 +1066,36 @@ implementation RegressionTestInput.BitwiseOperations.#cctor() -const unique RegressionTestInput.AsyncAttribute: Type; +const unique RegressionTestInput.AsyncAttribute$type: Type; -const {:extern} unique System.Attribute: Type; +const {:extern} unique System.Attribute$type: Type; -axiom $Subtype(System.Attribute, System.Object); +axiom $Subtype(System.Attribute$type, System.Object$type); -axiom $DisjointSubtree(System.Attribute, System.Object); +axiom $DisjointSubtree(System.Attribute$type, System.Object$type); -const {:extern} unique System.Runtime.InteropServices._Attribute: Type; +const {:extern} unique System.Runtime.InteropServices._Attribute$type: Type; -axiom $Subtype(System.Attribute, System.Runtime.InteropServices._Attribute); +axiom $Subtype(System.Attribute$type, System.Runtime.InteropServices._Attribute$type); -axiom $Subtype(RegressionTestInput.AsyncAttribute, System.Attribute); +axiom $Subtype(RegressionTestInput.AsyncAttribute$type, System.Attribute$type); -axiom $DisjointSubtree(RegressionTestInput.AsyncAttribute, System.Attribute); +axiom $DisjointSubtree(RegressionTestInput.AsyncAttribute$type, System.Attribute$type); -procedure RegressionTestInput.AsyncAttribute.#ctor($this: Ref); +procedure RegressionTestInput.AsyncAttribute.#ctor22($this: Ref); -procedure {:extern} System.Attribute.#ctor($this: Ref); +procedure {:extern} System.Attribute.#ctor45($this: Ref); -implementation RegressionTestInput.AsyncAttribute.#ctor($this: Ref) +implementation RegressionTestInput.AsyncAttribute.#ctor22($this: Ref) { var $localExc: Ref; var $label: int; - call System.Attribute.#ctor($this); + call System.Attribute.#ctor45($this); if ($Exception != null) { return; @@ -1116,17 +1116,17 @@ implementation RegressionTestInput.AsyncAttribute.#cctor() -const unique RegressionTestInput.RefParameters: Type; +const unique RegressionTestInput.RefParameters$type: Type; -axiom $Subtype(RegressionTestInput.RefParameters, System.Object); +axiom $Subtype(RegressionTestInput.RefParameters$type, System.Object$type); -axiom $DisjointSubtree(RegressionTestInput.RefParameters, System.Object); +axiom $DisjointSubtree(RegressionTestInput.RefParameters$type, System.Object$type); -procedure RegressionTestInput.RefParameters.M$System.Int32$(x$in: int) returns (x$out: int); +procedure RegressionTestInput.RefParameters.M$System.Int32$23(x$in: int) returns (x$out: int); -implementation RegressionTestInput.RefParameters.M$System.Int32$(x$in: int) returns (x$out: int) +implementation RegressionTestInput.RefParameters.M$System.Int32$23(x$in: int) returns (x$out: int) { var $localExc: Ref; var $label: int; @@ -1140,16 +1140,16 @@ implementation RegressionTestInput.RefParameters.M$System.Int32$(x$in: int) retu -procedure RegressionTestInput.RefParameters.#ctor($this: Ref); +procedure RegressionTestInput.RefParameters.#ctor24($this: Ref); -implementation RegressionTestInput.RefParameters.#ctor($this: Ref) +implementation RegressionTestInput.RefParameters.#ctor24($this: Ref) { var $localExc: Ref; var $label: int; - call System.Object.#ctor($this); + call System.Object.#ctor44($this); if ($Exception != null) { return; @@ -1170,22 +1170,22 @@ implementation RegressionTestInput.RefParameters.#cctor() -const unique RegressionTestInput.NestedGeneric: Type; +const unique RegressionTestInput.NestedGeneric$type: Type; -axiom $Subtype(RegressionTestInput.NestedGeneric, System.Object); +axiom $Subtype(RegressionTestInput.NestedGeneric$type, System.Object$type); -axiom $DisjointSubtree(RegressionTestInput.NestedGeneric, System.Object); +axiom $DisjointSubtree(RegressionTestInput.NestedGeneric$type, System.Object$type); -procedure RegressionTestInput.NestedGeneric.#ctor($this: Ref); +procedure RegressionTestInput.NestedGeneric.#ctor27($this: Ref); -implementation RegressionTestInput.NestedGeneric.#ctor($this: Ref) +implementation RegressionTestInput.NestedGeneric.#ctor27($this: Ref) { var $localExc: Ref; var $label: int; - call System.Object.#ctor($this); + call System.Object.#ctor44($this); if ($Exception != null) { return; @@ -1196,22 +1196,22 @@ implementation RegressionTestInput.NestedGeneric.#ctor($this: Ref) -const unique RegressionTestInput.NestedGeneric.C: Type; +const unique RegressionTestInput.NestedGeneric.C$type: Type; -axiom $Subtype(RegressionTestInput.NestedGeneric.C, System.Object); +axiom $Subtype(RegressionTestInput.NestedGeneric.C$type, System.Object$type); -axiom $DisjointSubtree(RegressionTestInput.NestedGeneric.C, System.Object); +axiom $DisjointSubtree(RegressionTestInput.NestedGeneric.C$type, System.Object$type); -procedure RegressionTestInput.NestedGeneric.C.#ctor($this: Ref); +procedure RegressionTestInput.NestedGeneric.C.#ctor26($this: Ref); -implementation RegressionTestInput.NestedGeneric.C.#ctor($this: Ref) +implementation RegressionTestInput.NestedGeneric.C.#ctor26($this: Ref) { var $localExc: Ref; var $label: int; - call System.Object.#ctor($this); + call System.Object.#ctor44($this); if ($Exception != null) { return; @@ -1222,21 +1222,21 @@ implementation RegressionTestInput.NestedGeneric.C.#ctor($this: Ref) -function RegressionTestInput.NestedGeneric.C.G(arg0: Type) : Type; +function RegressionTestInput.NestedGeneric.C.G$type(arg0: Type) : Type; function Child0(in: Type) : Type; -axiom (forall arg0: Type :: { RegressionTestInput.NestedGeneric.C.G(arg0) } Child0(RegressionTestInput.NestedGeneric.C.G(arg0)) == arg0); +axiom (forall arg0: Type :: { RegressionTestInput.NestedGeneric.C.G$type(arg0) } Child0(RegressionTestInput.NestedGeneric.C.G$type(arg0)) == arg0); -procedure RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int32($this: Ref, x$in: int); +procedure RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int3225($this: Ref, x$in: int); -procedure {:extern} System.Activator.CreateInstance``1(T: Type) returns ($result: Box); +procedure {:extern} System.Activator.CreateInstance``12(T: Type) returns ($result: Box); -implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int32($this: Ref, x$in: int) +implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int3225($this: Ref, x$in: int) { var x: int; var CS$0$0000: Box; @@ -1251,7 +1251,7 @@ implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int32($this: x := x$in; assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 187} true; - call System.Object.#ctor($this); + call System.Object.#ctor44($this); if ($Exception != null) { return; @@ -1268,7 +1268,7 @@ implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int32($this: } else { - call $tmp7 := System.Activator.CreateInstance``1(Child0($DynamicType($this))); + call $tmp7 := System.Activator.CreateInstance``12(Child0($DynamicType($this))); $tmp6 := Box2Box($tmp7); if ($Exception != null) { @@ -1315,7 +1315,7 @@ implementation RegressionTestInput.NestedGeneric.#cctor() -implementation {:inline 1} RegressionTestInput.S.#default_ctor(this: Ref) +implementation {:inline 1} RegressionTestInput.S298.#default_ctor(this: Ref) { } @@ -1335,19 +1335,19 @@ implementation {:inline 1} RegressionTestInput.S.#copy_ctor(this: Ref, other: Re -const unique RegressionTestInput.Class0: Type; +const unique RegressionTestInput.Class0$type: Type; -axiom $Subtype(RegressionTestInput.Class0, System.Object); +axiom $Subtype(RegressionTestInput.Class0$type, System.Object$type); -axiom $DisjointSubtree(RegressionTestInput.Class0, System.Object); +axiom $DisjointSubtree(RegressionTestInput.Class0$type, System.Object$type); var RegressionTestInput.Class0.StaticInt: int; -procedure RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) returns ($result: int); +procedure RegressionTestInput.Class0.StaticMethod$System.Int3228(x$in: int) returns ($result: int); -implementation RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) returns ($result: int) +implementation RegressionTestInput.Class0.StaticMethod$System.Int3228(x$in: int) returns ($result: int) { var x: int; var $localExc: Ref; @@ -1361,11 +1361,11 @@ implementation RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) r -procedure RegressionTestInput.Class0.M$System.Int32($this: Ref, x$in: int); +procedure RegressionTestInput.Class0.M$System.Int3229($this: Ref, x$in: int); -implementation RegressionTestInput.Class0.M$System.Int32($this: Ref, x$in: int) +implementation RegressionTestInput.Class0.M$System.Int3229($this: Ref, x$in: int) { var x: int; var __temp_1: int; @@ -1396,11 +1396,11 @@ implementation RegressionTestInput.Class0.M$System.Int32($this: Ref, x$in: int) -procedure RegressionTestInput.Class0.M$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int); +procedure RegressionTestInput.Class0.M$System.Int32$System.Int3230($this: Ref, x$in: int, y$in: int); -implementation RegressionTestInput.Class0.M$System.Int32$System.Int32($this: Ref, x$in: int, y$in: int) +implementation RegressionTestInput.Class0.M$System.Int32$System.Int3230($this: Ref, x$in: int, y$in: int) { var x: int; var y: int; @@ -1415,11 +1415,11 @@ implementation RegressionTestInput.Class0.M$System.Int32$System.Int32($this: Ref -procedure RegressionTestInput.Class0.M$System.Boolean($this: Ref, b$in: bool); +procedure RegressionTestInput.Class0.M$System.Boolean31($this: Ref, b$in: bool); -implementation RegressionTestInput.Class0.M$System.Boolean($this: Ref, b$in: bool) +implementation RegressionTestInput.Class0.M$System.Boolean31($this: Ref, b$in: bool) { var b: bool; var $localExc: Ref; @@ -1432,11 +1432,11 @@ implementation RegressionTestInput.Class0.M$System.Boolean($this: Ref, b$in: boo -procedure RegressionTestInput.Class0.M$RegressionTestInput.Class0($this: Ref, c$in: Ref); +procedure RegressionTestInput.Class0.M$RegressionTestInput.Class032($this: Ref, c$in: Ref); -implementation RegressionTestInput.Class0.M$RegressionTestInput.Class0($this: Ref, c$in: Ref) +implementation RegressionTestInput.Class0.M$RegressionTestInput.Class032($this: Ref, c$in: Ref) { var c: Ref; var $localExc: Ref; @@ -1449,18 +1449,18 @@ implementation RegressionTestInput.Class0.M$RegressionTestInput.Class0($this: Re -procedure RegressionTestInput.Class0.NonVoid($this: Ref) returns ($result: int); +procedure RegressionTestInput.Class0.NonVoid33($this: Ref) returns ($result: int); -implementation RegressionTestInput.Class0.NonVoid($this: Ref) returns ($result: int) +implementation RegressionTestInput.Class0.NonVoid33($this: Ref) returns ($result: int) { var $tmp8: 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 $tmp8 := RegressionTestInput.Class0.StaticMethod$System.Int3228(3); if ($Exception != null) { return; @@ -1472,11 +1472,11 @@ implementation RegressionTestInput.Class0.NonVoid($this: Ref) returns ($result: -procedure RegressionTestInput.Class0.OutParam$System.Int32$($this: Ref, x$in: int) returns (x$out: int, $result: int); +procedure RegressionTestInput.Class0.OutParam$System.Int32$34($this: Ref, x$in: int) returns (x$out: int, $result: int); -implementation RegressionTestInput.Class0.OutParam$System.Int32$($this: Ref, x$in: int) returns (x$out: int, $result: int) +implementation RegressionTestInput.Class0.OutParam$System.Int32$34($this: Ref, x$in: int) returns (x$out: int, $result: int) { var $localExc: Ref; var $label: int; @@ -1491,11 +1491,11 @@ implementation RegressionTestInput.Class0.OutParam$System.Int32$($this: Ref, x$i -procedure RegressionTestInput.Class0.RefParam$System.Int32$($this: Ref, x$in: int) returns (x$out: int, $result: int); +procedure RegressionTestInput.Class0.RefParam$System.Int32$35($this: Ref, x$in: int) returns (x$out: int, $result: int); -implementation RegressionTestInput.Class0.RefParam$System.Int32$($this: Ref, x$in: int) returns (x$out: int, $result: int) +implementation RegressionTestInput.Class0.RefParam$System.Int32$35($this: Ref, x$in: int) returns (x$out: int, $result: int) { var $localExc: Ref; var $label: int; @@ -1512,11 +1512,11 @@ implementation RegressionTestInput.Class0.RefParam$System.Int32$($this: Ref, x$i -procedure RegressionTestInput.Class0.AssignToInParam$System.Int32($this: Ref, x$in: int) returns ($result: int); +procedure RegressionTestInput.Class0.AssignToInParam$System.Int3236($this: Ref, x$in: int) returns ($result: int); -implementation RegressionTestInput.Class0.AssignToInParam$System.Int32($this: Ref, x$in: int) returns ($result: int) +implementation RegressionTestInput.Class0.AssignToInParam$System.Int3236($this: Ref, x$in: int) returns ($result: int) { var x: int; var $localExc: Ref; @@ -1534,11 +1534,11 @@ implementation RegressionTestInput.Class0.AssignToInParam$System.Int32($this: Re -procedure {:RegressionTestInput.Async} RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32($this: Ref, x$in: int) returns ($result: int); +procedure {:RegressionTestInput.Async} RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int3237($this: Ref, x$in: int) returns ($result: int); -implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32($this: Ref, x$in: int) returns ($result: int) +implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int3237($this: Ref, x$in: int) returns ($result: int) { var x: int; var $localExc: Ref; @@ -1552,11 +1552,11 @@ implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMetho -procedure RegressionTestInput.Class0.CallAsyncMethod$System.Int32($this: Ref, y$in: int) returns ($result: int); +procedure RegressionTestInput.Class0.CallAsyncMethod$System.Int3238($this: Ref, y$in: int) returns ($result: int); -implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int32($this: Ref, y$in: int) returns ($result: int) +implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int3238($this: Ref, y$in: int) returns ($result: int) { var y: int; var $tmp9: int; @@ -1565,7 +1565,7 @@ implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int32($this: Re 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} $tmp9 := RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int3237($this, y); if ($Exception != null) { return; @@ -1577,16 +1577,16 @@ implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int32($this: Re -procedure RegressionTestInput.Class0.#ctor($this: Ref); +procedure RegressionTestInput.Class0.#ctor39($this: Ref); -implementation RegressionTestInput.Class0.#ctor($this: Ref) +implementation RegressionTestInput.Class0.#ctor39($this: Ref) { var $localExc: Ref; var $label: int; - call System.Object.#ctor($this); + call System.Object.#ctor44($this); if ($Exception != null) { return; @@ -1608,21 +1608,21 @@ implementation RegressionTestInput.Class0.#cctor() -const unique RegressionTestInput.ClassWithBoolTypes: Type; +const unique RegressionTestInput.ClassWithBoolTypes$type: Type; -axiom $Subtype(RegressionTestInput.ClassWithBoolTypes, System.Object); +axiom $Subtype(RegressionTestInput.ClassWithBoolTypes$type, System.Object$type); -axiom $DisjointSubtree(RegressionTestInput.ClassWithBoolTypes, System.Object); +axiom $DisjointSubtree(RegressionTestInput.ClassWithBoolTypes$type, System.Object$type); var RegressionTestInput.ClassWithBoolTypes.staticB: bool; var RegressionTestInput.ClassWithBoolTypes.b: [Ref]bool; -procedure RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(x$in: int, y$in: int) returns ($result: bool); +procedure RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3240(x$in: int, y$in: int) returns ($result: bool); -implementation RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(x$in: int, y$in: int) returns ($result: bool) +implementation RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3240(x$in: int, y$in: int) returns ($result: bool) { var x: int; var y: int; @@ -1638,11 +1638,11 @@ implementation RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3 -procedure RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean($this: Ref, z$in: bool); +procedure RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean41($this: Ref, z$in: bool); -implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean($this: Ref, z$in: bool) +implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean41($this: Ref, z$in: bool) { var z: bool; var $localExc: Ref; @@ -1651,7 +1651,7 @@ implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean($this z := z$in; RegressionTestInput.ClassWithBoolTypes.b[$this] := false; assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 72} true; - call System.Object.#ctor($this); + call System.Object.#ctor44($this); if ($Exception != null) { return; @@ -1674,18 +1674,18 @@ implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean($this -procedure RegressionTestInput.ClassWithBoolTypes.Main(); +procedure RegressionTestInput.ClassWithBoolTypes.Main42(); -implementation RegressionTestInput.ClassWithBoolTypes.Main() +implementation RegressionTestInput.ClassWithBoolTypes.Main42() { var $tmp10: 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 $tmp10 := RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3240(3, 4); if ($Exception != null) { return; -- cgit v1.2.3