From 64d8963508ce048d00db3766f4ca597b792c1b95 Mon Sep 17 00:00:00 2001
From: Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com>
Date: Sat, 18 May 2013 21:15:20 -0700
Subject: reworked the linear and og implementation based on available
 variables theory

---
 Source/BoogieDriver/BoogieDriver.cs | 25 ++++++++++++-------------
 1 file changed, 12 insertions(+), 13 deletions(-)

(limited to 'Source/BoogieDriver')

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;
-- 
cgit v1.2.3