diff options
Diffstat (limited to 'BCT')
| -rw-r--r-- | BCT/BytecodeTranslator/Heap.cs | 7 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/MetadataTraverser.cs | 4 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs | 24 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs | 10 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs | 34 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/Program.cs | 26 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/Sink.cs | 6 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/StatementTraverser.cs | 11 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/TranslationHelper.cs | 2 | ||||
| -rw-r--r-- | BCT/PhoneControlsExtractor/PhoneBoogieCodeGenerator.py | 30 | ||||
| -rw-r--r-- | BCT/PhoneControlsExtractor/PhoneControlsExtractor.py | 12 | ||||
| -rw-r--r-- | BCT/RegressionTests/RegressionTestInput/Class1.cs | 7 | ||||
| -rw-r--r-- | BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt | 350 | ||||
| -rw-r--r-- | BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt | 270 | ||||
| -rw-r--r-- | BCT/RegressionTests/TranslationTest/UnitTest0.cs | 2 | ||||
| -rw-r--r-- | BCT/TranslationPlugins/PhoneControlsPlugin.cs | 56 |
16 files changed, 548 insertions, 303 deletions
diff --git a/BCT/BytecodeTranslator/Heap.cs b/BCT/BytecodeTranslator/Heap.cs index 751d8baa..648d4c9f 100644 --- a/BCT/BytecodeTranslator/Heap.cs +++ b/BCT/BytecodeTranslator/Heap.cs @@ -205,11 +205,8 @@ namespace BytecodeTranslator { /// </summary>
public override Bpl.Variable CreateFieldVariable(IFieldReference field) {
Bpl.Variable v;
- string fieldname = TypeHelper.GetTypeName(field.ContainingType) + "." + field.Name.Value;
+ string fieldname = MemberHelper.GetMemberSignature(field, NameFormattingOptions.DocumentationId);
fieldname = TranslationHelper.TurnStringIntoValidIdentifier(fieldname);
- // Need to append something to the name to avoid name clashes with other members (of a different
- // type) that have the same name.
- fieldname += "$field";
Bpl.IToken tok = field.Token();
if (field.IsStatic) {
@@ -227,7 +224,7 @@ namespace BytecodeTranslator { public override Bpl.Variable CreateEventVariable(IEventDefinition e) {
Bpl.Variable v;
- string fieldname = TypeHelper.GetTypeName(e.ContainingType) + "." + e.Name.Value;
+ string fieldname = MemberHelper.GetMemberSignature(e, NameFormattingOptions.DocumentationId);
fieldname = TranslationHelper.TurnStringIntoValidIdentifier(fieldname);
Bpl.IToken tok = e.Token();
diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs index f6903b8a..30def4a2 100644 --- a/BCT/BytecodeTranslator/MetadataTraverser.cs +++ b/BCT/BytecodeTranslator/MetadataTraverser.cs @@ -122,7 +122,7 @@ namespace BytecodeTranslator { string fullyQualifiedName = namedTypeDef.ToString();
string xamlForClass = PhoneCodeHelper.instance().getXAMLForPage(fullyQualifiedName);
if (xamlForClass != null) { // if not it is possibly an abstract page
- string uriName = PhoneControlsPlugin.getURIBase(xamlForClass);
+ string uriName = UriHelper.getURIBase(xamlForClass);
Bpl.Constant uriConstant = sink.FindOrCreateConstant(uriName);
PhoneCodeHelper.instance().setBoogieStringPageNameForPageClass(fullyQualifiedName, uriConstant.Name);
}
@@ -223,7 +223,7 @@ namespace BytecodeTranslator { private bool sawCctor = false;
private void CreateStaticConstructor(ITypeDefinition typeDefinition) {
- var typename = TypeHelper.GetTypeName(typeDefinition);
+ var typename = TypeHelper.GetTypeName(typeDefinition, Microsoft.Cci.NameFormattingOptions.DocumentationId);
typename = TranslationHelper.TurnStringIntoValidIdentifier(typename);
var proc = new Bpl.Procedure(Bpl.Token.NoToken, typename + ".#cctor",
new Bpl.TypeVariableSeq(),
diff --git a/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs b/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs index 6be74264..cd71e7cc 100644 --- a/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs +++ b/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs @@ -10,6 +10,28 @@ using Microsoft.Cci.MutableCodeModel; namespace BytecodeTranslator.Phone {
public static class UriHelper {
/// <summary>
+ /// uri is a valid URI but possibly partial (incomplete ?arg= values) and overspecified (complete ?arg=values)
+ /// This method returns a base URI
+ /// </summary>
+ /// <param name="uri"></param>
+ /// <returns></returns>
+ public static string getURIBase(string uri) {
+ // I need to build an absolute URI just to call getComponents() ...
+ Uri mockBaseUri = new Uri("mock://mock/", UriKind.RelativeOrAbsolute);
+ Uri realUri;
+ try {
+ realUri = new Uri(uri, UriKind.Absolute);
+ } catch (UriFormatException) {
+ // uri string is relative
+ realUri = new Uri(mockBaseUri, uri);
+ }
+
+ string str = realUri.GetComponents(UriComponents.Path | UriComponents.StrongAuthority | UriComponents.Scheme, UriFormat.UriEscaped);
+ Uri mockStrippedUri = new Uri(str);
+ return mockBaseUri.MakeRelativeUri(mockStrippedUri).ToString();
+ }
+
+ /// <summary>
/// checks if argument is locally created URI with static URI target
/// </summary>
/// <param name="arg"></param>
@@ -32,7 +54,7 @@ namespace BytecodeTranslator.Phone { if (staticURITarget == null)
return false;
- uri = staticURITarget.Value as string;
+ uri= staticURITarget.Value as string;
return true;
}
diff --git a/BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs b/BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs index 4d1f60fb..d79d2c00 100644 --- a/BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs +++ b/BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs @@ -31,6 +31,7 @@ namespace BytecodeTranslator.Phone { private IAssemblyReference coreAssemblyRef;
private IAssemblyReference phoneAssembly;
private IAssemblyReference phoneSystemWindowsAssembly;
+ private IAssemblyReference MSPhoneControlsAssembly;
private INamespaceTypeReference appBarIconButtonType;
private INamespaceTypeReference checkBoxType;
private INamespaceTypeReference radioButtonType;
@@ -39,6 +40,7 @@ namespace BytecodeTranslator.Phone { private INamespaceTypeReference toggleButtonType;
private INamespaceTypeReference controlType;
private INamespaceTypeReference uiElementType;
+ private INamespaceTypeReference pivotType;
private CompileTimeConstant trueConstant;
private CompileTimeConstant falseConstant;
@@ -65,6 +67,8 @@ namespace BytecodeTranslator.Phone { return checkBoxType;
} else if (classname == "ApplicationBarIconButton") {
return appBarIconButtonType;
+ } else if (classname == "Pivot") {
+ return pivotType;
} else if (classname == "DummyType") {
return Dummy.Type;
} else {
@@ -87,12 +91,17 @@ namespace BytecodeTranslator.Phone { AssemblyIdentity MSPhoneAssemblyId =
new AssemblyIdentity(host.NameTable.GetNameFor("Microsoft.Phone"), "", new Version("7.0.0.0"),
new byte[] { 0x24, 0xEE, 0xC0, 0xD8, 0xC8, 0x6C, 0xDA, 0x1E }, "");
+ AssemblyIdentity MSPhoneControlsAssemblyId=
+ new AssemblyIdentity(host.NameTable.GetNameFor("Microsoft.Phone.Controls"), "", new Version("7.0.0.0"),
+ new byte[] { 0x24, 0xEE, 0xC0, 0xD8, 0xC8, 0x6C, 0xDA, 0x1E }, "");
+
AssemblyIdentity MSPhoneSystemWindowsAssemblyId =
new AssemblyIdentity(host.NameTable.GetNameFor("System.Windows"), coreAssemblyRef.Culture, coreAssemblyRef.Version,
coreAssemblyRef.PublicKeyToken, "");
phoneAssembly = host.FindAssembly(MSPhoneAssemblyId);
phoneSystemWindowsAssembly = host.FindAssembly(MSPhoneSystemWindowsAssemblyId);
+ MSPhoneControlsAssembly= host.FindAssembly(MSPhoneControlsAssemblyId);
// TODO determine the needed types dynamically
appBarIconButtonType= platform.CreateReference(phoneAssembly, "Microsoft", "Phone", "Shell", "ApplicationBarIconButton");
@@ -103,6 +112,7 @@ namespace BytecodeTranslator.Phone { toggleButtonType = platform.CreateReference(phoneSystemWindowsAssembly, "System", "Windows", "Controls", "Primitives", "ToggleButton");
controlType = platform.CreateReference(phoneSystemWindowsAssembly, "System", "Windows", "Controls", "Control");
uiElementType = platform.CreateReference(phoneSystemWindowsAssembly, "System", "Windows", "UIElement");
+ pivotType = platform.CreateReference(MSPhoneControlsAssembly, "Microsoft", "Phone", "Controls", "Pivot");
trueConstant = new CompileTimeConstant() {
Type = platform.SystemBoolean,
diff --git a/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs b/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs index f94f0044..2d3533aa 100644 --- a/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs +++ b/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs @@ -13,6 +13,8 @@ namespace BytecodeTranslator.Phone { private ITypeReference cancelEventArgsType;
private ITypeReference typeTraversed;
private IMethodDefinition methodTraversed;
+ private static HashSet<IMethodDefinition> navCallers= new HashSet<IMethodDefinition>();
+ public static IEnumerable<IMethodDefinition> NavCallers { get { return navCallers; } }
public PhoneNavigationCodeTraverser(MetadataReaderHost host, ITypeReference typeTraversed, IMethodDefinition methodTraversed) : base() {
this.host = host;
@@ -29,10 +31,13 @@ namespace BytecodeTranslator.Phone { cancelEventArgsType = platform.CreateReference(assembly, "System", "ComponentModel", "CancelEventArgs");
}
+ public override void Visit(IEnumerable<IAssemblyReference> assemblyReferences) {
+ base.Visit(assemblyReferences);
+ }
+
+
public override void Visit(IMethodDefinition method) {
if (method.IsConstructor && PhoneTypeHelper.isPhoneApplicationClass(typeTraversed, host)) {
- // TODO BUG doing this is generating a fresh variable definition somewhere that the BCT then translates into two different (identical) declarations
- // TODO maybe a bug introduced here or a BCT bug
string mainPageUri = PhoneCodeHelper.instance().PhonePlugin.getMainPageXAML();
SourceMethodBody sourceBody = method.Body as SourceMethodBody;
if (sourceBody != null) {
@@ -41,7 +46,7 @@ namespace BytecodeTranslator.Phone { Assignment uriInitAssign = new Assignment() {
Source = new CompileTimeConstant() {
Type = host.PlatformType.SystemString,
- Value = PhoneControlsPlugin.getURIBase(mainPageUri),
+ Value = UriHelper.getURIBase(mainPageUri),
},
Type = host.PlatformType.SystemString,
Target = new TargetExpression() {
@@ -78,10 +83,13 @@ namespace BytecodeTranslator.Phone { navCallFound = false;
navCallIsStatic = false;
this.Visit(statement);
- if (navCallFound && navCallIsStatic) {
- staticNavStmts.Add(new Tuple<IStatement, StaticURIMode, string>(statement, currentStaticMode, unpurifiedFoundURI));
- } else if (navCallFound) {
- nonStaticNavStmts.Add(statement);
+ if (navCallFound) {
+ navCallers.Add(methodTraversed);
+ if (navCallIsStatic) {
+ staticNavStmts.Add(new Tuple<IStatement, StaticURIMode, string>(statement, currentStaticMode, unpurifiedFoundURI));
+ } else {
+ nonStaticNavStmts.Add(statement);
+ }
}
}
@@ -106,6 +114,8 @@ namespace BytecodeTranslator.Phone { UriHelper.isArgumentURILocallyCreatedStaticRoot(expr, host, out target);
if (!isStatic)
target = "--Other non inferrable target--";
+ else
+ target = UriHelper.getURIBase(target);
} catch (InvalidOperationException) {
}
}
@@ -140,11 +150,13 @@ namespace BytecodeTranslator.Phone { string target;
if (isNavigationOnBackKeyPressHandler(methodCall, out target)) {
PhoneCodeHelper.instance().BackKeyPressNavigates = true;
- ICollection<string> targets = PhoneCodeHelper.instance().BackKeyNavigatingOffenders[typeTraversed];
- if (targets == null) {
+ ICollection<string> targets;
+ try {
+ targets= PhoneCodeHelper.instance().BackKeyNavigatingOffenders[typeTraversed];
+ } catch (KeyNotFoundException) {
targets = new HashSet<string>();
}
- targets.Add(target);
+ targets.Add("\"" + target + "\"");
PhoneCodeHelper.instance().BackKeyNavigatingOffenders[typeTraversed]= targets;
} else if (isCancelOnBackKeyPressHandler(methodCall)) {
PhoneCodeHelper.instance().BackKeyPressHandlerCancels = true;
@@ -247,7 +259,7 @@ namespace BytecodeTranslator.Phone { Assignment currentURIAssign = new Assignment() {
Source = new CompileTimeConstant() {
Type = host.PlatformType.SystemString,
- Value = PhoneControlsPlugin.getURIBase(entry.Item3),
+ Value = UriHelper.getURIBase(entry.Item3).ToLower(),
},
Type = host.PlatformType.SystemString,
Target = new TargetExpression() {
diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs index 18d735af..231a21cf 100644 --- a/BCT/BytecodeTranslator/Program.cs +++ b/BCT/BytecodeTranslator/Program.cs @@ -31,6 +31,9 @@ namespace BytecodeTranslator { [OptionDescription("Break into debugger", ShortForm = "break")]
public bool breakIntoDebugger = false;
+ [OptionDescription("Emit a 'capture state' directive after each statement, (default: false)", ShortForm = "c")]
+ public bool captureState = false;
+
[OptionDescription("Search paths for assembly dependencies.", ShortForm = "lib")]
public List<string> libpaths = new List<string>();
@@ -165,16 +168,16 @@ namespace BytecodeTranslator { return result;
}
- public static int TranslateAssembly(List<string> assemblyNames, HeapFactory heapFactory, Options/*?*/ options, List<Regex> exemptionList, bool whiteList) {
+ public static int TranslateAssembly(List<string> assemblyNames, HeapFactory heapFactory, Options options, List<Regex> exemptionList, bool whiteList) {
Contract.Requires(assemblyNames != null);
Contract.Requires(heapFactory != null);
- var libPaths = options == null ? null : options.libpaths;
- var wholeProgram = options == null ? false : options.wholeProgram;
- var/*?*/ stubAssemblies = options == null ? null : options.stub;
- var phoneControlsConfigFile = options == null ? null : options.phoneControls;
- var doPhoneNav = options == null ? false : options.phoneNavigationCode;
- var doPhoneFeedback = options == null ? false : options.phoneFeedbackCode;
+ var libPaths = options.libpaths;
+ var wholeProgram = options.wholeProgram;
+ var/*?*/ stubAssemblies = options.stub;
+ var phoneControlsConfigFile = options.phoneControls;
+ var doPhoneNav = options.phoneNavigationCode;
+ var doPhoneFeedback = options.phoneFeedbackCode;
var host = new CodeContractAwareHostEnvironment(libPaths != null ? libPaths : Enumerable<string>.Empty, true, true);
Host = host;
@@ -247,7 +250,7 @@ namespace BytecodeTranslator { else
traverserFactory = new CLRSemantics();
- Sink sink= new Sink(host, traverserFactory, heapFactory, exemptionList, whiteList);
+ Sink sink= new Sink(host, traverserFactory, heapFactory, options, exemptionList, whiteList);
TranslationHelper.tmpVarCounter = 0;
MetadataTraverser translator;
translator= traverserFactory.MakeMetadataTraverser(sink, contractExtractors, pdbReaders);
@@ -324,6 +327,13 @@ namespace BytecodeTranslator { System.Console.WriteLine("Total methods seen: {0}, inlined: {1}", inlineTraverser.TotalMethodsCount, inlineTraverser.InlinedMethodsCount);
}
+ if (PhoneCodeHelper.instance().PhoneNavigationToggled) {
+ // TODO integrate into the pipeline and spit out the boogie code
+ foreach (IMethodDefinition def in PhoneNavigationCodeTraverser.NavCallers) {
+ System.Console.WriteLine(def.ToString());
+ }
+ }
+
Microsoft.Boogie.TokenTextWriter writer = new Microsoft.Boogie.TokenTextWriter(primaryModule.Name + ".bpl");
Prelude.Emit(writer);
sink.TranslatedProgram.Emit(writer);
diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs index b2c1177e..1427b836 100644 --- a/BCT/BytecodeTranslator/Sink.cs +++ b/BCT/BytecodeTranslator/Sink.cs @@ -27,10 +27,11 @@ namespace BytecodeTranslator { get { return this.factory; }
}
readonly TraverserFactory factory;
+ private readonly Options options;
readonly bool whiteList;
readonly List<Regex> exemptionList;
- public Sink(IContractAwareHost host, TraverserFactory factory, HeapFactory heapFactory, List<Regex> exemptionList, bool whiteList) {
+ public Sink(IContractAwareHost host, TraverserFactory factory, HeapFactory heapFactory, Options options, List<Regex> exemptionList, bool whiteList) {
Contract.Requires(host != null);
Contract.Requires(factory != null);
Contract.Requires(heapFactory != null);
@@ -38,6 +39,7 @@ namespace BytecodeTranslator { this.host = host;
this.factory = factory;
var b = heapFactory.MakeHeap(this, out this.heap, out this.TranslatedProgram); // TODO: what if it returns false?
+ this.options = options;
this.exemptionList = exemptionList;
this.whiteList = whiteList;
if (this.TranslatedProgram == null) {
@@ -52,6 +54,8 @@ namespace BytecodeTranslator { }
}
+ public Options Options { get { return this.options; } }
+
public Heap Heap {
get { return this.heap; }
}
diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs index 4c927b3e..015e57ce 100644 --- a/BCT/BytecodeTranslator/StatementTraverser.cs +++ b/BCT/BytecodeTranslator/StatementTraverser.cs @@ -54,6 +54,8 @@ namespace BytecodeTranslator public readonly Bpl.StmtListBuilder StmtBuilder = new Bpl.StmtListBuilder();
private bool contractContext;
internal readonly Stack<IExpression> operandStack = new Stack<IExpression>();
+ private bool captureState;
+ private static int captureStateCounter = 0;
#region Constructors
public StatementTraverser(Sink sink, PdbReader/*?*/ pdbReader, bool contractContext) {
@@ -61,6 +63,7 @@ namespace BytecodeTranslator this.factory = sink.Factory;
PdbReader = pdbReader;
this.contractContext = contractContext;
+ this.captureState = sink.Options.captureState;
}
#endregion
@@ -108,6 +111,14 @@ namespace BytecodeTranslator public override void Visit(IStatement statement) {
EmitSourceContext(statement);
+ if (this.sink.Options.captureState) {
+ var tok = statement.Token();
+ var state = String.Format("s{0}", StatementTraverser.captureStateCounter++);
+ var attrib = new Bpl.QKeyValue(tok, "captureState ", new List<object> { state }, null);
+ StmtBuilder.Add(
+ new Bpl.AssumeCmd(tok, Bpl.Expr.True, attrib)
+ );
+ }
base.Visit(statement);
}
diff --git a/BCT/BytecodeTranslator/TranslationHelper.cs b/BCT/BytecodeTranslator/TranslationHelper.cs index a17165ee..924aba5e 100644 --- a/BCT/BytecodeTranslator/TranslationHelper.cs +++ b/BCT/BytecodeTranslator/TranslationHelper.cs @@ -42,6 +42,7 @@ namespace BytecodeTranslator { var parameterToken = parameterDefinition.Token();
var typeToken = parameterDefinition.Type.Token();
var parameterName = TranslationHelper.TurnStringIntoValidIdentifier(parameterDefinition.Name.Value);
+ if (String.IsNullOrWhiteSpace(parameterName)) parameterName = "P" + parameterDefinition.Index.ToString();
this.inParameterCopy = new Bpl.Formal(parameterToken, new Bpl.TypedIdent(typeToken, parameterName + "$in", ptype), true);
if (parameterDefinition.IsByReference) {
@@ -154,6 +155,7 @@ namespace BytecodeTranslator { s = s.Replace('[', '$');
s = s.Replace(']', '$');
s = s.Replace('|', '$');
+ s = s.Replace('+', '$');
s = GetRidOfSurrogateCharacters(s);
return s;
}
diff --git a/BCT/PhoneControlsExtractor/PhoneBoogieCodeGenerator.py b/BCT/PhoneControlsExtractor/PhoneBoogieCodeGenerator.py index 37b35746..2071ce21 100644 --- a/BCT/PhoneControlsExtractor/PhoneBoogieCodeGenerator.py +++ b/BCT/PhoneControlsExtractor/PhoneBoogieCodeGenerator.py @@ -5,7 +5,7 @@ from xml.dom import minidom from itertools import product
import xml.dom
-CONTROL_NAMES= ["Button", "CheckBox", "RadioButton"]
+CONTROL_NAMES= ["Button", "CheckBox", "RadioButton", "ApplicationBarIconButton", "Pivot"]
CONTAINER_CONTROL_NAMES= ["Canvas", "Grid", "StackPanel"]
# TODO externalize strings, share with C# code
@@ -20,6 +20,8 @@ originalPageVars= [] boogiePageVars= []
boogiePageClasses= []
dummyPageVar= "dummyBoogieStringPageName"
+anonymousControlCount= 0;
+ANONYMOUS_CONTROL_PREFIX= "__BOOGIE_ANONYMOUS_CONTROL_"
def showUsage():
print "PhoneBoogieCodeGenerator -- create boilerplate code for Boogie verification of Phone apps"
@@ -29,7 +31,14 @@ def showUsage(): print "\t--controls <app_control_info_file>: Phone app control info. See PhoneControlsExtractor. Short form: -c"
print "\t--output <code_output_file>: file to write with boilerplate code. Short form: -o\n"
-def loadControlInfo(infoMap, controlClass, controlName, enabled, visible, clickHandler, checkedHandler, uncheckedHandler, bplName):
+def isAnonymousControl(control):
+ name= control["bplName"]
+ return name.find(ANONYMOUS_CONTROL_PREFIX) != -1
+
+def loadControlInfo(infoMap, controlClass, controlName, enabled, visible, clickHandler, checkedHandler, uncheckedHandler, selectionChangedHandler, bplName):
+ global anonymousControlCount
+ global ANONYMOUS_CONTROL_PREFIX
+
newControl={}
newControl["class"]= controlClass
newControl["enabled"]= enabled
@@ -37,6 +46,11 @@ def loadControlInfo(infoMap, controlClass, controlName, enabled, visible, clickH newControl["clickHandler"]= clickHandler
newControl["checkedHandler"]= checkedHandler
newControl["uncheckedHandler"]= uncheckedHandler
+ newControl["selectionChangedHandler"]= selectionChangedHandler
+ if (bplName == ""):
+ # anonymous control, need a dummy boogie var, but we cannot know how it got initialized
+ bplName= ANONYMOUS_CONTROL_PREFIX + str(anonymousControlCount)
+ anonymousControlCount= anonymousControlCount+1
newControl["bplName"]=bplName
infoMap[controlName]= newControl
@@ -115,7 +129,7 @@ def outputPageControlDriver(file, originalPageName, boogiePageName): for entry in staticControlsMap[originalPageName]["controls"].keys():
controlInfo= staticControlsMap[originalPageName]["controls"][entry]
if controlInfo["bplName"] == "":
- continue
+ continue;
if not ifInitialized:
file.write("\t\tif ($activeControl == " + str(activeControl) + ") {\n")
ifInitialized= True
@@ -139,6 +153,10 @@ def outputPageControlDriver(file, originalPageName, boogiePageName): file.write("\t\t\t\tif ($handlerToActivate == 2) {\n")
file.write("\t\t\t\t\tcall " + staticControlsMap[originalPageName]["class"] + "." + controlInfo["uncheckedHandler"] + "$System.Object$System.Windows.RoutedEventArgs(" + controlInfo["bplName"] + "[" + boogiePageName + "],null,null);\n")
file.write("\t\t\t\t}\n")
+ if not controlInfo["selectionChangedHandler"] == "":
+ file.write("\t\t\t\tif ($handlerToActivate == 3) {\n")
+ file.write("\t\t\t\t\tcall " + staticControlsMap[originalPageName]["class"] + "." + controlInfo["selectionChangedHandler"] + "$System.Object$System.Windows.RoutedEventArgs(" + controlInfo["bplName"] + "[" + boogiePageName + "],null,null);\n")
+ file.write("\t\t\t\t}\n")
file.write("\t\t\t}\n")
file.write("\t\t}\n")
@@ -203,14 +221,14 @@ def buildControlInfo(controlInfoFileName): file = open(controlInfoFileName, "r")
# 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>
+ # <pageClassName>,<page.xaml file>,<xaml boogie string representation>,<controlClassName>,<controlName (as in field name)>,<IsEnabledValue>,<VisibilityValue>,<ClickValue>,<CheckedValue>,<UncheckedValue>,<SelectionChangedValue>,<BoogieName>
mainPageXAML= file.readline().strip()
currentNavigationVariable= file.readline().strip()
mainAppClassname= file.readline().strip()
infoLine= file.readline().strip()
while not infoLine == "":
- pageClass, pageName, pageBoogieStringName, controlClass, controlName, enabled, visible, clickHandler, checkedHandler, uncheckedHandler, bplName= infoLine.split(",")
+ pageClass, pageName, pageBoogieStringName, controlClass, controlName, enabled, visible, clickHandler, checkedHandler, uncheckedHandler, selectionChangedHandler, bplName= infoLine.split(",")
pageInfo={}
pageInfo["class"]=pageClass
try:
@@ -224,7 +242,7 @@ def buildControlInfo(controlInfoFileName): pageControlInfo= pageInfo["controls"]
except KeyError:
pageInfo["controls"]=pageControlInfo
- loadControlInfo(pageControlInfo, controlClass, controlName, enabled, visible, clickHandler, checkedHandler, uncheckedHandler, bplName)
+ loadControlInfo(pageControlInfo, controlClass, controlName, enabled, visible, clickHandler, checkedHandler, uncheckedHandler, selectionChangedHandler, bplName)
pageInfo["controls"]= pageControlInfo
staticControlsMap[pageName]=pageInfo
diff --git a/BCT/PhoneControlsExtractor/PhoneControlsExtractor.py b/BCT/PhoneControlsExtractor/PhoneControlsExtractor.py index 9285d6c8..82090e29 100644 --- a/BCT/PhoneControlsExtractor/PhoneControlsExtractor.py +++ b/BCT/PhoneControlsExtractor/PhoneControlsExtractor.py @@ -4,7 +4,7 @@ import os from xml.dom import minidom
import xml.dom
-CONTROL_NAMES= ["Button", "CheckBox", "RadioButton", "ApplicationBarIconButton"]
+CONTROL_NAMES= ["Button", "CheckBox", "RadioButton", "ApplicationBarIconButton", "Pivot"]
# TODO maybe a control is enabled but its parent is not, must take this into account
# TODO a possible solution is to tie the enabled value to that of the parent in the app until it is either overriden
@@ -70,6 +70,7 @@ def addDummyControlToMap(pageXAML, parentPage): newControl["Click"] = ""
newControl["Checked"] = ""
newControl["Unchecked"] = ""
+ newControl["SelectionChanged"]= ""
newControl["XAML"]= pageXAML
pageControls.append(newControl)
staticControlsMap[parentPage]= pageControls
@@ -98,6 +99,7 @@ def addControlToMap(pageXAML, parentPage, controlNode): newControl["Click"] = controlNode.getAttribute("Click").replace(",",COMMA_REPLACEMENT).replace("=",COMMA_REPLACEMENT)
newControl["Checked"] = controlNode.getAttribute("Checked").replace(",",COMMA_REPLACEMENT).replace("=",COMMA_REPLACEMENT)
newControl["Unchecked"] = controlNode.getAttribute("Unchecked").replace(",",COMMA_REPLACEMENT).replace("=",COMMA_REPLACEMENT)
+ newControl["SelectionChanged"] = controlNode.getAttribute("SelectionChanged").replace(",",COMMA_REPLACEMENT).replace("=",COMMA_REPLACEMENT)
newControl["XAML"]= pageXAML
pageControls.append(newControl)
staticControlsMap[parentPage]= pageControls
@@ -145,7 +147,7 @@ def outputPhoneControls(outputFileName): outputFile= open(outputFileName, "w")
# 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>
+ # <pageClassName>,<page.xaml file>,<boogie string page name>,<controlClassName>,<controlName (as in field name)>,<IsEnabledValue>,<VisibilityValue>,<ClickValue>,<CheckedValue>,<UncheckedValue>,<SelChangedValue>
outputFile.write(mainPageXAML + "\n")
outputFile.write("dummyNavigationVariable_unknown\n")
outputFile.write("dummyMainAppName_unknown\n") # I could possibly deduce it from WMAppManifest.xml, but I'm unsure. Doing it later is safe anyway
@@ -167,10 +169,14 @@ def outputPhoneControls(outputFileName): unchecked= control["Unchecked"]
if (unchecked.find(COMMA_REPLACEMENT) != -1):
unchecked= ""
+ selectionChanged= control["SelectionChanged"]
+ if (selectionChanged.find(COMMA_REPLACEMENT) != -1):
+ selectionChanged= ""
pageXAML= control["XAML"]
# last comma is to account for bpl translation name, that is unknown for now
# 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.write(page + "," + os.path.basename(pageXAML) + ",dummyBoogieStringPageName," + control["Type"] + "," + control["Name"] + \
+ "," + isEnabled + "," + visibility + "," + click + "," + checked + "," + unchecked + "," + selectionChanged + ",\n")
outputFile.close()
diff --git a/BCT/RegressionTests/RegressionTestInput/Class1.cs b/BCT/RegressionTests/RegressionTestInput/Class1.cs index ac2a0b2d..6dfccde6 100644 --- a/BCT/RegressionTests/RegressionTestInput/Class1.cs +++ b/BCT/RegressionTests/RegressionTestInput/Class1.cs @@ -190,5 +190,12 @@ namespace RegressionTestInput { }
}
}
+ public class TestForClassesDifferingOnlyInBeingGeneric {
+ public int x;
+ }
+
+ public class TestForClassesDifferingOnlyInBeingGeneric<T> {
+ public int x;
+ }
}
diff --git a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt index a0f72ae1..59d9be9b 100644 --- a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt @@ -492,7 +492,7 @@ procedure RegressionTestInput.RealNumbers.WriteDouble$System.Double3($this: Ref, -procedure {:extern} System.Console.WriteLine$System.Double43(value$in: Real);
+procedure {:extern} System.Console.WriteLine$System.Double45(value$in: Real);
@@ -504,7 +504,7 @@ implementation RegressionTestInput.RealNumbers.WriteDouble$System.Double3($this: d := d$in;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 162} true;
- call System.Console.WriteLine$System.Double43(d);
+ call System.Console.WriteLine$System.Double45(d);
if ($Exception != null)
{
return;
@@ -597,7 +597,7 @@ procedure RegressionTestInput.RealNumbers.#ctor6($this: Ref); -procedure {:extern} System.Object.#ctor44($this: Ref);
+procedure {:extern} System.Object.#ctor46($this: Ref);
@@ -606,7 +606,7 @@ implementation RegressionTestInput.RealNumbers.#ctor6($this: Ref) var $localExc: Ref;
var $label: int;
- call System.Object.#ctor44($this);
+ call System.Object.#ctor46($this);
if ($Exception != null)
{
return;
@@ -617,11 +617,11 @@ implementation RegressionTestInput.RealNumbers.#ctor6($this: Ref) -procedure RegressionTestInput.RealNumbers.#cctor();
+procedure T$RegressionTestInput.RealNumbers.#cctor();
-implementation RegressionTestInput.RealNumbers.#cctor()
+implementation T$RegressionTestInput.RealNumbers.#cctor()
{
}
@@ -633,9 +633,9 @@ axiom $Subtype(RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap$type, Sys axiom $DisjointSubtree(RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap$type, System.Object$type);
-const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x$field: Field;
+const unique F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x: Field;
-const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y$field: Field;
+const unique F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y: Field;
procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M7($this: Ref);
@@ -647,7 +647,7 @@ implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M7($this: var $label: int;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 130} true;
- $Heap := Write($Heap, $this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y$field, Int2Box(Box2Int(Read($Heap, $this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x$field))));
+ $Heap := Write($Heap, $this, F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y, Int2Box(Box2Int(Read($Heap, $this, F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x))));
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 131} true;
return;
}
@@ -663,9 +663,9 @@ implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor8($t var $localExc: Ref;
var $label: int;
- $Heap := Write($Heap, $this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x$field, Int2Box(0));
- $Heap := Write($Heap, $this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y$field, Int2Box(0));
- call System.Object.#ctor44($this);
+ $Heap := Write($Heap, $this, F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x, Int2Box(0));
+ $Heap := Write($Heap, $this, F$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y, Int2Box(0));
+ call System.Object.#ctor46($this);
if ($Exception != null)
{
return;
@@ -676,11 +676,11 @@ implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor8($t -procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor();
+procedure T$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor();
-implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor()
+implementation T$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor()
{
}
@@ -712,9 +712,9 @@ axiom $Subtype(RegressionTestInput.S$type, System.ValueType$type); axiom $DisjointSubtree(RegressionTestInput.S$type, System.ValueType$type);
-const unique RegressionTestInput.S.x$field: Field;
+const unique F$RegressionTestInput.S.x: Field;
-const unique RegressionTestInput.S.b$field: Field;
+const unique F$RegressionTestInput.S.b: Field;
implementation RegressionTestInput.CreateStruct.Create9($this: Ref) returns ($result: Ref)
{
@@ -729,9 +729,9 @@ implementation RegressionTestInput.CreateStruct.Create9($this: Ref) returns ($re assume $DynamicType($tmp0) == RegressionTestInput.S$type;
s := $tmp0;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 142} true;
- assert Box2Int(Read($Heap, s, RegressionTestInput.S.x$field)) == 0;
+ assert Box2Int(Read($Heap, s, F$RegressionTestInput.S.x)) == 0;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 143} true;
- assert !Box2Bool(Read($Heap, s, RegressionTestInput.S.b$field));
+ assert !Box2Bool(Read($Heap, s, F$RegressionTestInput.S.b));
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 145} true;
$result := s;
return;
@@ -751,9 +751,9 @@ implementation RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTes s := s$in;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 147} true;
- $Heap := Write($Heap, s, RegressionTestInput.S.x$field, Int2Box(3));
+ $Heap := Write($Heap, s, F$RegressionTestInput.S.x, Int2Box(3));
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 148} true;
- assert Box2Int(Read($Heap, s, RegressionTestInput.S.x$field)) == 3;
+ assert Box2Int(Read($Heap, s, F$RegressionTestInput.S.x)) == 3;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 150} true;
$result := s;
return;
@@ -770,7 +770,7 @@ implementation RegressionTestInput.CreateStruct.#ctor11($this: Ref) var $localExc: Ref;
var $label: int;
- call System.Object.#ctor44($this);
+ call System.Object.#ctor46($this);
if ($Exception != null)
{
return;
@@ -781,11 +781,11 @@ implementation RegressionTestInput.CreateStruct.#ctor11($this: Ref) -procedure RegressionTestInput.CreateStruct.#cctor();
+procedure T$RegressionTestInput.CreateStruct.#cctor();
-implementation RegressionTestInput.CreateStruct.#cctor()
+implementation T$RegressionTestInput.CreateStruct.#cctor()
{
}
@@ -797,9 +797,9 @@ axiom $Subtype(RegressionTestInput.ClassWithArrayTypes$type, System.Object$type) axiom $DisjointSubtree(RegressionTestInput.ClassWithArrayTypes$type, System.Object$type);
-var RegressionTestInput.ClassWithArrayTypes.s$field: Ref;
+var F$RegressionTestInput.ClassWithArrayTypes.s: Ref;
-const unique RegressionTestInput.ClassWithArrayTypes.a$field: Field;
+const unique F$RegressionTestInput.ClassWithArrayTypes.a: Field;
procedure RegressionTestInput.ClassWithArrayTypes.Main112();
@@ -853,11 +853,11 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main213() assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 100} true;
call $tmp3 := Alloc();
assume $ArrayLength($tmp3) == 1 * 5;
- RegressionTestInput.ClassWithArrayTypes.s$field := $tmp3;
+ F$RegressionTestInput.ClassWithArrayTypes.s := $tmp3;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 101} true;
- $ArrayContents := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s$field := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s$field][0 := Int2Box(2)]];
+ $ArrayContents := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s := $ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s][0 := Int2Box(2)]];
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 102} true;
- assert Box2Int($ArrayContents[RegressionTestInput.ClassWithArrayTypes.s$field][0]) == 2;
+ assert Box2Int($ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s][0]) == 2;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 104} true;
call $tmp4 := Alloc();
assume $ArrayLength($tmp4) == 1 * 4;
@@ -867,7 +867,7 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main213() assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 106} true;
assert Box2Int($ArrayContents[t][0]) == 1;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 108} true;
- assert Box2Int($ArrayContents[RegressionTestInput.ClassWithArrayTypes.s$field][0]) == 2;
+ assert Box2Int($ArrayContents[F$RegressionTestInput.ClassWithArrayTypes.s][0]) == 2;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 109} true;
return;
}
@@ -888,12 +888,12 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int3214($thi x := x$in;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 114} true;
- $ArrayContents := $ArrayContents[Box2Ref(Read($Heap, $this, RegressionTestInput.ClassWithArrayTypes.a$field)) := $ArrayContents[Box2Ref(Read($Heap, $this, RegressionTestInput.ClassWithArrayTypes.a$field))][x := Int2Box(42)]];
+ $ArrayContents := $ArrayContents[Box2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a)) := $ArrayContents[Box2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a))][x := Int2Box(42)]];
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 115} true;
- $ArrayContents := $ArrayContents[Box2Ref(Read($Heap, $this, RegressionTestInput.ClassWithArrayTypes.a$field)) := $ArrayContents[Box2Ref(Read($Heap, $this, RegressionTestInput.ClassWithArrayTypes.a$field))][x + 1 := Int2Box(43)]];
+ $ArrayContents := $ArrayContents[Box2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a)) := $ArrayContents[Box2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a))][x + 1 := Int2Box(43)]];
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 116} true;
- _loc0 := Box2Ref(Read($Heap, $this, RegressionTestInput.ClassWithArrayTypes.a$field));
- _loc1 := Box2Ref(Read($Heap, $this, RegressionTestInput.ClassWithArrayTypes.a$field));
+ _loc0 := Box2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a));
+ _loc1 := Box2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a));
assert Box2Int($ArrayContents[_loc0][x + 1]) == Box2Int($ArrayContents[_loc1][x]) + 1;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 117} true;
return;
@@ -922,7 +922,7 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array15 if (!(if xs != null then $ArrayLength(xs) <= 0 else true))
{
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 121} true;
- $ArrayContents := $ArrayContents[Box2Ref(Read($Heap, $this, RegressionTestInput.ClassWithArrayTypes.a$field)) := $ArrayContents[Box2Ref(Read($Heap, $this, RegressionTestInput.ClassWithArrayTypes.a$field))][0 := Int2Box(Box2Int($ArrayContents[xs][0]))]];
+ $ArrayContents := $ArrayContents[Box2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a)) := $ArrayContents[Box2Ref(Read($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a))][0 := Int2Box(Box2Int($ArrayContents[xs][0]))]];
}
else
{
@@ -943,8 +943,8 @@ implementation RegressionTestInput.ClassWithArrayTypes.#ctor16($this: Ref) var $localExc: Ref;
var $label: int;
- $Heap := Write($Heap, $this, RegressionTestInput.ClassWithArrayTypes.a$field, Ref2Box(null));
- call System.Object.#ctor44($this);
+ $Heap := Write($Heap, $this, F$RegressionTestInput.ClassWithArrayTypes.a, Ref2Box(null));
+ call System.Object.#ctor46($this);
if ($Exception != null)
{
return;
@@ -955,13 +955,52 @@ implementation RegressionTestInput.ClassWithArrayTypes.#ctor16($this: Ref) -procedure RegressionTestInput.ClassWithArrayTypes.#cctor();
+procedure T$RegressionTestInput.ClassWithArrayTypes.#cctor();
-implementation RegressionTestInput.ClassWithArrayTypes.#cctor()
+implementation T$RegressionTestInput.ClassWithArrayTypes.#cctor()
+{
+ F$RegressionTestInput.ClassWithArrayTypes.s := null;
+}
+
+
+
+function RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric$type(arg0: Type) : Type;
+
+function Child0(in: Type) : Type;
+
+axiom (forall arg0: Type :: { RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric$type(arg0) } Child0(RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric$type(arg0)) == arg0);
+
+const unique F$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1.x: Field;
+
+procedure RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1.#ctor17($this: Ref);
+
+
+
+implementation RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1.#ctor17($this: Ref)
+{
+ var $localExc: Ref;
+ var $label: int;
+
+ $Heap := Write($Heap, $this, F$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1.x, Int2Box(0));
+ call System.Object.#ctor46($this);
+ if ($Exception != null)
+ {
+ return;
+ }
+
+ return;
+}
+
+
+
+procedure T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1.#cctor();
+
+
+
+implementation T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1.#cctor()
{
- RegressionTestInput.ClassWithArrayTypes.s$field := null;
}
@@ -972,11 +1011,11 @@ axiom $Subtype(RegressionTestInput.BitwiseOperations$type, System.Object$type); axiom $DisjointSubtree(RegressionTestInput.BitwiseOperations$type, System.Object$type);
-procedure RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$System.Int3217($this: Ref, x$in: int, y$in: int) returns ($result: int);
+procedure RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$System.Int3218($this: Ref, x$in: int, y$in: int) returns ($result: int);
-implementation RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$System.Int3217($this: Ref, x$in: int, y$in: int) returns ($result: int)
+implementation RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$System.Int3218($this: Ref, x$in: int, y$in: int) returns ($result: int)
{
var x: int;
var y: int;
@@ -992,11 +1031,11 @@ implementation RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$Sys -procedure RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$System.Int3218($this: Ref, x$in: int, y$in: int) returns ($result: int);
+procedure RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$System.Int3219($this: Ref, x$in: int, y$in: int) returns ($result: int);
-implementation RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$System.Int3218($this: Ref, x$in: int, y$in: int) returns ($result: int)
+implementation RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$System.Int3219($this: Ref, x$in: int, y$in: int) returns ($result: int)
{
var x: int;
var y: int;
@@ -1012,11 +1051,11 @@ implementation RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$Syst -procedure RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$System.Int3219($this: Ref, x$in: int, y$in: int) returns ($result: int);
+procedure RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$System.Int3220($this: Ref, x$in: int, y$in: int) returns ($result: int);
-implementation RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$System.Int3219($this: Ref, x$in: int, y$in: int) returns ($result: int)
+implementation RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$System.Int3220($this: Ref, x$in: int, y$in: int) returns ($result: int)
{
var x: int;
var y: int;
@@ -1032,11 +1071,11 @@ implementation RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$Sy -procedure RegressionTestInput.BitwiseOperations.BitwiseNegation$System.Int3220($this: Ref, x$in: int) returns ($result: int);
+procedure RegressionTestInput.BitwiseOperations.BitwiseNegation$System.Int3221($this: Ref, x$in: int) returns ($result: int);
-implementation RegressionTestInput.BitwiseOperations.BitwiseNegation$System.Int3220($this: Ref, x$in: int) returns ($result: int)
+implementation RegressionTestInput.BitwiseOperations.BitwiseNegation$System.Int3221($this: Ref, x$in: int) returns ($result: int)
{
var x: int;
var $localExc: Ref;
@@ -1050,16 +1089,16 @@ implementation RegressionTestInput.BitwiseOperations.BitwiseNegation$System.Int3 -procedure RegressionTestInput.BitwiseOperations.#ctor21($this: Ref);
+procedure RegressionTestInput.BitwiseOperations.#ctor22($this: Ref);
-implementation RegressionTestInput.BitwiseOperations.#ctor21($this: Ref)
+implementation RegressionTestInput.BitwiseOperations.#ctor22($this: Ref)
{
var $localExc: Ref;
var $label: int;
- call System.Object.#ctor44($this);
+ call System.Object.#ctor46($this);
if ($Exception != null)
{
return;
@@ -1070,11 +1109,11 @@ implementation RegressionTestInput.BitwiseOperations.#ctor21($this: Ref) -procedure RegressionTestInput.BitwiseOperations.#cctor();
+procedure T$RegressionTestInput.BitwiseOperations.#cctor();
-implementation RegressionTestInput.BitwiseOperations.#cctor()
+implementation T$RegressionTestInput.BitwiseOperations.#cctor()
{
}
@@ -1096,20 +1135,20 @@ axiom $Subtype(RegressionTestInput.AsyncAttribute$type, System.Attribute$type); axiom $DisjointSubtree(RegressionTestInput.AsyncAttribute$type, System.Attribute$type);
-procedure RegressionTestInput.AsyncAttribute.#ctor22($this: Ref);
+procedure RegressionTestInput.AsyncAttribute.#ctor23($this: Ref);
-procedure {:extern} System.Attribute.#ctor45($this: Ref);
+procedure {:extern} System.Attribute.#ctor47($this: Ref);
-implementation RegressionTestInput.AsyncAttribute.#ctor22($this: Ref)
+implementation RegressionTestInput.AsyncAttribute.#ctor23($this: Ref)
{
var $localExc: Ref;
var $label: int;
- call System.Attribute.#ctor45($this);
+ call System.Attribute.#ctor47($this);
if ($Exception != null)
{
return;
@@ -1120,11 +1159,11 @@ implementation RegressionTestInput.AsyncAttribute.#ctor22($this: Ref) -procedure RegressionTestInput.AsyncAttribute.#cctor();
+procedure T$RegressionTestInput.AsyncAttribute.#cctor();
-implementation RegressionTestInput.AsyncAttribute.#cctor()
+implementation T$RegressionTestInput.AsyncAttribute.#cctor()
{
}
@@ -1136,11 +1175,11 @@ axiom $Subtype(RegressionTestInput.RefParameters$type, System.Object$type); axiom $DisjointSubtree(RegressionTestInput.RefParameters$type, System.Object$type);
-procedure RegressionTestInput.RefParameters.M$System.Int32$23(x$in: int) returns (x$out: int);
+procedure RegressionTestInput.RefParameters.M$System.Int32$24(x$in: int) returns (x$out: int);
-implementation RegressionTestInput.RefParameters.M$System.Int32$23(x$in: int) returns (x$out: int)
+implementation RegressionTestInput.RefParameters.M$System.Int32$24(x$in: int) returns (x$out: int)
{
var $localExc: Ref;
var $label: int;
@@ -1154,16 +1193,16 @@ implementation RegressionTestInput.RefParameters.M$System.Int32$23(x$in: int) re -procedure RegressionTestInput.RefParameters.#ctor24($this: Ref);
+procedure RegressionTestInput.RefParameters.#ctor25($this: Ref);
-implementation RegressionTestInput.RefParameters.#ctor24($this: Ref)
+implementation RegressionTestInput.RefParameters.#ctor25($this: Ref)
{
var $localExc: Ref;
var $label: int;
- call System.Object.#ctor44($this);
+ call System.Object.#ctor46($this);
if ($Exception != null)
{
return;
@@ -1174,11 +1213,11 @@ implementation RegressionTestInput.RefParameters.#ctor24($this: Ref) -procedure RegressionTestInput.RefParameters.#cctor();
+procedure T$RegressionTestInput.RefParameters.#cctor();
-implementation RegressionTestInput.RefParameters.#cctor()
+implementation T$RegressionTestInput.RefParameters.#cctor()
{
}
@@ -1190,16 +1229,16 @@ axiom $Subtype(RegressionTestInput.NestedGeneric$type, System.Object$type); axiom $DisjointSubtree(RegressionTestInput.NestedGeneric$type, System.Object$type);
-procedure RegressionTestInput.NestedGeneric.#ctor27($this: Ref);
+procedure RegressionTestInput.NestedGeneric.#ctor28($this: Ref);
-implementation RegressionTestInput.NestedGeneric.#ctor27($this: Ref)
+implementation RegressionTestInput.NestedGeneric.#ctor28($this: Ref)
{
var $localExc: Ref;
var $label: int;
- call System.Object.#ctor44($this);
+ call System.Object.#ctor46($this);
if ($Exception != null)
{
return;
@@ -1216,16 +1255,16 @@ axiom $Subtype(RegressionTestInput.NestedGeneric.C$type, System.Object$type); axiom $DisjointSubtree(RegressionTestInput.NestedGeneric.C$type, System.Object$type);
-procedure RegressionTestInput.NestedGeneric.C.#ctor26($this: Ref);
+procedure RegressionTestInput.NestedGeneric.C.#ctor27($this: Ref);
-implementation RegressionTestInput.NestedGeneric.C.#ctor26($this: Ref)
+implementation RegressionTestInput.NestedGeneric.C.#ctor27($this: Ref)
{
var $localExc: Ref;
var $label: int;
- call System.Object.#ctor44($this);
+ call System.Object.#ctor46($this);
if ($Exception != null)
{
return;
@@ -1238,11 +1277,9 @@ implementation RegressionTestInput.NestedGeneric.C.#ctor26($this: Ref) function RegressionTestInput.NestedGeneric.C.G$type(arg0: Type) : Type;
-function Child0(in: Type) : Type;
-
axiom (forall arg0: Type :: { RegressionTestInput.NestedGeneric.C.G$type(arg0) } Child0(RegressionTestInput.NestedGeneric.C.G$type(arg0)) == arg0);
-procedure RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int3225($this: Ref, x$in: int);
+procedure RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int3226($this: Ref, x$in: int);
@@ -1250,7 +1287,7 @@ procedure {:extern} System.Activator.CreateInstance``12(T: Type) returns ($resul -implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int3225($this: Ref, x$in: int)
+implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int3226($this: Ref, x$in: int)
{
var x: int;
var CS$0$0000: Box;
@@ -1265,7 +1302,7 @@ implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int3225($thi x := x$in;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 187} true;
- call System.Object.#ctor44($this);
+ call System.Object.#ctor46($this);
if ($Exception != null)
{
return;
@@ -1299,31 +1336,31 @@ implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int3225($thi -procedure RegressionTestInput.NestedGeneric.C.G.#cctor();
+procedure T$RegressionTestInput.NestedGeneric.C.G`1.#cctor();
-implementation RegressionTestInput.NestedGeneric.C.G.#cctor()
+implementation T$RegressionTestInput.NestedGeneric.C.G`1.#cctor()
{
}
-procedure RegressionTestInput.NestedGeneric.C.#cctor();
+procedure T$RegressionTestInput.NestedGeneric.C.#cctor();
-implementation RegressionTestInput.NestedGeneric.C.#cctor()
+implementation T$RegressionTestInput.NestedGeneric.C.#cctor()
{
}
-procedure RegressionTestInput.NestedGeneric.#cctor();
+procedure T$RegressionTestInput.NestedGeneric.#cctor();
-implementation RegressionTestInput.NestedGeneric.#cctor()
+implementation T$RegressionTestInput.NestedGeneric.#cctor()
{
}
@@ -1343,8 +1380,47 @@ procedure RegressionTestInput.S.#copy_ctor(this: Ref, other: Ref); implementation {:inline 1} RegressionTestInput.S.#copy_ctor(this: Ref, other: Ref)
{
- $Heap := Write($Heap, other, RegressionTestInput.S.x$field, Int2Box(Box2Int(Read($Heap, this, RegressionTestInput.S.x$field))));
- $Heap := Write($Heap, other, RegressionTestInput.S.b$field, Bool2Box(Box2Bool(Read($Heap, this, RegressionTestInput.S.b$field))));
+ $Heap := Write($Heap, other, F$RegressionTestInput.S.x, Int2Box(Box2Int(Read($Heap, this, F$RegressionTestInput.S.x))));
+ $Heap := Write($Heap, other, F$RegressionTestInput.S.b, Bool2Box(Box2Bool(Read($Heap, this, F$RegressionTestInput.S.b))));
+}
+
+
+
+const unique RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric$type: Type;
+
+axiom $Subtype(RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric$type, System.Object$type);
+
+axiom $DisjointSubtree(RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric$type, System.Object$type);
+
+const unique F$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.x: Field;
+
+procedure RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.#ctor29($this: Ref);
+
+
+
+implementation RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.#ctor29($this: Ref)
+{
+ var $localExc: Ref;
+ var $label: int;
+
+ $Heap := Write($Heap, $this, F$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.x, Int2Box(0));
+ call System.Object.#ctor46($this);
+ if ($Exception != null)
+ {
+ return;
+ }
+
+ return;
+}
+
+
+
+procedure T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.#cctor();
+
+
+
+implementation T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.#cctor()
+{
}
@@ -1355,13 +1431,13 @@ axiom $Subtype(RegressionTestInput.Class0$type, System.Object$type); axiom $DisjointSubtree(RegressionTestInput.Class0$type, System.Object$type);
-var RegressionTestInput.Class0.StaticInt$field: int;
+var F$RegressionTestInput.Class0.StaticInt: int;
-procedure RegressionTestInput.Class0.StaticMethod$System.Int3228(x$in: int) returns ($result: int);
+procedure RegressionTestInput.Class0.StaticMethod$System.Int3230(x$in: int) returns ($result: int);
-implementation RegressionTestInput.Class0.StaticMethod$System.Int3228(x$in: int) returns ($result: int)
+implementation RegressionTestInput.Class0.StaticMethod$System.Int3230(x$in: int) returns ($result: int)
{
var x: int;
var $localExc: Ref;
@@ -1375,11 +1451,11 @@ implementation RegressionTestInput.Class0.StaticMethod$System.Int3228(x$in: int) -procedure RegressionTestInput.Class0.M$System.Int3229($this: Ref, x$in: int);
+procedure RegressionTestInput.Class0.M$System.Int3231($this: Ref, x$in: int);
-implementation RegressionTestInput.Class0.M$System.Int3229($this: Ref, x$in: int)
+implementation RegressionTestInput.Class0.M$System.Int3231($this: Ref, x$in: int)
{
var x: int;
var __temp_1: int;
@@ -1401,20 +1477,20 @@ implementation RegressionTestInput.Class0.M$System.Int3229($this: Ref, x$in: int assert (if x == 3 then y <= 8 else false);
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 23} true;
- RegressionTestInput.Class0.StaticInt$field := y;
+ F$RegressionTestInput.Class0.StaticInt := y;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 24} true;
- assert y == RegressionTestInput.Class0.StaticInt$field;
+ assert y == F$RegressionTestInput.Class0.StaticInt;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 25} true;
return;
}
-procedure RegressionTestInput.Class0.M$System.Int32$System.Int3230($this: Ref, x$in: int, y$in: int);
+procedure RegressionTestInput.Class0.M$System.Int32$System.Int3232($this: Ref, x$in: int, y$in: int);
-implementation RegressionTestInput.Class0.M$System.Int32$System.Int3230($this: Ref, x$in: int, y$in: int)
+implementation RegressionTestInput.Class0.M$System.Int32$System.Int3232($this: Ref, x$in: int, y$in: int)
{
var x: int;
var y: int;
@@ -1429,11 +1505,11 @@ implementation RegressionTestInput.Class0.M$System.Int32$System.Int3230($this: R -procedure RegressionTestInput.Class0.M$System.Boolean31($this: Ref, b$in: bool);
+procedure RegressionTestInput.Class0.M$System.Boolean33($this: Ref, b$in: bool);
-implementation RegressionTestInput.Class0.M$System.Boolean31($this: Ref, b$in: bool)
+implementation RegressionTestInput.Class0.M$System.Boolean33($this: Ref, b$in: bool)
{
var b: bool;
var $localExc: Ref;
@@ -1446,11 +1522,11 @@ implementation RegressionTestInput.Class0.M$System.Boolean31($this: Ref, b$in: b -procedure RegressionTestInput.Class0.M$RegressionTestInput.Class032($this: Ref, c$in: Ref);
+procedure RegressionTestInput.Class0.M$RegressionTestInput.Class034($this: Ref, c$in: Ref);
-implementation RegressionTestInput.Class0.M$RegressionTestInput.Class032($this: Ref, c$in: Ref)
+implementation RegressionTestInput.Class0.M$RegressionTestInput.Class034($this: Ref, c$in: Ref)
{
var c: Ref;
var $localExc: Ref;
@@ -1463,41 +1539,41 @@ implementation RegressionTestInput.Class0.M$RegressionTestInput.Class032($this: -procedure RegressionTestInput.Class0.NonVoid33($this: Ref) returns ($result: int);
+procedure RegressionTestInput.Class0.NonVoid35($this: Ref) returns ($result: int);
-implementation RegressionTestInput.Class0.NonVoid33($this: Ref) returns ($result: int)
+implementation RegressionTestInput.Class0.NonVoid35($this: Ref) returns ($result: int)
{
var $tmp8: int;
var $localExc: Ref;
var $label: int;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 34} true;
- call $tmp8 := RegressionTestInput.Class0.StaticMethod$System.Int3228(3);
+ call $tmp8 := RegressionTestInput.Class0.StaticMethod$System.Int3230(3);
if ($Exception != null)
{
return;
}
- $result := 3 + RegressionTestInput.Class0.StaticInt$field + $tmp8;
+ $result := 3 + F$RegressionTestInput.Class0.StaticInt + $tmp8;
return;
}
-procedure RegressionTestInput.Class0.OutParam$System.Int32$34($this: Ref, x$in: int) returns (x$out: int, $result: int);
+procedure RegressionTestInput.Class0.OutParam$System.Int32$36($this: Ref, x$in: int) returns (x$out: int, $result: int);
-implementation RegressionTestInput.Class0.OutParam$System.Int32$34($this: Ref, x$in: int) returns (x$out: int, $result: int)
+implementation RegressionTestInput.Class0.OutParam$System.Int32$36($this: Ref, x$in: int) returns (x$out: int, $result: int)
{
var $localExc: Ref;
var $label: int;
x$out := x$in;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 37} true;
- x$out := 3 + RegressionTestInput.Class0.StaticInt$field;
+ x$out := 3 + F$RegressionTestInput.Class0.StaticInt;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 39} true;
$result := x$out;
return;
@@ -1505,11 +1581,11 @@ implementation RegressionTestInput.Class0.OutParam$System.Int32$34($this: Ref, x -procedure RegressionTestInput.Class0.RefParam$System.Int32$35($this: Ref, x$in: int) returns (x$out: int, $result: int);
+procedure RegressionTestInput.Class0.RefParam$System.Int32$37($this: Ref, x$in: int) returns (x$out: int, $result: int);
-implementation RegressionTestInput.Class0.RefParam$System.Int32$35($this: Ref, x$in: int) returns (x$out: int, $result: int)
+implementation RegressionTestInput.Class0.RefParam$System.Int32$37($this: Ref, x$in: int) returns (x$out: int, $result: int)
{
var $localExc: Ref;
var $label: int;
@@ -1518,7 +1594,7 @@ implementation RegressionTestInput.Class0.RefParam$System.Int32$35($this: Ref, x assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 42} true;
x$out := x$out + 1;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 43} true;
- RegressionTestInput.Class0.StaticInt$field := x$out;
+ F$RegressionTestInput.Class0.StaticInt := x$out;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 45} true;
$result := x$out;
return;
@@ -1526,11 +1602,11 @@ implementation RegressionTestInput.Class0.RefParam$System.Int32$35($this: Ref, x -procedure RegressionTestInput.Class0.AssignToInParam$System.Int3236($this: Ref, x$in: int) returns ($result: int);
+procedure RegressionTestInput.Class0.AssignToInParam$System.Int3238($this: Ref, x$in: int) returns ($result: int);
-implementation RegressionTestInput.Class0.AssignToInParam$System.Int3236($this: Ref, x$in: int) returns ($result: int)
+implementation RegressionTestInput.Class0.AssignToInParam$System.Int3238($this: Ref, x$in: int) returns ($result: int)
{
var x: int;
var $localExc: Ref;
@@ -1540,7 +1616,7 @@ implementation RegressionTestInput.Class0.AssignToInParam$System.Int3236($this: assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 48} true;
x := x + 1;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 49} true;
- RegressionTestInput.Class0.StaticInt$field := x;
+ F$RegressionTestInput.Class0.StaticInt := x;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 51} true;
$result := x;
return;
@@ -1548,11 +1624,11 @@ implementation RegressionTestInput.Class0.AssignToInParam$System.Int3236($this: -procedure {:RegressionTestInput.Async} RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int3237($this: Ref, x$in: int) returns ($result: int);
+procedure {:RegressionTestInput.Async} RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int3239($this: Ref, x$in: int) returns ($result: int);
-implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int3237($this: Ref, x$in: int) returns ($result: int)
+implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int3239($this: Ref, x$in: int) returns ($result: int)
{
var x: int;
var $localExc: Ref;
@@ -1566,11 +1642,11 @@ implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMetho -procedure RegressionTestInput.Class0.CallAsyncMethod$System.Int3238($this: Ref, y$in: int) returns ($result: int);
+procedure RegressionTestInput.Class0.CallAsyncMethod$System.Int3240($this: Ref, y$in: int) returns ($result: int);
-implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int3238($this: Ref, y$in: int) returns ($result: int)
+implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int3240($this: Ref, y$in: int) returns ($result: int)
{
var y: int;
var $tmp9: int;
@@ -1579,7 +1655,7 @@ implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int3238($this: y := y$in;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 60} true;
- call {:async} $tmp9 := RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int3237($this, y);
+ call {:async} $tmp9 := RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int3239($this, y);
if ($Exception != null)
{
return;
@@ -1591,16 +1667,16 @@ implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int3238($this: -procedure RegressionTestInput.Class0.#ctor39($this: Ref);
+procedure RegressionTestInput.Class0.#ctor41($this: Ref);
-implementation RegressionTestInput.Class0.#ctor39($this: Ref)
+implementation RegressionTestInput.Class0.#ctor41($this: Ref)
{
var $localExc: Ref;
var $label: int;
- call System.Object.#ctor44($this);
+ call System.Object.#ctor46($this);
if ($Exception != null)
{
return;
@@ -1611,13 +1687,13 @@ implementation RegressionTestInput.Class0.#ctor39($this: Ref) -procedure RegressionTestInput.Class0.#cctor();
+procedure T$RegressionTestInput.Class0.#cctor();
-implementation RegressionTestInput.Class0.#cctor()
+implementation T$RegressionTestInput.Class0.#cctor()
{
- RegressionTestInput.Class0.StaticInt$field := 0;
+ F$RegressionTestInput.Class0.StaticInt := 0;
}
@@ -1628,15 +1704,15 @@ axiom $Subtype(RegressionTestInput.ClassWithBoolTypes$type, System.Object$type); axiom $DisjointSubtree(RegressionTestInput.ClassWithBoolTypes$type, System.Object$type);
-var RegressionTestInput.ClassWithBoolTypes.staticB$field: bool;
+var F$RegressionTestInput.ClassWithBoolTypes.staticB: bool;
-const unique RegressionTestInput.ClassWithBoolTypes.b$field: Field;
+const unique F$RegressionTestInput.ClassWithBoolTypes.b: Field;
-procedure RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3240(x$in: int, y$in: int) returns ($result: bool);
+procedure RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3242(x$in: int, y$in: int) returns ($result: bool);
-implementation RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3240(x$in: int, y$in: int) returns ($result: bool)
+implementation RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3242(x$in: int, y$in: int) returns ($result: bool)
{
var x: int;
var y: int;
@@ -1652,32 +1728,32 @@ implementation RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3 -procedure RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean41($this: Ref, z$in: bool);
+procedure RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean43($this: Ref, z$in: bool);
-implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean41($this: Ref, z$in: bool)
+implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean43($this: Ref, z$in: bool)
{
var z: bool;
var $localExc: Ref;
var $label: int;
z := z$in;
- $Heap := Write($Heap, $this, RegressionTestInput.ClassWithBoolTypes.b$field, Bool2Box(false));
+ $Heap := Write($Heap, $this, F$RegressionTestInput.ClassWithBoolTypes.b, Bool2Box(false));
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 72} true;
- call System.Object.#ctor44($this);
+ call System.Object.#ctor46($this);
if ($Exception != null)
{
return;
}
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 73} true;
- $Heap := Write($Heap, $this, RegressionTestInput.ClassWithBoolTypes.b$field, Bool2Box(z));
+ $Heap := Write($Heap, $this, F$RegressionTestInput.ClassWithBoolTypes.b, Bool2Box(z));
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 74} true;
if (z)
{
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 74} true;
- RegressionTestInput.ClassWithBoolTypes.staticB$field := z;
+ F$RegressionTestInput.ClassWithBoolTypes.staticB := z;
}
else
{
@@ -1688,18 +1764,18 @@ implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean41($th -procedure RegressionTestInput.ClassWithBoolTypes.Main42();
+procedure RegressionTestInput.ClassWithBoolTypes.Main44();
-implementation RegressionTestInput.ClassWithBoolTypes.Main42()
+implementation RegressionTestInput.ClassWithBoolTypes.Main44()
{
var $tmp10: bool;
var $localExc: Ref;
var $label: int;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 78} true;
- call $tmp10 := RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3240(3, 4);
+ call $tmp10 := RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3242(3, 4);
if ($Exception != null)
{
return;
@@ -1711,13 +1787,13 @@ implementation RegressionTestInput.ClassWithBoolTypes.Main42() -procedure RegressionTestInput.ClassWithBoolTypes.#cctor();
+procedure T$RegressionTestInput.ClassWithBoolTypes.#cctor();
-implementation RegressionTestInput.ClassWithBoolTypes.#cctor()
+implementation T$RegressionTestInput.ClassWithBoolTypes.#cctor()
{
- RegressionTestInput.ClassWithBoolTypes.staticB$field := false;
+ F$RegressionTestInput.ClassWithBoolTypes.staticB := false;
}
diff --git a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt index d2b5950a..d93b6815 100644 --- a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt @@ -478,7 +478,7 @@ procedure RegressionTestInput.RealNumbers.WriteDouble$System.Double3($this: Ref, -procedure {:extern} System.Console.WriteLine$System.Double43(value$in: Real);
+procedure {:extern} System.Console.WriteLine$System.Double45(value$in: Real);
@@ -490,7 +490,7 @@ implementation RegressionTestInput.RealNumbers.WriteDouble$System.Double3($this: d := d$in;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 162} true;
- call System.Console.WriteLine$System.Double43(d);
+ call System.Console.WriteLine$System.Double45(d);
if ($Exception != null)
{
return;
@@ -583,7 +583,7 @@ procedure RegressionTestInput.RealNumbers.#ctor6($this: Ref); -procedure {:extern} System.Object.#ctor44($this: Ref);
+procedure {:extern} System.Object.#ctor46($this: Ref);
@@ -592,7 +592,7 @@ implementation RegressionTestInput.RealNumbers.#ctor6($this: Ref) var $localExc: Ref;
var $label: int;
- call System.Object.#ctor44($this);
+ call System.Object.#ctor46($this);
if ($Exception != null)
{
return;
@@ -603,11 +603,11 @@ implementation RegressionTestInput.RealNumbers.#ctor6($this: Ref) -procedure RegressionTestInput.RealNumbers.#cctor();
+procedure T$RegressionTestInput.RealNumbers.#cctor();
-implementation RegressionTestInput.RealNumbers.#cctor()
+implementation T$RegressionTestInput.RealNumbers.#cctor()
{
}
@@ -651,7 +651,7 @@ implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor8($t RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x[$this] := 0;
RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y[$this] := 0;
- call System.Object.#ctor44($this);
+ call System.Object.#ctor46($this);
if ($Exception != null)
{
return;
@@ -662,11 +662,11 @@ implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor8($t -procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor();
+procedure T$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor();
-implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor()
+implementation T$RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor()
{
}
@@ -756,7 +756,7 @@ implementation RegressionTestInput.CreateStruct.#ctor11($this: Ref) var $localExc: Ref;
var $label: int;
- call System.Object.#ctor44($this);
+ call System.Object.#ctor46($this);
if ($Exception != null)
{
return;
@@ -767,11 +767,11 @@ implementation RegressionTestInput.CreateStruct.#ctor11($this: Ref) -procedure RegressionTestInput.CreateStruct.#cctor();
+procedure T$RegressionTestInput.CreateStruct.#cctor();
-implementation RegressionTestInput.CreateStruct.#cctor()
+implementation T$RegressionTestInput.CreateStruct.#cctor()
{
}
@@ -930,7 +930,7 @@ implementation RegressionTestInput.ClassWithArrayTypes.#ctor16($this: Ref) var $label: int;
RegressionTestInput.ClassWithArrayTypes.a[$this] := null;
- call System.Object.#ctor44($this);
+ call System.Object.#ctor46($this);
if ($Exception != null)
{
return;
@@ -941,28 +941,67 @@ implementation RegressionTestInput.ClassWithArrayTypes.#ctor16($this: Ref) -procedure RegressionTestInput.ClassWithArrayTypes.#cctor();
+procedure T$RegressionTestInput.ClassWithArrayTypes.#cctor();
-implementation RegressionTestInput.ClassWithArrayTypes.#cctor()
+implementation T$RegressionTestInput.ClassWithArrayTypes.#cctor()
{
RegressionTestInput.ClassWithArrayTypes.s := null;
}
+function RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric$type(arg0: Type) : Type;
+
+function Child0(in: Type) : Type;
+
+axiom (forall arg0: Type :: { RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric$type(arg0) } Child0(RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric$type(arg0)) == arg0);
+
+var RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.x: [Ref]int;
+
+procedure RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1.#ctor17($this: Ref);
+
+
+
+implementation RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1.#ctor17($this: Ref)
+{
+ var $localExc: Ref;
+ var $label: int;
+
+ RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.x[$this] := 0;
+ call System.Object.#ctor46($this);
+ if ($Exception != null)
+ {
+ return;
+ }
+
+ return;
+}
+
+
+
+procedure T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1.#cctor();
+
+
+
+implementation T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric`1.#cctor()
+{
+}
+
+
+
const unique RegressionTestInput.BitwiseOperations$type: Type;
axiom $Subtype(RegressionTestInput.BitwiseOperations$type, System.Object$type);
axiom $DisjointSubtree(RegressionTestInput.BitwiseOperations$type, System.Object$type);
-procedure RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$System.Int3217($this: Ref, x$in: int, y$in: int) returns ($result: int);
+procedure RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$System.Int3218($this: Ref, x$in: int, y$in: int) returns ($result: int);
-implementation RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$System.Int3217($this: Ref, x$in: int, y$in: int) returns ($result: int)
+implementation RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$System.Int3218($this: Ref, x$in: int, y$in: int) returns ($result: int)
{
var x: int;
var y: int;
@@ -978,11 +1017,11 @@ implementation RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$Sys -procedure RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$System.Int3218($this: Ref, x$in: int, y$in: int) returns ($result: int);
+procedure RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$System.Int3219($this: Ref, x$in: int, y$in: int) returns ($result: int);
-implementation RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$System.Int3218($this: Ref, x$in: int, y$in: int) returns ($result: int)
+implementation RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$System.Int3219($this: Ref, x$in: int, y$in: int) returns ($result: int)
{
var x: int;
var y: int;
@@ -998,11 +1037,11 @@ implementation RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$Syst -procedure RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$System.Int3219($this: Ref, x$in: int, y$in: int) returns ($result: int);
+procedure RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$System.Int3220($this: Ref, x$in: int, y$in: int) returns ($result: int);
-implementation RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$System.Int3219($this: Ref, x$in: int, y$in: int) returns ($result: int)
+implementation RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$System.Int3220($this: Ref, x$in: int, y$in: int) returns ($result: int)
{
var x: int;
var y: int;
@@ -1018,11 +1057,11 @@ implementation RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$Sy -procedure RegressionTestInput.BitwiseOperations.BitwiseNegation$System.Int3220($this: Ref, x$in: int) returns ($result: int);
+procedure RegressionTestInput.BitwiseOperations.BitwiseNegation$System.Int3221($this: Ref, x$in: int) returns ($result: int);
-implementation RegressionTestInput.BitwiseOperations.BitwiseNegation$System.Int3220($this: Ref, x$in: int) returns ($result: int)
+implementation RegressionTestInput.BitwiseOperations.BitwiseNegation$System.Int3221($this: Ref, x$in: int) returns ($result: int)
{
var x: int;
var $localExc: Ref;
@@ -1036,16 +1075,16 @@ implementation RegressionTestInput.BitwiseOperations.BitwiseNegation$System.Int3 -procedure RegressionTestInput.BitwiseOperations.#ctor21($this: Ref);
+procedure RegressionTestInput.BitwiseOperations.#ctor22($this: Ref);
-implementation RegressionTestInput.BitwiseOperations.#ctor21($this: Ref)
+implementation RegressionTestInput.BitwiseOperations.#ctor22($this: Ref)
{
var $localExc: Ref;
var $label: int;
- call System.Object.#ctor44($this);
+ call System.Object.#ctor46($this);
if ($Exception != null)
{
return;
@@ -1056,11 +1095,11 @@ implementation RegressionTestInput.BitwiseOperations.#ctor21($this: Ref) -procedure RegressionTestInput.BitwiseOperations.#cctor();
+procedure T$RegressionTestInput.BitwiseOperations.#cctor();
-implementation RegressionTestInput.BitwiseOperations.#cctor()
+implementation T$RegressionTestInput.BitwiseOperations.#cctor()
{
}
@@ -1082,20 +1121,20 @@ axiom $Subtype(RegressionTestInput.AsyncAttribute$type, System.Attribute$type); axiom $DisjointSubtree(RegressionTestInput.AsyncAttribute$type, System.Attribute$type);
-procedure RegressionTestInput.AsyncAttribute.#ctor22($this: Ref);
+procedure RegressionTestInput.AsyncAttribute.#ctor23($this: Ref);
-procedure {:extern} System.Attribute.#ctor45($this: Ref);
+procedure {:extern} System.Attribute.#ctor47($this: Ref);
-implementation RegressionTestInput.AsyncAttribute.#ctor22($this: Ref)
+implementation RegressionTestInput.AsyncAttribute.#ctor23($this: Ref)
{
var $localExc: Ref;
var $label: int;
- call System.Attribute.#ctor45($this);
+ call System.Attribute.#ctor47($this);
if ($Exception != null)
{
return;
@@ -1106,11 +1145,11 @@ implementation RegressionTestInput.AsyncAttribute.#ctor22($this: Ref) -procedure RegressionTestInput.AsyncAttribute.#cctor();
+procedure T$RegressionTestInput.AsyncAttribute.#cctor();
-implementation RegressionTestInput.AsyncAttribute.#cctor()
+implementation T$RegressionTestInput.AsyncAttribute.#cctor()
{
}
@@ -1122,11 +1161,11 @@ axiom $Subtype(RegressionTestInput.RefParameters$type, System.Object$type); axiom $DisjointSubtree(RegressionTestInput.RefParameters$type, System.Object$type);
-procedure RegressionTestInput.RefParameters.M$System.Int32$23(x$in: int) returns (x$out: int);
+procedure RegressionTestInput.RefParameters.M$System.Int32$24(x$in: int) returns (x$out: int);
-implementation RegressionTestInput.RefParameters.M$System.Int32$23(x$in: int) returns (x$out: int)
+implementation RegressionTestInput.RefParameters.M$System.Int32$24(x$in: int) returns (x$out: int)
{
var $localExc: Ref;
var $label: int;
@@ -1140,16 +1179,16 @@ implementation RegressionTestInput.RefParameters.M$System.Int32$23(x$in: int) re -procedure RegressionTestInput.RefParameters.#ctor24($this: Ref);
+procedure RegressionTestInput.RefParameters.#ctor25($this: Ref);
-implementation RegressionTestInput.RefParameters.#ctor24($this: Ref)
+implementation RegressionTestInput.RefParameters.#ctor25($this: Ref)
{
var $localExc: Ref;
var $label: int;
- call System.Object.#ctor44($this);
+ call System.Object.#ctor46($this);
if ($Exception != null)
{
return;
@@ -1160,11 +1199,11 @@ implementation RegressionTestInput.RefParameters.#ctor24($this: Ref) -procedure RegressionTestInput.RefParameters.#cctor();
+procedure T$RegressionTestInput.RefParameters.#cctor();
-implementation RegressionTestInput.RefParameters.#cctor()
+implementation T$RegressionTestInput.RefParameters.#cctor()
{
}
@@ -1176,16 +1215,16 @@ axiom $Subtype(RegressionTestInput.NestedGeneric$type, System.Object$type); axiom $DisjointSubtree(RegressionTestInput.NestedGeneric$type, System.Object$type);
-procedure RegressionTestInput.NestedGeneric.#ctor27($this: Ref);
+procedure RegressionTestInput.NestedGeneric.#ctor28($this: Ref);
-implementation RegressionTestInput.NestedGeneric.#ctor27($this: Ref)
+implementation RegressionTestInput.NestedGeneric.#ctor28($this: Ref)
{
var $localExc: Ref;
var $label: int;
- call System.Object.#ctor44($this);
+ call System.Object.#ctor46($this);
if ($Exception != null)
{
return;
@@ -1202,16 +1241,16 @@ axiom $Subtype(RegressionTestInput.NestedGeneric.C$type, System.Object$type); axiom $DisjointSubtree(RegressionTestInput.NestedGeneric.C$type, System.Object$type);
-procedure RegressionTestInput.NestedGeneric.C.#ctor26($this: Ref);
+procedure RegressionTestInput.NestedGeneric.C.#ctor27($this: Ref);
-implementation RegressionTestInput.NestedGeneric.C.#ctor26($this: Ref)
+implementation RegressionTestInput.NestedGeneric.C.#ctor27($this: Ref)
{
var $localExc: Ref;
var $label: int;
- call System.Object.#ctor44($this);
+ call System.Object.#ctor46($this);
if ($Exception != null)
{
return;
@@ -1224,11 +1263,9 @@ implementation RegressionTestInput.NestedGeneric.C.#ctor26($this: Ref) function RegressionTestInput.NestedGeneric.C.G$type(arg0: Type) : Type;
-function Child0(in: Type) : Type;
-
axiom (forall arg0: Type :: { RegressionTestInput.NestedGeneric.C.G$type(arg0) } Child0(RegressionTestInput.NestedGeneric.C.G$type(arg0)) == arg0);
-procedure RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int3225($this: Ref, x$in: int);
+procedure RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int3226($this: Ref, x$in: int);
@@ -1236,7 +1273,7 @@ procedure {:extern} System.Activator.CreateInstance``12(T: Type) returns ($resul -implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int3225($this: Ref, x$in: int)
+implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int3226($this: Ref, x$in: int)
{
var x: int;
var CS$0$0000: Box;
@@ -1251,7 +1288,7 @@ implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int3225($thi x := x$in;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 187} true;
- call System.Object.#ctor44($this);
+ call System.Object.#ctor46($this);
if ($Exception != null)
{
return;
@@ -1285,31 +1322,31 @@ implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int3225($thi -procedure RegressionTestInput.NestedGeneric.C.G.#cctor();
+procedure T$RegressionTestInput.NestedGeneric.C.G`1.#cctor();
-implementation RegressionTestInput.NestedGeneric.C.G.#cctor()
+implementation T$RegressionTestInput.NestedGeneric.C.G`1.#cctor()
{
}
-procedure RegressionTestInput.NestedGeneric.C.#cctor();
+procedure T$RegressionTestInput.NestedGeneric.C.#cctor();
-implementation RegressionTestInput.NestedGeneric.C.#cctor()
+implementation T$RegressionTestInput.NestedGeneric.C.#cctor()
{
}
-procedure RegressionTestInput.NestedGeneric.#cctor();
+procedure T$RegressionTestInput.NestedGeneric.#cctor();
-implementation RegressionTestInput.NestedGeneric.#cctor()
+implementation T$RegressionTestInput.NestedGeneric.#cctor()
{
}
@@ -1335,6 +1372,45 @@ implementation {:inline 1} RegressionTestInput.S.#copy_ctor(this: Ref, other: Re +const unique RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric$type: Type;
+
+axiom $Subtype(RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric$type, System.Object$type);
+
+axiom $DisjointSubtree(RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric$type, System.Object$type);
+
+var RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.x: [Ref]int;
+
+procedure RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.#ctor29($this: Ref);
+
+
+
+implementation RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.#ctor29($this: Ref)
+{
+ var $localExc: Ref;
+ var $label: int;
+
+ RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.x[$this] := 0;
+ call System.Object.#ctor46($this);
+ if ($Exception != null)
+ {
+ return;
+ }
+
+ return;
+}
+
+
+
+procedure T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.#cctor();
+
+
+
+implementation T$RegressionTestInput.TestForClassesDifferingOnlyInBeingGeneric.#cctor()
+{
+}
+
+
+
const unique RegressionTestInput.Class0$type: Type;
axiom $Subtype(RegressionTestInput.Class0$type, System.Object$type);
@@ -1343,11 +1419,11 @@ axiom $DisjointSubtree(RegressionTestInput.Class0$type, System.Object$type); var RegressionTestInput.Class0.StaticInt: int;
-procedure RegressionTestInput.Class0.StaticMethod$System.Int3228(x$in: int) returns ($result: int);
+procedure RegressionTestInput.Class0.StaticMethod$System.Int3230(x$in: int) returns ($result: int);
-implementation RegressionTestInput.Class0.StaticMethod$System.Int3228(x$in: int) returns ($result: int)
+implementation RegressionTestInput.Class0.StaticMethod$System.Int3230(x$in: int) returns ($result: int)
{
var x: int;
var $localExc: Ref;
@@ -1361,11 +1437,11 @@ implementation RegressionTestInput.Class0.StaticMethod$System.Int3228(x$in: int) -procedure RegressionTestInput.Class0.M$System.Int3229($this: Ref, x$in: int);
+procedure RegressionTestInput.Class0.M$System.Int3231($this: Ref, x$in: int);
-implementation RegressionTestInput.Class0.M$System.Int3229($this: Ref, x$in: int)
+implementation RegressionTestInput.Class0.M$System.Int3231($this: Ref, x$in: int)
{
var x: int;
var __temp_1: int;
@@ -1396,11 +1472,11 @@ implementation RegressionTestInput.Class0.M$System.Int3229($this: Ref, x$in: int -procedure RegressionTestInput.Class0.M$System.Int32$System.Int3230($this: Ref, x$in: int, y$in: int);
+procedure RegressionTestInput.Class0.M$System.Int32$System.Int3232($this: Ref, x$in: int, y$in: int);
-implementation RegressionTestInput.Class0.M$System.Int32$System.Int3230($this: Ref, x$in: int, y$in: int)
+implementation RegressionTestInput.Class0.M$System.Int32$System.Int3232($this: Ref, x$in: int, y$in: int)
{
var x: int;
var y: int;
@@ -1415,11 +1491,11 @@ implementation RegressionTestInput.Class0.M$System.Int32$System.Int3230($this: R -procedure RegressionTestInput.Class0.M$System.Boolean31($this: Ref, b$in: bool);
+procedure RegressionTestInput.Class0.M$System.Boolean33($this: Ref, b$in: bool);
-implementation RegressionTestInput.Class0.M$System.Boolean31($this: Ref, b$in: bool)
+implementation RegressionTestInput.Class0.M$System.Boolean33($this: Ref, b$in: bool)
{
var b: bool;
var $localExc: Ref;
@@ -1432,11 +1508,11 @@ implementation RegressionTestInput.Class0.M$System.Boolean31($this: Ref, b$in: b -procedure RegressionTestInput.Class0.M$RegressionTestInput.Class032($this: Ref, c$in: Ref);
+procedure RegressionTestInput.Class0.M$RegressionTestInput.Class034($this: Ref, c$in: Ref);
-implementation RegressionTestInput.Class0.M$RegressionTestInput.Class032($this: Ref, c$in: Ref)
+implementation RegressionTestInput.Class0.M$RegressionTestInput.Class034($this: Ref, c$in: Ref)
{
var c: Ref;
var $localExc: Ref;
@@ -1449,18 +1525,18 @@ implementation RegressionTestInput.Class0.M$RegressionTestInput.Class032($this: -procedure RegressionTestInput.Class0.NonVoid33($this: Ref) returns ($result: int);
+procedure RegressionTestInput.Class0.NonVoid35($this: Ref) returns ($result: int);
-implementation RegressionTestInput.Class0.NonVoid33($this: Ref) returns ($result: int)
+implementation RegressionTestInput.Class0.NonVoid35($this: Ref) returns ($result: int)
{
var $tmp8: int;
var $localExc: Ref;
var $label: int;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 34} true;
- call $tmp8 := RegressionTestInput.Class0.StaticMethod$System.Int3228(3);
+ call $tmp8 := RegressionTestInput.Class0.StaticMethod$System.Int3230(3);
if ($Exception != null)
{
return;
@@ -1472,11 +1548,11 @@ implementation RegressionTestInput.Class0.NonVoid33($this: Ref) returns ($result -procedure RegressionTestInput.Class0.OutParam$System.Int32$34($this: Ref, x$in: int) returns (x$out: int, $result: int);
+procedure RegressionTestInput.Class0.OutParam$System.Int32$36($this: Ref, x$in: int) returns (x$out: int, $result: int);
-implementation RegressionTestInput.Class0.OutParam$System.Int32$34($this: Ref, x$in: int) returns (x$out: int, $result: int)
+implementation RegressionTestInput.Class0.OutParam$System.Int32$36($this: Ref, x$in: int) returns (x$out: int, $result: int)
{
var $localExc: Ref;
var $label: int;
@@ -1491,11 +1567,11 @@ implementation RegressionTestInput.Class0.OutParam$System.Int32$34($this: Ref, x -procedure RegressionTestInput.Class0.RefParam$System.Int32$35($this: Ref, x$in: int) returns (x$out: int, $result: int);
+procedure RegressionTestInput.Class0.RefParam$System.Int32$37($this: Ref, x$in: int) returns (x$out: int, $result: int);
-implementation RegressionTestInput.Class0.RefParam$System.Int32$35($this: Ref, x$in: int) returns (x$out: int, $result: int)
+implementation RegressionTestInput.Class0.RefParam$System.Int32$37($this: Ref, x$in: int) returns (x$out: int, $result: int)
{
var $localExc: Ref;
var $label: int;
@@ -1512,11 +1588,11 @@ implementation RegressionTestInput.Class0.RefParam$System.Int32$35($this: Ref, x -procedure RegressionTestInput.Class0.AssignToInParam$System.Int3236($this: Ref, x$in: int) returns ($result: int);
+procedure RegressionTestInput.Class0.AssignToInParam$System.Int3238($this: Ref, x$in: int) returns ($result: int);
-implementation RegressionTestInput.Class0.AssignToInParam$System.Int3236($this: Ref, x$in: int) returns ($result: int)
+implementation RegressionTestInput.Class0.AssignToInParam$System.Int3238($this: Ref, x$in: int) returns ($result: int)
{
var x: int;
var $localExc: Ref;
@@ -1534,11 +1610,11 @@ implementation RegressionTestInput.Class0.AssignToInParam$System.Int3236($this: -procedure {:RegressionTestInput.Async} RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int3237($this: Ref, x$in: int) returns ($result: int);
+procedure {:RegressionTestInput.Async} RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int3239($this: Ref, x$in: int) returns ($result: int);
-implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int3237($this: Ref, x$in: int) returns ($result: int)
+implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int3239($this: Ref, x$in: int) returns ($result: int)
{
var x: int;
var $localExc: Ref;
@@ -1552,11 +1628,11 @@ implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMetho -procedure RegressionTestInput.Class0.CallAsyncMethod$System.Int3238($this: Ref, y$in: int) returns ($result: int);
+procedure RegressionTestInput.Class0.CallAsyncMethod$System.Int3240($this: Ref, y$in: int) returns ($result: int);
-implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int3238($this: Ref, y$in: int) returns ($result: int)
+implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int3240($this: Ref, y$in: int) returns ($result: int)
{
var y: int;
var $tmp9: int;
@@ -1565,7 +1641,7 @@ implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int3238($this: y := y$in;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 60} true;
- call {:async} $tmp9 := RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int3237($this, y);
+ call {:async} $tmp9 := RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int3239($this, y);
if ($Exception != null)
{
return;
@@ -1577,16 +1653,16 @@ implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int3238($this: -procedure RegressionTestInput.Class0.#ctor39($this: Ref);
+procedure RegressionTestInput.Class0.#ctor41($this: Ref);
-implementation RegressionTestInput.Class0.#ctor39($this: Ref)
+implementation RegressionTestInput.Class0.#ctor41($this: Ref)
{
var $localExc: Ref;
var $label: int;
- call System.Object.#ctor44($this);
+ call System.Object.#ctor46($this);
if ($Exception != null)
{
return;
@@ -1597,11 +1673,11 @@ implementation RegressionTestInput.Class0.#ctor39($this: Ref) -procedure RegressionTestInput.Class0.#cctor();
+procedure T$RegressionTestInput.Class0.#cctor();
-implementation RegressionTestInput.Class0.#cctor()
+implementation T$RegressionTestInput.Class0.#cctor()
{
RegressionTestInput.Class0.StaticInt := 0;
}
@@ -1618,11 +1694,11 @@ var RegressionTestInput.ClassWithBoolTypes.staticB: bool; var RegressionTestInput.ClassWithBoolTypes.b: [Ref]bool;
-procedure RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3240(x$in: int, y$in: int) returns ($result: bool);
+procedure RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3242(x$in: int, y$in: int) returns ($result: bool);
-implementation RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3240(x$in: int, y$in: int) returns ($result: bool)
+implementation RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3242(x$in: int, y$in: int) returns ($result: bool)
{
var x: int;
var y: int;
@@ -1638,11 +1714,11 @@ implementation RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3 -procedure RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean41($this: Ref, z$in: bool);
+procedure RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean43($this: Ref, z$in: bool);
-implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean41($this: Ref, z$in: bool)
+implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean43($this: Ref, z$in: bool)
{
var z: bool;
var $localExc: Ref;
@@ -1651,7 +1727,7 @@ implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean41($th z := z$in;
RegressionTestInput.ClassWithBoolTypes.b[$this] := false;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 72} true;
- call System.Object.#ctor44($this);
+ call System.Object.#ctor46($this);
if ($Exception != null)
{
return;
@@ -1674,18 +1750,18 @@ implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean41($th -procedure RegressionTestInput.ClassWithBoolTypes.Main42();
+procedure RegressionTestInput.ClassWithBoolTypes.Main44();
-implementation RegressionTestInput.ClassWithBoolTypes.Main42()
+implementation RegressionTestInput.ClassWithBoolTypes.Main44()
{
var $tmp10: bool;
var $localExc: Ref;
var $label: int;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 78} true;
- call $tmp10 := RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3240(3, 4);
+ call $tmp10 := RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3242(3, 4);
if ($Exception != null)
{
return;
@@ -1697,11 +1773,11 @@ implementation RegressionTestInput.ClassWithBoolTypes.Main42() -procedure RegressionTestInput.ClassWithBoolTypes.#cctor();
+procedure T$RegressionTestInput.ClassWithBoolTypes.#cctor();
-implementation RegressionTestInput.ClassWithBoolTypes.#cctor()
+implementation T$RegressionTestInput.ClassWithBoolTypes.#cctor()
{
RegressionTestInput.ClassWithBoolTypes.staticB := false;
}
diff --git a/BCT/RegressionTests/TranslationTest/UnitTest0.cs b/BCT/RegressionTests/TranslationTest/UnitTest0.cs index e3da57b5..a8b5fdb2 100644 --- a/BCT/RegressionTests/TranslationTest/UnitTest0.cs +++ b/BCT/RegressionTests/TranslationTest/UnitTest0.cs @@ -61,7 +61,7 @@ namespace TranslationTest { #endregion
private string ExecuteTest(string assemblyName, HeapFactory heapFactory) {
- BCT.TranslateAssembly(new List<string>{assemblyName}, heapFactory, null, null, false);
+ BCT.TranslateAssembly(new List<string>{assemblyName}, heapFactory, new Options(), null, false);
var fileName = Path.ChangeExtension(assemblyName, "bpl");
var s = File.ReadAllText(fileName);
return s;
diff --git a/BCT/TranslationPlugins/PhoneControlsPlugin.cs b/BCT/TranslationPlugins/PhoneControlsPlugin.cs index e539b1b8..daa7c345 100644 --- a/BCT/TranslationPlugins/PhoneControlsPlugin.cs +++ b/BCT/TranslationPlugins/PhoneControlsPlugin.cs @@ -7,7 +7,7 @@ using System.IO; namespace TranslationPlugins {
public enum Visibility { Visible, Collapsed };
- public enum Event { Click, Checked, Unchecked };
+ public enum Event { Click, Checked, Unchecked, SelectionChanged };
public class HandlerSignature {
public static string[] getParameterTypesForHandler(Event controlEvent) {
@@ -15,6 +15,7 @@ namespace TranslationPlugins { case Event.Checked:
case Event.Unchecked:
case Event.Click:
+ case Event.SelectionChanged:
return new string[] { "object", "System.WindowsRoutedventArgs" };
default:
throw new NotImplementedException("Handlers for event: " + controlEvent + " not supported yet");
@@ -94,7 +95,7 @@ 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= 11;
+ private static int CONFIG_LINE_FIELDS= 12;
private static int PAGE_CLASS_FIELD= 0;
private static int PAGE_XAML_FIELD= 1;
private static int PAGE_BOOGIE_STRING_FIELD = 2;
@@ -105,7 +106,8 @@ namespace TranslationPlugins { 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 static int SELECTIONCHANGED_HANDLER_FIELD = 10;
+ private static int BPL_NAME_FIELD = 11;
private IDictionary<string, PageStructure> pageStructureInfo;
@@ -125,28 +127,6 @@ namespace TranslationPlugins { return mockBaseUri.MakeRelativeUri(mockStrippedUri).ToString();
}
- /// <summary>
- /// uri is a valid URI but possibly partial (incomplete ?arg= values) and overspecified (complete ?arg=values)
- /// This method returns a base URI
- /// </summary>
- /// <param name="uri"></param>
- /// <returns></returns>
- public static string getURIBase(string uri) {
- // I need to build an absolute URI just to call getComponents() ...
- Uri mockBaseUri = new Uri("mock://mock/", UriKind.RelativeOrAbsolute);
- Uri realUri;
- try {
- realUri = new Uri(uri, UriKind.Absolute);
- } catch (UriFormatException) {
- // uri string is relative
- realUri = new Uri(mockBaseUri, uri);
- }
-
- string str = realUri.GetComponents(UriComponents.Path | UriComponents.StrongAuthority | UriComponents.Scheme, UriFormat.UriEscaped);
- Uri mockStrippedUri = new Uri(str);
- return mockBaseUri.MakeRelativeUri(mockStrippedUri).ToString();
- }
-
//public static string getFullyQualifiedControlClass(string controlClass) {
// // TODO do an actual API discovery. The problem will be differencing 7.0 apps from 7.1 apps
// return "System.Windows.Controls." + controlClass;
@@ -190,6 +170,7 @@ namespace TranslationPlugins { }
private void setPageAsMainPage(string pageXAML) {
+ pageXAML = pageXAML.ToLower();
int lastDirPos= pageXAML.LastIndexOf('/');
if (lastDirPos != -1)
pageXAML = pageXAML.Substring(lastDirPos+1);
@@ -212,14 +193,15 @@ namespace TranslationPlugins { public void DumpControlStructure(StreamWriter outputStream) {
// maintain same format as input format
- string pageClass, pageXAML, pageBoogieStringName, controlClass, controlName, enabled, visibility, clickHandler, checkedHandler, uncheckedHandler, bplName;
+ string pageClass, pageXAML, pageBoogieStringName, controlClass, controlName, enabled, visibility, clickHandler,
+ checkedHandler, uncheckedHandler, selectionChangedHandler, bplName;
outputStream.WriteLine(getMainPageXAML());
outputStream.WriteLine(getBoogieNavigationVariable());
outputStream.WriteLine(getMainAppTypeName());
foreach (KeyValuePair<string, PageStructure> entry in this.pageStructureInfo) {
pageClass = entry.Key;
- pageXAML = entry.Value.PageXAML;
+ pageXAML = entry.Value.PageXAML.ToLower();
pageBoogieStringName = entry.Value.PageBoogieName;
foreach (ControlInfoStructure controlInfo in entry.Value.getAllControlsInfo()) {
controlClass= controlInfo.ClassName;
@@ -253,8 +235,17 @@ namespace TranslationPlugins { } else {
uncheckedHandler = "";
}
+
+ handlers = controlInfo.getHandlers(Event.SelectionChanged);
+ if (handlers.Any()) {
+ selectionChangedHandler= handlers.First().Name;
+ } else {
+ selectionChangedHandler = "";
+ }
bplName = controlInfo.BplName;
- outputStream.WriteLine(pageClass + "," + pageXAML + "," + pageBoogieStringName + "," + controlClass + "," + controlName + "," + enabled + "," + visibility + "," + clickHandler + "," + checkedHandler + "," + uncheckedHandler + "," + bplName);
+ outputStream.WriteLine(pageClass + "," + pageXAML.ToLower() + "," + pageBoogieStringName + "," + controlClass + "," + controlName + "," + enabled + "," +
+ visibility + "," + clickHandler + "," + checkedHandler + "," + uncheckedHandler + "," + selectionChangedHandler + "," +
+ bplName);
}
}
}
@@ -276,14 +267,15 @@ namespace TranslationPlugins { // TODO the page.xaml value is saved with no directory information: if two pages exist with same name but different directories it will treat them as the same
// TODO I'm not handling this for now, and I won't be handling relative/absolute URI either for now
- string pageClass, pageXAML, pageBoogieStringName, controlClass, controlName, enabled, visibility, clickHandler, checkedHandler, uncheckedHandler, bplName;
+ string pageClass, pageXAML, pageBoogieStringName, controlClass, controlName, enabled, visibility, clickHandler, checkedHandler,
+ uncheckedHandler, selectionChangedHandler, bplName;
string configLine = configStream.ReadLine();
string[] inputLine;
PageStructure pageStr;
ControlInfoStructure controlInfoStr;
// first line just states the main page xaml
- string mainPageXAML= configLine.Trim();
+ string mainPageXAML= configLine.Trim().ToLower();
configLine = configStream.ReadLine();
// second line states boogie current nav variable, possibly dummy value
@@ -305,7 +297,7 @@ namespace TranslationPlugins { throw new ArgumentException("Config input line contains wrong number of fields: " + inputLine.Length + ", expected " + CONFIG_LINE_FIELDS);
pageClass = inputLine[PAGE_CLASS_FIELD].Trim();
- pageXAML = inputLine[PAGE_XAML_FIELD].Trim();
+ pageXAML = inputLine[PAGE_XAML_FIELD].Trim().ToLower();
pageBoogieStringName = inputLine[PAGE_BOOGIE_STRING_FIELD].Trim();
controlClass = inputLine[CONTROL_CLASS_FIELD].Trim();
controlName = inputLine[CONTROL_NAME_FIELD].Trim();
@@ -317,6 +309,7 @@ namespace TranslationPlugins { clickHandler = inputLine[CLICK_HANDLER_FIELD].Trim();
checkedHandler = inputLine[CHECKED_HANDLER_FIELD].Trim();
uncheckedHandler = inputLine[UNCHECKED_HANDLER_FIELD].Trim();
+ selectionChangedHandler = inputLine[SELECTIONCHANGED_HANDLER_FIELD].Trim();
bplName = inputLine[BPL_NAME_FIELD].Trim();
try {
@@ -341,6 +334,7 @@ namespace TranslationPlugins { controlInfoStr.setHandler(Event.Click, clickHandler);
controlInfoStr.setHandler(Event.Checked, checkedHandler);
controlInfoStr.setHandler(Event.Unchecked, uncheckedHandler);
+ controlInfoStr.setHandler(Event.SelectionChanged, selectionChangedHandler);
pageStr.setControlInfo(controlName, controlInfoStr);
pageStructureInfo[pageClass] = pageStr;
|