diff options
| -rw-r--r-- | BCT/PhoneControlsExtractor/PhoneBoogieCodeGenerator.py | 39 |
1 files changed, 27 insertions, 12 deletions
diff --git a/BCT/PhoneControlsExtractor/PhoneBoogieCodeGenerator.py b/BCT/PhoneControlsExtractor/PhoneBoogieCodeGenerator.py index e5c412c0..886eaa91 100644 --- a/BCT/PhoneControlsExtractor/PhoneBoogieCodeGenerator.py +++ b/BCT/PhoneControlsExtractor/PhoneBoogieCodeGenerator.py @@ -57,7 +57,7 @@ def outputPageVariables(file): pageVar= "var " + pageVarName + ": Ref;\n"
file.write(pageVar)
-def outputMainProcedure(file):
+def outputMainProcedures(file, batFile):
for i,j in product(range(0, len(boogiePageVars)),repeat=2):
if i == j:
continue
@@ -66,9 +66,6 @@ def outputMainProcedure(file): if (boogiePageVars[j]["boogieStringName"] == dummyPageVar):
continue
- print "continuing with i " + str(i) + ", j " + str(j)
- print boogiePageVars[i]["boogieStringName"]
- print boogiePageVars[j]["boogieStringName"]
file.write("procedure __BOOGIE_VERIFICATION_PROCEDURE_" + str(i) + "_" + str(j) + "();\n")
file.write("implementation __BOOGIE_VERIFICATION_PROCEDURE_" + str(i) + "_" + str(j) + "() {\n")
file.write("\tvar $doWork: bool;\n")
@@ -94,6 +91,13 @@ def outputMainProcedure(file): file.write("\tassert false;\n");
file.write("}\n")
+ batFile.write("type BOOGIE_PARTIAL.bpl > BOOGIE_PLACEHOLDER.bpl\n")
+ batFile.write("type BOOGIE_BOILERPLATE.bpl >> BOOGIE_PLACEHOLDER.bpl\n")
+ batFile.write("%POIROT_ROOT%\Corral\BctCleanup.exe BOOGIE_PLACEHOLDER.bpl BOOGIE_PLACEHOLDER_Clean.bpl /main:__BOOGIE_VERIFICATION_PROCEDURE_" + str(i) + "_" + str(j) +"\n");
+ batFile.write("del corral_out_trace.txt\n")
+ batFile.write("%POIROT_ROOT%\corral\corral.exe /k:1 /recursionBound:20 /main:__BOOGIE_VERIFICATION_PROCEDURE_" + str(i) +"_" + str(j) + " BOOGIE_PLACEHOLDER_Clean_" + str(i) + "_" + str(j) + ".bpl\n")
+ batFile.write("if exist corral_out_trace.txt move corral_out_trace.txt corral_out_trace_" + str(i) + "_" + str(j) + ".txt\n")
+
def outputPageControlDriver(file, originalPageName, boogiePageName):
file.write("procedure drive" + boogiePageName + "Controls();\n")
file.write("implementation drive" + boogiePageName + "Controls() {\n")
@@ -107,10 +111,14 @@ def outputPageControlDriver(file, originalPageName, boogiePageName): file.write("\thavoc $activeControl;\n")
file.write("\twhile (" + CONTINUEONPAGE_VAR + ") {\n")
activeControl=0
+ ifInitialized= False
for entry in staticControlsMap[originalPageName]["controls"].keys():
controlInfo= staticControlsMap[originalPageName]["controls"][entry]
- if activeControl==0:
- file.write("\t\tif ($activeControl == 0) {\n")
+ if controlInfo["bplName"] == "":
+ continue
+ if not ifInitialized:
+ file.write("\t\tif ($activeControl == str(activeControl)) {\n")
+ ifInitialized= True
else:
file.write("\t\telse if ($activeControl == " + str(activeControl) + ") {\n")
@@ -139,7 +147,7 @@ def outputPageControlDriver(file, originalPageName, boogiePageName): file.write("}\n")
-def outputControlDrivers(file):
+def outputControlDrivers(file, batFile):
for i in range(0,len(boogiePageVars)):
outputPageControlDriver(file, originalPageVars[i],boogiePageVars[i]["name"])
@@ -150,7 +158,10 @@ def outputControlDrivers(file): file.write("\n")
for i in range(0,len(boogiePageVars)):
- file.write("\tcall isCurrent" + boogiePageVars[i]["name"] + " := System.String.op_Equality$System.String$System.String(" + currentNavigationVariable + "," + boogiePageVars[i]["boogieStringName"] + ");\n")
+ if boogiePageVars[i]["boogieStringName"] == dummyPageVar:
+ file.write("\tisCurrent" + boogiePageVars[i]["name"] + " := false;\n")
+ else:
+ 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)):
@@ -172,13 +183,17 @@ def outputURIHavocProcedure(file): # file.write("\tassume )
file.write("}\n")
-def outputBoilerplate(outputFile):
+#build a batch file for test running at the same time
+def outputBoilerplate(outputFile, cmdFile):
file= open(outputFile,"w")
+ batFile= open(cmdFile, "w")
+ batFile.write("del corral_out_trace.txt")
outputPageVariables(file)
outputURIHavocProcedure(file)
- outputControlDrivers(file)
- outputMainProcedure(file)
+ outputControlDrivers(file, batFile)
+ outputMainProcedures(file, batFile)
file.close()
+ batFile.close()
def buildControlInfo(controlInfoFileName):
global mainPageXAML
@@ -238,7 +253,7 @@ def main(): outputFile= a
buildControlInfo(controlFile)
- outputBoilerplate(outputFile)
+ outputBoilerplate(outputFile, outputFile + ".bat")
if __name__ == "__main__":
main()
\ No newline at end of file |