minor name changes, boogie code cleanup

3 files changed, 8 insertions, 298 deletions

diff --git a/BCT/BytecodeTranslator/Phone/PhoneTraverser.cs b/BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs
index 5f4680a8..121c4384 100644
--- a/BCT/BytecodeTranslator/Phone/PhoneTraverser.cs
+++ b/BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs
@@ -23,7 +23,7 @@ namespace BytecodeTranslator {
   /// <summary>

   /// Traverse code looking for phone specific points of interest, possibly injecting necessary code in-between

   /// </summary>

-  public class PhoneCodeTraverser : BaseCodeTraverser {

+  public class PhoneInitializationCodeTraverser : BaseCodeTraverser {

     private readonly IMethodDefinition methodBeingTraversed;

     private static bool initializationFound= false;

     private PhoneControlsPlugin phonePlugin;

@@ -69,7 +69,7 @@ namespace BytecodeTranslator {
       }

     }

 

-    public PhoneCodeTraverser(MetadataReaderHost host, IMethodDefinition traversedMethod, PhoneControlsPlugin phonePlugin) : base() {

+    public PhoneInitializationCodeTraverser(MetadataReaderHost host, IMethodDefinition traversedMethod, PhoneControlsPlugin phonePlugin) : base() {

       this.methodBeingTraversed = traversedMethod;

       this.phonePlugin = phonePlugin;

       this.host = host;

@@ -140,11 +140,6 @@ namespace BytecodeTranslator {
       this.Visit(block);

     }

 

-    private Assignment MakeFieldAssigment(string assignType, string objectName, string objectType, string fieldName, string sourceObjName, string sourceObjType, string sourceObjFieldName) {

-      /* TODO */

-      return null;

-    }

-

     private void injectPhoneInitializationCode(BlockStatement block, Statement statementAfter) {

       // TODO check page name against container name

       IEnumerable<ControlInfoStructure> controls= phonePlugin.getControlsForPage(methodBeingTraversed.Container.ToString());

@@ -241,7 +236,9 @@ namespace BytecodeTranslator {
       return new List<IStatement>();

     }

 

+    // TODO should stop propagating the string

     private IEnumerable<IStatement> getCodeForSettingEventHandlers(ControlInfoStructure controlInfo, string eventName) {

+

       // TODO not implemented yet

       return new List<IStatement>();

     }

@@ -271,11 +268,11 @@ namespace BytecodeTranslator {
   /// <summary>

   /// Traverse metadata looking only for PhoneApplicationPage's constructors

   /// </summary>

-  public class PhoneMetadataTraverser : BaseMetadataTraverser {

+  public class PhoneInitializationMetadataTraverser : BaseMetadataTraverser {

     private PhoneControlsPlugin phoneControlsInfo;

     private MetadataReaderHost host;

 

-    public PhoneMetadataTraverser(PhoneControlsPlugin phonePlugin, MetadataReaderHost host)

+    public PhoneInitializationMetadataTraverser(PhoneControlsPlugin phonePlugin, MetadataReaderHost host)

       : base() {

         this.phoneControlsInfo = phonePlugin;

         this.host = host;

@@ -323,7 +320,7 @@ namespace BytecodeTranslator {
       if (!method.IsConstructor)

         return;

 

-      PhoneCodeTraverser codeTraverser = new PhoneCodeTraverser(host, method, phoneControlsInfo);

+      PhoneInitializationCodeTraverser codeTraverser = new PhoneInitializationCodeTraverser(host, method, phoneControlsInfo);

       var methodBody = method.Body as SourceMethodBody;

       if (methodBody == null)

         return;

diff --git a/BCT/BytecodeTranslator/Phone/stubs.bpl b/BCT/BytecodeTranslator/Phone/stubs.bpl
index caa8210b..ae97e03f 100644
--- a/BCT/BytecodeTranslator/Phone/stubs.bpl
+++ b/BCT/BytecodeTranslator/Phone/stubs.bpl
@@ -1,286 +1,3 @@
-// BEGIN INJECTED CODE

-

-procedure UpdateNavigation(uri:Ref);

-implementation UpdateNavigation(uri:Ref) {

-    CurrentNavigationPage := uri;

-}

-

-procedure DriveControls();

-implementation DriveControls() {

-  var isCurrentPage1: bool;

-  var isCurrentPage2: bool;

-  var isCurrentPage3: bool;

-  var isCurrentPage4: bool;

-

-  // TODO there can be parameters in the URI and other stuff that makes this checks quite unreliable

-  call isCurrentPage1 := System.String.op_Equality$System.String$System.String(CurrentNavigationPage, $string_literal_$Page1.xaml_0);

-  call isCurrentPage2 := System.String.op_Equality$System.String$System.String(CurrentNavigationPage, $string_literal_$Page2.xaml_1);

-  call isCurrentPage3 := System.String.op_Equality$System.String$System.String(CurrentNavigationPage, $string_literal_$Page3.xaml_2);

-  call isCurrentPage4 := System.String.op_Equality$System.String$System.String(CurrentNavigationPage, $string_literal_$Page4.xaml_3);

-  

-  if (isCurrentPage1) {

-    call drivePage1Controls();

-  } else if (isCurrentPage2) {

-    call drivePage2Controls();

-  } else if (isCurrentPage3) {

-    call drivePage3Controls();

-  } else if (isCurrentPage4) {

-    call drivePage4Controls();

-  }

-}

-

-procedure drivePage1Controls();

-implementation drivePage1Controls() {

-  var $continueOnPage: bool;

-  var $activeControl: int;

-  var $control: Ref;

-  var $isEnabledRef: Ref;

-  var $isEnabled: bool;

-

-  $continueOnPage:=true;

-  havoc $activeControl;

-  while ($continueOnPage) {

-      if ($activeControl==0) {

-        // radio1 check

-        $control := SimpleNavigationApp.Page1.radioButton1[$page1];

-        call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);

-        $isEnabled := Box2Bool(Ref2Box($isEnabledRef));

-        if ($isEnabled) {

-          call System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($control, Box2Ref(Bool2Box(true)));

-        }

-      } else if ($activeControl==1) {

-        // radio2 check

-        $control := SimpleNavigationApp.Page1.radioButton2[$page1];

-        call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);

-        $isEnabled := Box2Bool(Ref2Box($isEnabledRef));

-        if ($isEnabled) {

-          call System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($control, Box2Ref(Bool2Box(true)));

-        }

-      } else if ($activeControl==2) {

-        // radio3 check

-        $control := SimpleNavigationApp.Page1.radioButton3[$page1];

-        call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);

-        $isEnabled := Box2Bool(Ref2Box($isEnabledRef));

-        if ($isEnabled) {

-          call System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($control, Box2Ref(Bool2Box(true)));

-        }

-      } else if ($activeControl==3) {

-        //radio4 check

-        $control := SimpleNavigationApp.Page1.radioButton4[$page1];

-        call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);

-        $isEnabled := Box2Bool(Ref2Box($isEnabledRef));

-        if ($isEnabled) {

-          call System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($control, Box2Ref(Bool2Box(true)));

-        }

-      } else if ($activeControl==4) {

-        //button click

-        $control := SimpleNavigationApp.Page1.btnNavigate[$page1];

-        call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);

-        $isEnabled := Box2Bool(Ref2Box($isEnabledRef));

-        if ($isEnabled) {

-          call SimpleNavigationApp.Page1.btnNavigate_Click$System.Object$System.Windows.RoutedEventArgs($page1, null, null);

-          $continueOnPage := false;

-        }

-    }

-  }

-}

-

-procedure drivePage2Controls();

-implementation drivePage2Controls() {

-  var $continueOnPage: bool;

-  var $activeControl: int;

-  var $control: Ref;

-  var $isEnabledRef: Ref;

-  var $isEnabled: bool;

-

-  $continueOnPage:=true;

-  havoc $activeControl;

-  while ($continueOnPage) {

-      if ($activeControl==0) {

-        // radio1 check

-        $control := SimpleNavigationApp.Page2.radioButton1[$page2];

-        call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);

-        $isEnabled := Box2Bool(Ref2Box($isEnabledRef));

-        if ($isEnabled) {

-          call System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($control, Box2Ref(Bool2Box(true)));

-        }

-      } else if ($activeControl==1) {

-        // radio2 check

-        $control := SimpleNavigationApp.Page2.radioButton2[$page2];

-        call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);

-        $isEnabled := Box2Bool(Ref2Box($isEnabledRef));

-        if ($isEnabled) {

-          call System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($control, Box2Ref(Bool2Box(true)));

-        }

-      } else if ($activeControl==2) {

-        // radio3 check

-        $control := SimpleNavigationApp.Page2.radioButton3[$page2];

-        call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);

-        $isEnabled := Box2Bool(Ref2Box($isEnabledRef));

-        if ($isEnabled) {

-          call System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($control, Box2Ref(Bool2Box(true)));

-        }

-      } else if ($activeControl==3) {

-        //radio4 check

-        $control := SimpleNavigationApp.Page2.radioButton4[$page2];

-        call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);

-        $isEnabled := Box2Bool(Ref2Box($isEnabledRef));

-        if ($isEnabled) {

-          call System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($control, Box2Ref(Bool2Box(true)));

-        }

-      } else if ($activeControl==4) {

-        //button click

-        $control := SimpleNavigationApp.Page2.btnNavigate[$page2];

-        call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);

-        $isEnabled := Box2Bool(Ref2Box($isEnabledRef));

-        if ($isEnabled) {

-          call SimpleNavigationApp.Page2.btnNavigate_Click$System.Object$System.Windows.RoutedEventArgs($page2, null, null);

-          $continueOnPage := false;

-        }

-    }

-  }

-}

-

-procedure drivePage3Controls();

-implementation drivePage3Controls() {

-  var $continueOnPage: bool;

-  var $activeControl: int;

-  var $control: Ref;

-  var $isEnabledRef: Ref;

-  var $isEnabled: bool;

-

-  $continueOnPage:=true;

-  havoc $activeControl;

-  while ($continueOnPage) {

-      if ($activeControl==0) {

-        // radio1 check

-        $control := SimpleNavigationApp.Page3.radioButton1[$page3];

-        call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);

-        $isEnabled := Box2Bool(Ref2Box($isEnabledRef));

-        if ($isEnabled) {

-          call System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($control, Box2Ref(Bool2Box(true)));

-        }

-      } else if ($activeControl==1) {

-        // radio2 check

-        $control := SimpleNavigationApp.Page3.radioButton2[$page3];

-        call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);

-        $isEnabled := Box2Bool(Ref2Box($isEnabledRef));

-        if ($isEnabled) {

-          call System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($control, Box2Ref(Bool2Box(true)));

-        }

-      } else if ($activeControl==2) {

-        // radio3 check

-        $control := SimpleNavigationApp.Page3.radioButton3[$page3];

-        call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);

-        $isEnabled := Box2Bool(Ref2Box($isEnabledRef));

-        if ($isEnabled) {

-          call System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($control, Box2Ref(Bool2Box(true)));

-        }

-      } else if ($activeControl==3) {

-        //radio4 check

-        $control := SimpleNavigationApp.Page3.radioButton4[$page3];

-        call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);

-        $isEnabled := Box2Bool(Ref2Box($isEnabledRef));

-        if ($isEnabled) {

-          call System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($control, Box2Ref(Bool2Box(true)));

-        }

-      } else if ($activeControl==4) {

-        //button click

-        $control := SimpleNavigationApp.Page3.btnNavigate[$page3];

-        call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);

-        $isEnabled := Box2Bool(Ref2Box($isEnabledRef));

-        if ($isEnabled) {

-          call SimpleNavigationApp.Page3.btnNavigate_Click$System.Object$System.Windows.RoutedEventArgs($page3, null, null);

-          $continueOnPage := false;

-        }

-    }

-  }

-}

-

-procedure drivePage4Controls();

-implementation drivePage4Controls() {

-  var $continueOnPage: bool;

-  var $activeControl: int;

-  var $control: Ref;

-  var $isEnabledRef: Ref;

-  var $isEnabled: bool;

-

-  $continueOnPage:=true;

-  havoc $activeControl;

-  while ($continueOnPage) {

-      if ($activeControl==0) {

-        // radio1 check

-        $control := SimpleNavigationApp.Page4.radioButton1[$page4];

-        call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);

-        $isEnabled := Box2Bool(Ref2Box($isEnabledRef));

-        if ($isEnabled) {

-          call System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($control, Box2Ref(Bool2Box(true)));

-        }

-      } else if ($activeControl==1) {

-        // radio2 check

-        $control := SimpleNavigationApp.Page4.radioButton2[$page4];

-        call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);

-        $isEnabled := Box2Bool(Ref2Box($isEnabledRef));

-        if ($isEnabled) {

-          call System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($control, Box2Ref(Bool2Box(true)));

-        }

-      } else if ($activeControl==2) {

-        // radio3 check

-        $control := SimpleNavigationApp.Page4.radioButton3[$page4];

-        call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);

-        $isEnabled := Box2Bool(Ref2Box($isEnabledRef));

-        if ($isEnabled) {

-          call System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($control, Box2Ref(Bool2Box(true)));

-        }

-      } else if ($activeControl==3) {

-        //radio4 check

-        $control := SimpleNavigationApp.Page4.radioButton4[$page4];

-        call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);

-        $isEnabled := Box2Bool(Ref2Box($isEnabledRef));

-        if ($isEnabled) {

-          call System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($control, Box2Ref(Bool2Box(true)));

-        }

-      } else if ($activeControl==4) {

-        //button click

-        $control := SimpleNavigationApp.Page4.btnNavigate[$page4];

-        call $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);

-        $isEnabled := Box2Bool(Ref2Box($isEnabledRef));

-        if ($isEnabled) {

-          call SimpleNavigationApp.Page4.btnNavigate_Click$System.Object$System.Windows.RoutedEventArgs($page4, null, null);

-          $continueOnPage := false;

-        }

-    }

-  }

-}

-

-var $page1: Ref;

-var $page2: Ref;

-var $page3: Ref;

-var $page4: Ref;

-

-procedure SimpleNavigationApp.Main();

-implementation SimpleNavigationApp.Main() {

-  var $doWork: bool;

-  var $activeControl: int;

-  var $isEnabledRef: Ref;

-  var $isEnabled: bool;

-  var $control: Ref;

-

-  call SimpleNavigationApp.Page1.#ctor($page1);

-  call SimpleNavigationApp.Page2.#ctor($page2);

-  call SimpleNavigationApp.Page3.#ctor($page3);

-  call SimpleNavigationApp.Page4.#ctor($page4);

-  call SimpleNavigationApp.Page1.Page1_Loaded$System.Object$System.Windows.RoutedEventArgs($page1, null, null);

-

-  CurrentNavigationPage := $string_literal_$Page1.xaml_0;

-

-  havoc $doWork;

-  while ($doWork) {

-    call DriveControls();

-    havoc $doWork; 

-  }

-}

-

 function isControlEnabled(Ref) : bool;

 function isControlChecked(Ref) : bool;

 

@@ -322,7 +39,3 @@ implementation System.Windows.Controls.Primitives.ToggleButton.get_IsChecked($th
   $result := Box2Ref(Bool2Box(isChecked));

 }

 

-var CurrentNavigationPage: Ref;

-var uriToNavigate: Ref;

-

-// END INJECTED CODE
\ No newline at end of file
diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
index 28149cbd..a9d44200 100644
--- a/BCT/BytecodeTranslator/Program.cs
+++ b/BCT/BytecodeTranslator/Program.cs
@@ -176,7 +176,7 @@ namespace BytecodeTranslator {
       var primaryModule = modules[0];

 

       if (phoneControlsConfigFile != null && phoneControlsConfigFile != "") {

-        PhoneMetadataTraverser tr = new PhoneMetadataTraverser(new PhoneControlsPlugin(phoneControlsConfigFile), host);

+        PhoneInitializationMetadataTraverser tr = new PhoneInitializationMetadataTraverser(new PhoneControlsPlugin(phoneControlsConfigFile), host);

         tr.InjectPhoneCodeAssemblies(modules);

       }