dynamic navigation variable tracking and base page name tracking

5 files changed, 122 insertions, 48 deletions

diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs
index 7abb070c..02ae0c9f 100644
--- a/BCT/BytecodeTranslator/MetadataTraverser.cs
+++ b/BCT/BytecodeTranslator/MetadataTraverser.cs
@@ -67,6 +67,8 @@ namespace BytecodeTranslator {
       var savedPrivateTypes = this.privateTypes;

       this.privateTypes = new List<ITypeDefinition>();

 

+      trackPageNameVariableName(typeDefinition);

+

       if (typeDefinition.IsClass) {

         bool savedSawCctor = this.sawCctor;

         this.sawCctor = false;

@@ -100,6 +102,16 @@ namespace BytecodeTranslator {
     }

     List<ITypeDefinition> privateTypes = new List<ITypeDefinition>();

 

+    private void trackPageNameVariableName(ITypeDefinition typeDef) {

+      if (typeDef.isPhoneApplicationPageClass(sink.host)) {

+        INamespaceTypeDefinition namedTypeDef = typeDef as INamespaceTypeDefinition;

+        string fullyQualifiedName = namedTypeDef.ContainingNamespace.Name.Value + "." + namedTypeDef.Name.Value;

+        string uriName = PhoneCodeHelper.getURIBase(PhoneCodeHelper.getXAMLForPage(fullyQualifiedName));

+        Bpl.Constant uriConstant= sink.FindOrCreateConstant(uriName);

+        PhoneCodeHelper.setBoogieStringPageNameForPageClass(fullyQualifiedName, uriConstant.Name);

+      }

+    }

+

     private void CreateDefaultStructConstructor(ITypeDefinition typeDefinition) {

       Contract.Requires(typeDefinition.IsStruct);

 

@@ -482,15 +494,26 @@ namespace BytecodeTranslator {
 

       // if tracked by the phone plugin, we need to find out the bpl assigned name for future use

       if (PhoneCodeHelper.PhonePlugin != null) {

-        INamespaceTypeReference namedContainerRef= fieldDefinition.ContainingType as INamespaceTypeReference;

-        if (namedContainerRef != null) {

-          string containerName = namedContainerRef.ContainingUnitNamespace.Unit.Name.Value + "." + namedContainerRef.Name.Value;

-          IEnumerable<ControlInfoStructure> controls= PhoneCodeHelper.PhonePlugin.getControlsForPage(containerName);

-          if (controls != null) {

-            ControlInfoStructure ctrlInfo = controls.FirstOrDefault(ctrl => ctrl.Name == fieldDefinition.Name.Value);

-            if (ctrlInfo != null)

-              ctrlInfo.BplName = fieldVar.Name;

-          }

+        trackControlVariableName(fieldDefinition, fieldVar);

+        trackNavigationVariableName(fieldDefinition, fieldVar);

+      }

+    }

+

+    private static void trackNavigationVariableName(IFieldDefinition fieldDefinition, Bpl.Variable fieldVar) {

+      if (fieldDefinition.Name.Value.Equals(PhoneCodeHelper.IL_CURRENT_NAVIGATION_URI_VARIABLE)) {

+        PhoneCodeHelper.setBoogieNavigationVariable(fieldVar.Name);

+      }

+    }

+

+    private static void trackControlVariableName(IFieldDefinition fieldDefinition, Bpl.Variable fieldVar) {

+      INamespaceTypeReference namedContainerRef = fieldDefinition.ContainingType as INamespaceTypeReference;

+      if (namedContainerRef != null) {

+        string containerName = namedContainerRef.ContainingUnitNamespace.Unit.Name.Value + "." + namedContainerRef.Name.Value;

+        IEnumerable<ControlInfoStructure> controls = PhoneCodeHelper.PhonePlugin.getControlsForPage(containerName);

+        if (controls != null) {

+          ControlInfoStructure ctrlInfo = controls.FirstOrDefault(ctrl => ctrl.Name == fieldDefinition.Name.Value);

+          if (ctrlInfo != null)

+            ctrlInfo.BplName = fieldVar.Name;

         }

       }

     }

diff --git a/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs b/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs
index ff6f3298..e9cc208b 100644
--- a/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs
+++ b/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs
@@ -15,7 +15,7 @@ namespace BytecodeTranslator.Phone {
     // TODO ensure this name is unique in the program code, although it is esoteric enough

     // TODO externalize strings

     private const string IL_BOOGIE_VAR_PREFIX = "@__BOOGIE_";

-    private const string BOOGIE_VAR_PREFIX= "__BOOGIE_";

+    private const string BOOGIE_VAR_PREFIX = "__BOOGIE_";

     public const string IL_CURRENT_NAVIGATION_URI_VARIABLE = IL_BOOGIE_VAR_PREFIX + "CurrentNavigationURI__";

     public const string BOOGIE_CONTINUE_ON_PAGE_VARIABLE = BOOGIE_VAR_PREFIX + "ContinueOnPage__";

     public static readonly string[] NAV_CALLS = { /*"GoBack", "GoForward", "Navigate", "StopLoading"*/ "Navigate", "GoBack" };

@@ -46,7 +46,7 @@ namespace BytecodeTranslator.Phone {
     /// <param name="bplObject"></param>

     /// <returns>true if defining a new name, false if replacing</returns>

     public static bool setBoogieObjectForName(string name, Bpl.NamedDeclaration bplObject) {

-      bool ret= true;

+      bool ret = true;

       if (boogieObjects.ContainsKey(name))

         ret = false;

 

@@ -75,7 +75,7 @@ namespace BytecodeTranslator.Phone {
       return typeRef.isClass(targetType);

     }

 

-    public static bool isURIClass (this ITypeReference typeRef, IMetadataHost host) {

+    public static bool isURIClass(this ITypeReference typeRef, IMetadataHost host) {

       Microsoft.Cci.Immutable.PlatformType platformType = host.PlatformType as Microsoft.Cci.Immutable.PlatformType;

       if (platformType == null)

         return false;

@@ -84,7 +84,7 @@ namespace BytecodeTranslator.Phone {
       AssemblyIdentity systemAssemblyId = new AssemblyIdentity(host.NameTable.GetNameFor("System"), "", coreRef.Version, coreRef.PublicKeyToken, "");

       IAssemblyReference systemAssembly = host.FindAssembly(systemAssemblyId);

 

-      ITypeReference uriTypeRef= platformType.CreateReference(systemAssembly, "System", "Uri");

+      ITypeReference uriTypeRef = platformType.CreateReference(systemAssembly, "System", "Uri");

       return typeRef.isClass(uriTypeRef);

     }

 

@@ -158,9 +158,9 @@ namespace BytecodeTranslator.Phone {
       IList<string> constantStrings = new List<string>();

 

       // TODO this misses so many static strings, but let's start with this for now

-      IExpression leftOp= stringConcatExpr.Arguments.FirstOrDefault();

+      IExpression leftOp = stringConcatExpr.Arguments.FirstOrDefault();

       while (leftOp != null && leftOp is ICompileTimeConstant) {

-        ICompileTimeConstant strConst= leftOp as ICompileTimeConstant;

+        ICompileTimeConstant strConst = leftOp as ICompileTimeConstant;

         constantStrings.Add(strConst.Value as string);

         if (stringConcatExpr.Arguments.ToList()[1] is IMethodCall) {

           stringConcatExpr = stringConcatExpr.Arguments.ToList()[1] as IMethodCall;

@@ -173,7 +173,7 @@ namespace BytecodeTranslator.Phone {
         }

       }

 

-      uri= constantStrings.Aggregate((aggr, elem) => aggr + elem);

+      uri = constantStrings.Aggregate((aggr, elem) => aggr + elem);

       return Uri.IsWellFormedUriString(uri, UriKind.RelativeOrAbsolute);

     }

 

@@ -202,7 +202,7 @@ namespace BytecodeTranslator.Phone {
         realUri = new Uri(mockBaseUri, uri);

       }

 

-      string str= realUri.GetComponents(UriComponents.Path|UriComponents.StrongAuthority|UriComponents.Scheme, UriFormat.UriEscaped);

+      string str = realUri.GetComponents(UriComponents.Path | UriComponents.StrongAuthority | UriComponents.Scheme, UriFormat.UriEscaped);

       Uri mockStrippedUri = new Uri(str);

       return mockBaseUri.MakeRelativeUri(mockStrippedUri).ToString();

     }

@@ -215,5 +215,21 @@ namespace BytecodeTranslator.Phone {
     public static ITypeReference getMainAppTypeReference() {

       return mainAppTypeRef;

     }

+

+    public static void setBoogieNavigationVariable(string var) {

+      PhonePlugin.setBoogieNavigationVariable(var);

+    }

+

+    public static string getBoogieNavigationVariable() {

+      return PhonePlugin.getBoogieNavigationVariable();

+    }

+

+    public static string getXAMLForPage(string pageClass) {

+      return PhonePlugin.getXAMLForPage(pageClass);

+    }

+

+    public static void setBoogieStringPageNameForPageClass(string pageClass, string boogieStringName) {

+      PhonePlugin.setBoogieStringPageNameForPageClass(pageClass, boogieStringName);

+    }

   }

 }

diff --git a/BCT/PhoneControlsExtractor/PhoneBoogieCodeGenerator.py b/BCT/PhoneControlsExtractor/PhoneBoogieCodeGenerator.py
index c9a63c92..092acc5b 100644
--- a/BCT/PhoneControlsExtractor/PhoneBoogieCodeGenerator.py
+++ b/BCT/PhoneControlsExtractor/PhoneBoogieCodeGenerator.py
@@ -12,6 +12,7 @@ CONTINUEONPAGE_VAR= "__BOOGIE_ContinueOnPage__"
 

 staticControlsMap= {}

 mainPageXAML= None

+currentNavigationVariable= None

 originalPageVars= []

 boogiePageVars= []

 boogiePageClasses= []

@@ -42,7 +43,10 @@ def outputPageVariables(file):
   for entry in staticControlsMap.keys():

     pageVarName= "__BOOGIE_PAGE_VAR_" + entry

     originalPageVars.append(entry)

-    boogiePageVars.append(pageVarName)

+    pageInfo={}

+    pageInfo["name"]=pageVarName

+    pageInfo["boogieStringName"]= staticControlsMap[entry]["boogieStringName"]

+    boogiePageVars.append(pageInfo)

     boogiePageClasses.append(staticControlsMap[entry]["class"])

     pageVar= "var " + pageVarName + ": Ref;\n"

     file.write(pageVar)

@@ -57,7 +61,7 @@ def outputMainProcedure(file):
   file.write("\tvar $control: Ref;\n\n")

 

   for i in range(0,len(boogiePageVars)):

-    file.write("\tcall " + boogiePageClasses[i] + ".#ctor(" + boogiePageVars[i] + ");\n")

+    file.write("\tcall " + boogiePageClasses[i] + ".#ctor(" + boogiePageVars[i]["name"] + ");\n")

 

   file.write("\t//TODO still need to call Loaded handler on main page and the App ctor.\n")

   file.write("\thavoc $doWork;\n")

@@ -114,16 +118,16 @@ def outputPageControlDriver(file, originalPageName, boogiePageName):
 

 def outputControlDrivers(file):

   for i in range(0,len(boogiePageVars)):

-    outputPageControlDriver(file, originalPageVars[i],boogiePageVars[i])

+    outputPageControlDriver(file, originalPageVars[i],boogiePageVars[i]["name"])

 

   file.write("procedure DriveControls();\n")

   file.write("implementation DriveControls() {\n")

   for i in range(0,len(boogiePageVars)):

-    file.write("\tvar isCurrent" + boogiePageVars[i] + ": bool;\n")

+    file.write("\tvar isCurrent" + boogiePageVars[i]["name"] + ": bool;\n")

   file.write("\n")

 

   for i in range(0,len(boogiePageVars)):

-    file.write("\t//TODO call isCurrent" + boogiePageVars[i] + " := System.String.op_Equality$System.String$System.String(" + "BOOGIE_CURRENT_VAR" + "," + "BOOGIE_PAGE_APPROPRIATE_CONSTANT_STRING" + ");\n")

+    file.write("\tcall isCurrent" + boogiePageVars[i]["name"] + " := System.String.op_Equality$System.String$System.String(" + currentNavigationVariable + "," + boogiePageVars[i]["boogieStringName"] + ");\n")

 

   firstTime= True

   for i in range(0,len(boogiePageVars)):

@@ -133,15 +137,14 @@ def outputControlDrivers(file):
     else:

       file.write("\telse if")

 

-    file.write(" (isCurrent" + boogiePageVars[i] +  ") {\n")

-    file.write("\t\t call drive" + boogiePageVars[i] + "Controls();\n\t}\n")

+    file.write(" (isCurrent" + boogiePageVars[i]["name"] +  ") {\n")

+    file.write("\t\t call drive" + boogiePageVars[i]["name"] + "Controls();\n\t}\n")

   file.write("}\n")

 

 def outputURIHavocProcedure(file):

   file.write("procedure __BOOGIE_Havoc_CurrentURI__();\n")

   file.write("implementation __BOOGIE_Havoc_CurrentURI__() {\n")

-  file.write("// TODO change this name to a dynamically inferred one. This is just for testing right now\n")

-  file.write("\thavoc SimpleNavigationApp.App.$__BOOGIE_CurrentNavigationURI__;\n")

+  file.write("\thavoc " + currentNavigationVariable + ";\n")

   file.write("// TODO write assume statements to filter havoc'd variable to either of all pages\n")

   # file.write("\tassume )

   file.write("}\n")

@@ -156,15 +159,17 @@ def outputBoilerplate(outputFile):
 

 def buildControlInfo(controlInfoFileName):

   global mainPageXAML

+  global currentNavigationVariable

   global staticControlsMap

 

   file = open(controlInfoFileName, "r")

-  # Info file format is first line containing only the main page, and then one line per

-  # <pageClassName>,<page.xaml file>,<controlClassName>,<controlName (as in field name)>,<IsEnabledValue>,<VisibilityValue>,<ClickValue>,<CheckedValue>,<UncheckedValue>,<BoogieName>

+  # Info file format is first line containing only the main page, another line with boogie's current navigation variable and then one line per

+  # <pageClassName>,<page.xaml file>,<xaml boogie string representation>,<controlClassName>,<controlName (as in field name)>,<IsEnabledValue>,<VisibilityValue>,<ClickValue>,<CheckedValue>,<UncheckedValue>,<BoogieName>

   mainPageXAML= file.readline().strip()

+  currentNavigationVariable= file.readline().strip()

   infoLine= file.readline().strip()

   while not infoLine == "":

-    pageClass, pageName, controlClass, controlName, enabled, visible, clickHandler, checkedHandler, uncheckedHandler, bplName= infoLine.split(",")

+    pageClass, pageName, pageBoogieStringName, controlClass, controlName, enabled, visible, clickHandler, checkedHandler, uncheckedHandler, bplName= infoLine.split(",")

     pageInfo={}

     pageInfo["class"]=pageClass

     try:

@@ -172,6 +177,7 @@ def buildControlInfo(controlInfoFileName):
     except KeyError:

       staticControlsMap[pageName]=pageInfo

 

+    pageInfo["boogieStringName"]= pageBoogieStringName

     pageControlInfo={}

     try:

       pageControlInfo= pageInfo["controls"]

diff --git a/BCT/PhoneControlsExtractor/PhoneControlsExtractor.py b/BCT/PhoneControlsExtractor/PhoneControlsExtractor.py
index f4b3d6f4..4fe4e18f 100644
--- a/BCT/PhoneControlsExtractor/PhoneControlsExtractor.py
+++ b/BCT/PhoneControlsExtractor/PhoneControlsExtractor.py
@@ -103,9 +103,10 @@ def extractPhoneControlsFromPage(pageXAML):
 def outputPhoneControls(outputFileName):

   outputFile= open(outputFileName, "w")

 

-  # Output format is first line containing only the main page, and then one line per

-  # <pageClassName>,<page.xaml file>,<controlClassName>,<controlName (as in field name)>,<IsEnabledValue>,<VisibilityValue>,<ClickValue>,<CheckedValue>,<UncheckedValue>

+  # Output format is first line containing only the main page, then line containing boogie navigation variable, and then one line per

+  # <pageClassName>,<page.xaml file>,<boogie string page name>,<controlClassName>,<controlName (as in field name)>,<IsEnabledValue>,<VisibilityValue>,<ClickValue>,<CheckedValue>,<UncheckedValue>

   outputFile.write(mainPageXAML + "\n")

+  outputFile.write("dummyNavigationVariable_unknown\n")

   for page in staticControlsMap.keys():

     for control in staticControlsMap[page]:

       isEnabled= control["IsEnabled"]

@@ -115,7 +116,8 @@ def outputPhoneControls(outputFileName):
       unchecked= control["Unchecked"]

       pageXAML= control["XAML"]

       # last comma is to account for bpl translation name, that is unknown for now

-      outputFile.write(page + "," + os.path.basename(pageXAML) + "," + control["Type"] + "," + control["Name"] + "," + isEnabled + "," + visibility + "," + click + "," + checked + "," + unchecked + ",\n")

+      # boogie string page name is unknown for now

+      outputFile.write(page + "," + os.path.basename(pageXAML) + ",dummyBoogieStringPageName," + control["Type"] + "," + control["Name"] + "," + isEnabled + "," + visibility + "," + click + "," + checked + "," + unchecked + ",\n")

 

   outputFile.close()

 

diff --git a/BCT/TranslationPlugins/PhoneControlsPlugin.cs b/BCT/TranslationPlugins/PhoneControlsPlugin.cs
index 201d47d8..3d5b81c3 100644
--- a/BCT/TranslationPlugins/PhoneControlsPlugin.cs
+++ b/BCT/TranslationPlugins/PhoneControlsPlugin.cs
@@ -68,6 +68,7 @@ namespace TranslationPlugins {
       controlsInfo = new Dictionary<string, ControlInfoStructure>();

     }

 

+    public string PageBoogieName { get; set; }

     public string PageClassName { get; set; }

     public string PageXAML { get; set; }

     public bool IsMainPage { get; set; }

@@ -93,17 +94,18 @@ namespace TranslationPlugins {
   public class PhoneControlsPlugin : TranslationPlugin {

     // TODO this will probably need a complete rewrite once it is event based, and make it more push than pull

     // TODO but it doesn't make sense right now to make it BCT or CCI aware

-    private static int CONFIG_LINE_FIELDS= 10;

+    private static int CONFIG_LINE_FIELDS= 11;

     private static int PAGE_CLASS_FIELD= 0;

     private static int PAGE_XAML_FIELD= 1;

-    private static int CONTROL_CLASS_FIELD= 2;

-    private static int CONTROL_NAME_FIELD= 3;

-    private static int ENABLED_FIELD= 4;

-    private static int VISIBILITY_FIELD= 5;

-    private static int CLICK_HANDLER_FIELD= 6;

-    private static int CHECKED_HANDLER_FIELD= 7;

-    private static int UNCHECKED_HANDLER_FIELD = 8;

-    private static int BPL_NAME_FIELD = 9;

+    private static int PAGE_BOOGIE_STRING_FIELD = 2;

+    private static int CONTROL_CLASS_FIELD= 3;

+    private static int CONTROL_NAME_FIELD= 4;

+    private static int ENABLED_FIELD= 5;

+    private static int VISIBILITY_FIELD= 6;

+    private static int CLICK_HANDLER_FIELD= 7;

+    private static int CHECKED_HANDLER_FIELD= 8;

+    private static int UNCHECKED_HANDLER_FIELD = 9;

+    private static int BPL_NAME_FIELD = 10;

 

     private IDictionary<string, PageStructure> pageStructureInfo;

 

@@ -138,6 +140,15 @@ namespace TranslationPlugins {
       return entry.Value.PageXAML;

     }

 

+    private string boogieCurrentNavigationVariable;

+    public string getBoogieNavigationVariable() {

+      return boogieCurrentNavigationVariable;

+    }

+

+    public void setBoogieNavigationVariable(string var) {

+      boogieCurrentNavigationVariable = var;

+    }

+

     private void setPageAsMainPage(string pageXAML) {

       KeyValuePair<string,PageStructure> mainPageClass= pageStructureInfo.FirstOrDefault(keyValue => keyValue.Value.PageXAML == pageXAML);

       if (mainPageClass.Equals(default(KeyValuePair<string, PageStructure>))) {

@@ -149,11 +160,13 @@ namespace TranslationPlugins {
 

     public void DumpControlStructure(StreamWriter outputStream) {

       // maintain same format as input format

-      string pageClass, pageXAML, controlClass, controlName, enabled, visibility, clickHandler, checkedHandler, uncheckedHandler, bplName;

+      string pageClass, pageXAML, pageBoogieStringName, controlClass, controlName, enabled, visibility, clickHandler, checkedHandler, uncheckedHandler, bplName;

       outputStream.WriteLine(getMainPageXAML());

+      outputStream.WriteLine(getBoogieNavigationVariable());

       foreach (KeyValuePair<string, PageStructure> entry in this.pageStructureInfo) {

         pageClass = entry.Key;

         pageXAML = entry.Value.PageXAML;

+        pageBoogieStringName = entry.Value.PageBoogieName;

         foreach (ControlInfoStructure controlInfo in entry.Value.getAllControlsInfo()) {

           controlClass= controlInfo.ClassName;

           controlName = controlInfo.Name;

@@ -187,15 +200,19 @@ namespace TranslationPlugins {
             uncheckedHandler = "";

           }

           bplName = controlInfo.BplName;

-          outputStream.WriteLine(pageClass + "," + pageXAML + "," + controlClass + "," + controlName + "," + enabled + "," + visibility + "," + clickHandler + "," + checkedHandler + "," + uncheckedHandler + "," + bplName);

+          outputStream.WriteLine(pageClass + "," + pageXAML + "," + pageBoogieStringName + "," + controlClass + "," + controlName + "," + enabled + "," + visibility + "," + clickHandler + "," + checkedHandler + "," + uncheckedHandler + "," + bplName);

         }

       }

     }

 

+    public void setBoogieStringPageNameForPageClass(string pageClass, string boogieStringPageName) {

+      pageStructureInfo[pageClass].PageBoogieName = boogieStringPageName;

+    }

+

     private void LoadControlStructure(StreamReader configStream) {

       // TODO it would be nice to have some kind of dynamic definition of config format

       // TODO for now remember that config format is CSV

-      // TODO each line is <pageClassName>,<pageXAMLPath>,<controlClassName>,<controlName>,<IsEnabledValue>,<VisibilityValue>,<ClickValue>,<CheckedValue>,<UncheckedValue>,<BPL control name>

+      // TODO each line is <pageClassName>,<pageXAMLPath>,<pageBoogieStringName>,<controlClassName>,<controlName>,<IsEnabledValue>,<VisibilityValue>,<ClickValue>,<CheckedValue>,<UncheckedValue>,<BPL control name>

       // TODO BPL control name will most probably be empty, but it is useful to be able to dump it

       // TODO check PhoneControlsExtractor.py

 

@@ -203,17 +220,25 @@ namespace TranslationPlugins {
       // TODO I'm not handling this for now, and I won't be handling relative/absolute URI either for now

 

       try {

-        string pageClass, pageXAML, controlClass, controlName, enabled, visibility, clickHandler, checkedHandler, uncheckedHandler, bplName;

+        string pageClass, pageXAML, pageBoogieStringName, controlClass, controlName, enabled, visibility, clickHandler, checkedHandler, uncheckedHandler, bplName;

         string configLine = configStream.ReadLine();

         string[] inputLine;

         PageStructure pageStr;

         ControlInfoStructure controlInfoStr;

 

         // first line just states the main page xaml

-        string mainPage = configLine.Trim();

+        string mainPageXAML= configLine.Trim();

         configLine = configStream.ReadLine();

 

+        // second line states boogie current nav variable, possibly dummy value

+        setBoogieNavigationVariable(configLine.Trim());

+        configLine= configStream.ReadLine();

+

         while (configLine != null) {

+          if (configLine.Trim().Equals(string.Empty)) {

+            configLine = configStream.ReadLine();

+            continue;

+          }

           inputLine = configLine.Split(',');

 

           if (inputLine.Length != CONFIG_LINE_FIELDS)

@@ -221,6 +246,7 @@ namespace TranslationPlugins {
 

           pageClass = inputLine[PAGE_CLASS_FIELD];

           pageXAML = inputLine[PAGE_XAML_FIELD];

+          pageBoogieStringName = inputLine[PAGE_BOOGIE_STRING_FIELD];

           controlClass = inputLine[CONTROL_CLASS_FIELD];

           controlName = inputLine[CONTROL_NAME_FIELD];

           enabled = inputLine[ENABLED_FIELD];

@@ -236,6 +262,7 @@ namespace TranslationPlugins {
             pageStr = new PageStructure();

             pageStr.PageClassName = pageClass;

             pageStr.PageXAML = pageXAML;

+            pageStr.PageBoogieName = pageBoogieStringName;

             pageStr.IsMainPage = false;

           }

 

@@ -255,9 +282,9 @@ namespace TranslationPlugins {
           pageStr.setControlInfo(controlName, controlInfoStr);

           pageStructureInfo[pageClass] = pageStr;

           configLine = configStream.ReadLine();

-

-          setPageAsMainPage(mainPage);

         }

+

+        setPageAsMainPage(mainPageXAML);

       } catch (Exception) {

         // TODO log, I don't want to terminate BCT because of this

       }