reworked the linear and og implementation based on available variables theory

1 files changed, 12 insertions, 13 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index 3e2b83de..f448bcd2 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -194,23 +194,16 @@ namespace Microsoft.Boogie {
 

           if (CommandLineOptions.Clo.OwickiGriesDesugaredOutputFile != null)

           {

-              OwickiGriesTransform ogTransform = new OwickiGriesTransform(program);

+              OwickiGriesTransform ogTransform = new OwickiGriesTransform(linearTypechecker);

               ogTransform.Transform();

+              var eraser = new LinearEraser();

+              eraser.VisitProgram(program);

               int oldPrintUnstructured = CommandLineOptions.Clo.PrintUnstructured;

               CommandLineOptions.Clo.PrintUnstructured = 1;

               PrintBplFile(CommandLineOptions.Clo.OwickiGriesDesugaredOutputFile, program, false, false);

               CommandLineOptions.Clo.PrintUnstructured = oldPrintUnstructured;

           }

 

-          {

-              LinearSetTransform linearTransform = new LinearSetTransform(program);

-              linearTransform.Transform();

-              //int oldPrintUnstructured = CommandLineOptions.Clo.PrintUnstructured;

-              //CommandLineOptions.Clo.PrintUnstructured = 1;

-              //PrintBplFile("lsd.bpl", program, false, false);

-              //CommandLineOptions.Clo.PrintUnstructured = oldPrintUnstructured;

-          }

-

           EliminateDeadVariablesAndInline(program);

 

           if (CommandLineOptions.Clo.StagedHoudini > 0)

@@ -379,6 +372,8 @@ namespace Microsoft.Boogie {
       VerificationCompleted

     }

 

+    static LinearTypechecker linearTypechecker;

+

     /// <summary>

     /// Resolves and type checks the given Boogie program.  Any errors are reported to the

     /// console.  Returns:

@@ -414,9 +409,13 @@ namespace Microsoft.Boogie {
         return PipelineOutcome.TypeCheckingError;

       }

 

-      LinearTypechecker linearTypechecker = new LinearTypechecker();

-      linearTypechecker.VisitProgram(program);

-      if (linearTypechecker.errorCount > 0)

+      linearTypechecker = new LinearTypechecker(program);

+      linearTypechecker.Typecheck();

+      if (linearTypechecker.errorCount == 0)

+      {

+          linearTypechecker.Transform();

+      }

+      else

       {

           Console.WriteLine("{0} type checking errors detected in {1}", errorCount, bplFileName);

           return PipelineOutcome.TypeCheckingError;