Automated merge with https://hg01.codeplex.com/boogie

3 files changed, 25 insertions, 23 deletions

diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
index 67fbfdb8..151843d8 100644
--- a/BCT/BytecodeTranslator/Program.cs
+++ b/BCT/BytecodeTranslator/Program.cs
@@ -193,6 +193,8 @@ namespace BytecodeTranslator {
       var host = new CodeContractAwareHostEnvironment(libPaths != null ? libPaths : Enumerable<string>.Empty, true, true);

       Host = host;

 

+      Bpl.CommandLineOptions.Install(new Bpl.CommandLineOptions());

+

       #region Assemlies to translate (via cmd line)

       modules = new List<IModule>();

       var contractExtractors = new Dictionary<IUnit, IContractProvider>();

@@ -218,7 +220,7 @@ namespace BytecodeTranslator {
         }

         var m2 = Decompiler.GetCodeModelFromMetadataModel(host, m, pdbReader) as IModule;

         // The decompiler does not turn calls to Assert/Assume into Code Model nodes

-        m2 = new Microsoft.Cci.MutableContracts.ContractExtractor.AssertAssumeExtractor(host, pdbReader).Visit(m2);

+        m2 = new Microsoft.Cci.MutableContracts.ContractExtractor.AssertAssumeExtractor(host, pdbReader).Rewrite(m2);

         decompiledModules.Add(m2);

         host.RegisterAsLatest(m2);

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

diff --git a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
index f68465d1..39c9986a 100644
--- a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
@@ -10,7 +10,7 @@ procedure {:inline 1} Alloc() returns (x: Ref);
 

 

 

-implementation Alloc() returns (x: Ref)

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

 {

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

     $Alloc[x] := true;

@@ -38,7 +38,7 @@ procedure {:inline 1} System.Object.GetType(this: Ref) returns ($result: Ref);
 

 

 

-implementation System.Object.GetType(this: Ref) returns ($result: Ref)

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

 {

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

 }

@@ -63,7 +63,7 @@ procedure {:inline 1} System.Threading.Thread.#ctor$System.Threading.Parameteriz
 

 

 

-implementation System.Threading.Thread.#ctor$System.Threading.ParameterizedThreadStart(this: Ref, start$in: Ref)

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

 {

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

 }

@@ -74,7 +74,7 @@ procedure {:inline 1} System.Threading.Thread.Start$System.Object(this: Ref, par
 

 

 

-implementation System.Threading.Thread.Start$System.Object(this: Ref, parameter$in: Ref)

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

 {

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

 }

@@ -85,7 +85,7 @@ procedure {:inline 1} Wrapper_System.Threading.ParameterizedThreadStart.Invoke$S
 

 

 

-implementation Wrapper_System.Threading.ParameterizedThreadStart.Invoke$System.Object(this: Ref, obj$in: Ref)

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

 {

     $Exception := null;

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

@@ -101,7 +101,7 @@ procedure {:inline 1} System.Threading.Thread.#ctor$System.Threading.ThreadStart
 

 

 

-implementation System.Threading.Thread.#ctor$System.Threading.ThreadStart(this: Ref, start$in: Ref)

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

 {

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

 }

@@ -112,7 +112,7 @@ procedure {:inline 1} System.Threading.Thread.Start(this: Ref);
 

 

 

-implementation System.Threading.Thread.Start(this: Ref)

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

 {

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

 }

@@ -123,7 +123,7 @@ procedure {:inline 1} Wrapper_System.Threading.ThreadStart.Invoke(this: Ref);
 

 

 

-implementation Wrapper_System.Threading.ThreadStart.Invoke(this: Ref)

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

 {

     $Exception := null;

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

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

 

 

-implementation DelegateAdd(a: Ref, b: Ref) returns (c: Ref)

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

 {

   var d: Delegate;

 

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

 

 

-implementation DelegateRemove(a: Ref, b: Ref) returns (c: Ref)

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

 {

   var d: Delegate;

 

@@ -213,7 +213,7 @@ procedure {:inline 1} DelegateCreate(d: Delegate) returns (c: Ref);
 

 

 

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

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

 {

     call c := Alloc();

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

diff --git a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
index 9484ee38..22431543 100644
--- a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
@@ -8,7 +8,7 @@ procedure {:inline 1} Alloc() returns (x: Ref);
 

 

 

-implementation Alloc() returns (x: Ref)

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

 {

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

     $Alloc[x] := true;

@@ -36,7 +36,7 @@ procedure {:inline 1} System.Object.GetType(this: Ref) returns ($result: Ref);
 

 

 

-implementation System.Object.GetType(this: Ref) returns ($result: Ref)

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

 {

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

 }

@@ -61,7 +61,7 @@ procedure {:inline 1} System.Threading.Thread.#ctor$System.Threading.Parameteriz
 

 

 

-implementation System.Threading.Thread.#ctor$System.Threading.ParameterizedThreadStart(this: Ref, start$in: Ref)

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

 {

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

 }

@@ -72,7 +72,7 @@ procedure {:inline 1} System.Threading.Thread.Start$System.Object(this: Ref, par
 

 

 

-implementation System.Threading.Thread.Start$System.Object(this: Ref, parameter$in: Ref)

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

 {

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

 }

@@ -83,7 +83,7 @@ procedure {:inline 1} Wrapper_System.Threading.ParameterizedThreadStart.Invoke$S
 

 

 

-implementation Wrapper_System.Threading.ParameterizedThreadStart.Invoke$System.Object(this: Ref, obj$in: Ref)

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

 {

     $Exception := null;

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

@@ -99,7 +99,7 @@ procedure {:inline 1} System.Threading.Thread.#ctor$System.Threading.ThreadStart
 

 

 

-implementation System.Threading.Thread.#ctor$System.Threading.ThreadStart(this: Ref, start$in: Ref)

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

 {

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

 }

@@ -110,7 +110,7 @@ procedure {:inline 1} System.Threading.Thread.Start(this: Ref);
 

 

 

-implementation System.Threading.Thread.Start(this: Ref)

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

 {

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

 }

@@ -121,7 +121,7 @@ procedure {:inline 1} Wrapper_System.Threading.ThreadStart.Invoke(this: Ref);
 

 

 

-implementation Wrapper_System.Threading.ThreadStart.Invoke(this: Ref)

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

 {

     $Exception := null;

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

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

 

 

-implementation DelegateAdd(a: Ref, b: Ref) returns (c: Ref)

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

 {

   var d: Delegate;

 

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

 

 

-implementation DelegateRemove(a: Ref, b: Ref) returns (c: Ref)

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

 {

   var d: Delegate;

 

@@ -211,7 +211,7 @@ procedure {:inline 1} DelegateCreate(d: Delegate) returns (c: Ref);
 

 

 

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

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

 {

     call c := Alloc();

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