You can subscribe to this list here.
2008 |
Jan
|
Feb
|
Mar
|
Apr
|
May
(16) |
Jun
(42) |
Jul
(46) |
Aug
(48) |
Sep
(33) |
Oct
(26) |
Nov
(28) |
Dec
(38) |
---|---|---|---|---|---|---|---|---|---|---|---|---|
2009 |
Jan
(35) |
Feb
(80) |
Mar
(112) |
Apr
(108) |
May
(102) |
Jun
(126) |
Jul
(89) |
Aug
(82) |
Sep
(36) |
Oct
(7) |
Nov
(1) |
Dec
(4) |
2010 |
Jan
(87) |
Feb
|
Mar
(2) |
Apr
(1) |
May
|
Jun
|
Jul
|
Aug
|
Sep
|
Oct
|
Nov
|
Dec
|
From: <fra...@us...> - 2009-08-28 19:59:47
|
Revision: 1864 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1864&view=rev Author: frankrimlinger Date: 2009-08-28 19:59:39 +0000 (Fri, 28 Aug 2009) Log Message: ----------- Realized that most of the MangoFormal aliasing the system source code is very harmful and very unnecessary. At some point, lost sight of the design goal of aliasing, which is simply to allow the class loader to admit both the real and the aliased system classes. The burden on Mango is then to ensure that all formal analysis is done using the aliased class methods, not the real ones. Therefore, the only thing that needs to be aliased within the source code are 1) the actual name of the class within the class declaration, and to the extent there are package visibility issues, the names of the extended classes 2) final methods that cannot be overloaded, 3) constructor method names, which of course must be the same as the aliased class name, 4) anything else I can't think of right now. TODO eliminating all method name, field name, and signature aliasing in the system source code. The only final method that gets the treatment is getClass_MangoFormal(). START WITH Double_MangoFormal. TODO: Simplify MangoMethodPeer, which is supposed to produced the aliased methods. Signature aliasing is no longer necessary. It is only necessary to alias getClass to getClass_MangoFormal. Since the JVM patches in the constructors, they are not an issue. End of story. Completed native implementation of Object_MangoFormal. Created new class mango.lang.reflect.Mango_Array for native array accessors. Created mango.io.Mango_PrintStream to provide native buffer support. Complete rewrite of Array_MangoFormal to use new native accessors. Another issue has to do with "this". If you are going to pass "this" to another method, you might have to wrap with a native method like so XXX formal2nominal(XXX_MangoFormal obj){} The native implementation just returns obj, but the declaration at the source code level is enough to fake out the compiler. Probably this issue is what started the signature aliasing business, but clearly the new solution is bfc. Put all the required formal2nominal methods in the native support class mango.lang.Mango_Object NB: Of course it is ok for native support to have _MangoFormal in signatures if this helps avoid formal2nominal wrappers. Final thought: you could always write your own class loader, but it would have to be integrated into jpf core and it really does not belong there. Modified Paths: -------------- branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/MakeClass.java branches/mango/Mango/Mango/src/mango/worker/Worker.java branches/mango/Mango/Mango/src/mango/worker/engine/hash/Hash.java branches/mango/Mango/Mango/src/mango/worker/engine/rule/Rule.java branches/mango/Mango/javapathfinder-mango-bridge/mango/CompositionImplication.java branches/mango/Mango/javapathfinder-mango-bridge/mango/StableImplication.java branches/mango/Mango/javapathfinder-mango-bridge/mango/TemplateImplication.java branches/mango/Mango/mangoUserHome/frank/rules/rulebase.zip branches/mango/Mango/mangoUserHome/system/System/java/io/FileOutputStream_MangoFormal.java branches/mango/Mango/mangoUserHome/system/System/java/io/FilterOutputStream_MangoFormal.java branches/mango/Mango/mangoUserHome/system/System/java/io/InputStream_MangoFormal.java branches/mango/Mango/mangoUserHome/system/System/java/io/ObjectStreamClass_MangoFormal.java branches/mango/Mango/mangoUserHome/system/System/java/io/OutputStream_MangoFormal.java branches/mango/Mango/mangoUserHome/system/System/java/io/PrintStream_MangoFormal.java branches/mango/Mango/mangoUserHome/system/System/java/lang/Boolean_MangoFormal.java branches/mango/Mango/mangoUserHome/system/System/java/lang/Byte_MangoFormal.java branches/mango/Mango/mangoUserHome/system/System/java/lang/CharSequence_MangoFormal.java branches/mango/Mango/mangoUserHome/system/System/java/lang/Character_MangoFormal.java branches/mango/Mango/mangoUserHome/system/System/java/lang/ClassCastException_MangoFormal.java branches/mango/Mango/mangoUserHome/system/System/java/lang/Class_MangoFormal.java branches/mango/Mango/mangoUserHome/system/System/java/lang/Double_MangoFormal.java branches/mango/Mango/mangoUserHome/system/System/java/lang/Object_MangoFormal.java branches/mango/Mango/mangoUserHome/system/System/java/lang/reflect/Array_MangoFormal.java branches/mango/Mango/mangoUserHome/system/System/mango/lang/Mango_Byte.java branches/mango/Mango/mangoUserHome/system/System/mango/lang/Mango_Class.java Added Paths: ----------- branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/HashCode.java branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Object_MangoFormal/ branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Object_MangoFormal/getClass_MangoFormal()Ljava.lang.Class_MangoFormal;/ branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Object_MangoFormal/getClass_MangoFormal()Ljava.lang.Class_MangoFormal;/Final case.zip branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Object_MangoFormal/getClass_MangoFormal([Ljava.lang.Object_MangoFormal;)Ljava.lang.Class_MangoFormal;/ branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Object_MangoFormal/getClass_MangoFormal([Ljava.lang.Object_MangoFormal;)Ljava.lang.Class_MangoFormal;/Final case.zip branches/mango/Mango/mangoUserHome/frank/sessions/mango/ branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/ branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/ branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/Mango_Array/ branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/Mango_Array/<init>()V/ branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/Mango_Array/<init>()V/Final case.zip branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/Mango_Array/getLength(Ljava.lang.Object_MangoFormal;)I/ branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/Mango_Array/getLength(Ljava.lang.Object_MangoFormal;)I/Final case.zip branches/mango/Mango/mangoUserHome/system/System/mango/io/ branches/mango/Mango/mangoUserHome/system/System/mango/io/Mango_PrintStream.java branches/mango/Mango/mangoUserHome/system/System/mango/lang/reflect/ branches/mango/Mango/mangoUserHome/system/System/mango/lang/reflect/Mango_Array.java Removed Paths: ------------- branches/mango/Mango/mangoUserHome/system/System/mango/lang/Mango_Boolean.java branches/mango/Mango/mangoUserHome/system/System/mango/lang/Mango_Object.java This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <fra...@us...> - 2009-08-28 03:26:45
|
Revision: 1863 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1863&view=rev Author: frankrimlinger Date: 2009-08-28 03:26:37 +0000 (Fri, 28 Aug 2009) Log Message: ----------- Another tweak to ATHROWCREATOR. The issue is whether or not the originating instruction of the throw is an invocation or not. If it is an invocation, then a frame has already been set up for the called method, and we need to pop that frame *before* setting up the exception. But if the originating instruction is NOT an invocation, then ATHROWCREATE just puts the exception on the current frame. NB: this has nothing to do with an exception thrown but not caught within the called method. These are handled by a different mechanism. This issue has been bouncing around all summer. I finally get it. Modified Paths: -------------- branches/mango/Mango/Mango/src/mango/worker/Worker.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROWCREATOR.java branches/mango/Mango/mangoUserHome/frank/rules/rulebase.zip branches/mango/Mango/mangoUserHome/frank/sessions/Casting/cast(DFILI;)LI;/objI is undefined.zip branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/forName(Ljava.lang.String_MangoFormal;)Ljava.lang.Class_MangoFormal;/Final case. className is undefined.zip branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/forName(Ljava.lang.String_MangoFormal;)Ljava.lang.Class_MangoFormal;/className is defined.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getComponentType(Ljava.lang.Class_MangoFormal;)Ljava.lang.Class_MangoFormal;/Final case. clazz is an array.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getComponentType(Ljava.lang.Class_MangoFormal;)Ljava.lang.Class_MangoFormal;/clazz is not an array.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getComponentType(Ljava.lang.Class_MangoFormal;)Ljava.lang.Class_MangoFormal;/clazz is undefined.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getName()Ljava.lang.String_MangoFormal;/Final case.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/intComponentTest2()Ljava.lang.String_MangoFormal;/Final case.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isPrimitive(Ljava.lang.Class_MangoFormal;)Z/clazz is defined.zip Added Paths: ----------- branches/mango/Mango/mangoUserHome/frank/sessions/Casting/<init>()V/Final case.zip branches/mango/Mango/mangoUserHome/frank/sessions/Casting/cast(DFILI;)LI;/Final case. objI may be cast to I.zip branches/mango/Mango/mangoUserHome/frank/sessions/Casting/cast(DFILI;)LI;/objI may not be cast to I.zip branches/mango/Mango/mangoUserHome/frank/sessions/I/<init>()V/Final case.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isInterface(Ljava.lang.Class_MangoFormal;)Z/Final case. clazz is undefined.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isInterface(Ljava.lang.Class_MangoFormal;)Z/clazz is defined.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isInterfaceIsFalse()Z/Final case.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isInterfaceIsTrue()Z/Final case.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isPrimitive(Ljava.lang.Class_MangoFormal;)Z/Final case. clazz is undefined.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isPrimitiveFalse()Z/Final case.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isPrimitiveTrue()Z/Final case.zip Removed Paths: ------------- branches/mango/Mango/mangoUserHome/frank/sessions/Casting/<init>()V/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/Casting/cast(DFILI;)LI;/Class name of objI may be cast to I.zip branches/mango/Mango/mangoUserHome/frank/sessions/Casting/cast(DFILI;)LI;/Class name of objI may not be cast to I.zip branches/mango/Mango/mangoUserHome/frank/sessions/I/<init>()V/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/I/compareTo(LI;)I/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/I/compareTo(Ljava.lang.Object_MangoFormal;)I/Class name of compareTo_LocalVar_at_offset_1_lineNumber_1 may be cast to I.zip branches/mango/Mango/mangoUserHome/frank/sessions/I/compareTo(Ljava.lang.Object_MangoFormal;)I/Class name of compareTo_LocalVar_at_offset_1_lineNumber_1 may not be cast to I.zip branches/mango/Mango/mangoUserHome/frank/sessions/I/compareTo(Ljava.lang.Object_MangoFormal;)I/compareTo_LocalVar_at_offset_1_lineNumber_1 is undefined.zip branches/mango/Mango/mangoUserHome/frank/sessions/I/whatHappens()Ljava.lang.Class_MangoFormal;/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/I/whatHappens1()Ljava.lang.Class_MangoFormal;/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/I/whatHappens2()Ljava.lang.Class_MangoFormal;/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/I/whatHappens3()Ljava.lang.Class_MangoFormal;/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isPrimitive(Ljava.lang.Class_MangoFormal;)Z/clazz is undefined.zip This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <fra...@us...> - 2009-08-27 22:50:04
|
Revision: 1862 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1862&view=rev Author: frankrimlinger Date: 2009-08-27 22:49:44 +0000 (Thu, 27 Aug 2009) Log Message: ----------- These are the notes for 1861, somehow they didn't take. Fixed nasty bug in MakeClass action, which was returning a ClassNameSym instead of the correct ClassObjectSym. The distinction is critical. A ClassNameSym is the name of a class, and as such is the value of an expression (valueH (loc obj ^className) heap) On the other hand, a ClassNameObject names a Class object, as such is the return value of a method-returning-Class<?>. Since the native implementations of forName() and getComponentType() ultimately boil down to the MakeClass action, these implementations were broken. With this fix, specification of public String intComponentTest(){ Class<?> clazz=int[].class.getComponentType(); boolean test=(clazz.equals(Integer.TYPE)); if(test){ return clazz.getName(); } return "failed"; } is Final case: Returns java.lang.String: int Actually, to get the specification to look like this, reimplemented an old device to omit heap items that are represented as the return value in "special" cases, like that of a String. FWIW, it is now conceptually easier to implement other special cases as then need arises. Also, got rid of the "." at the end of the return value, which is more confusion then help. Also, suppressing "_MangoFormal" in all translations, as this is in an internal thing. Note that _MangoFormal is still exposed to the file system, and to method signatures. There is no easy way around this. Fixed specification window so that it *displays* the name of the current session with _MangoFormal suppressed. This is more readable. A session name now indicates whether or not it is the final case. The cases of session can be replayed in any order, except that the final case has to be last. No more guessing which one that is. Need to finish rebuilding all sessions for changes to take root. With all this clean up in place, it remains to rehab the Object implementation, do the heapPtr upgrade, declare MangoBaseline. Then finally the real project can start. Modified Paths: -------------- branches/mango/Mango/Mango/src/mango/worker/Worker.java This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <fra...@us...> - 2009-08-27 22:46:36
|
Revision: 1861 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1861&view=rev Author: frankrimlinger Date: 2009-08-27 22:46:22 +0000 (Thu, 27 Aug 2009) Log Message: ----------- Modified Paths: -------------- branches/mango/Mango/Mango/src/mango/control/action/input/RuleBaseAction.java branches/mango/Mango/Mango/src/mango/core/CoreRule.java branches/mango/Mango/Mango/src/mango/module/definition/action/CloseBothAction.java branches/mango/Mango/Mango/src/mango/module/definition/action/CloseCaseAction.java branches/mango/Mango/Mango/src/mango/module/definition/model/DefinitionManager.java branches/mango/Mango/Mango/src/mango/module/definition/msg/CloseCaseMsg.java branches/mango/Mango/Mango/src/mango/module/definition/msg/CloseCaseTranslateMsg.java branches/mango/Mango/Mango/src/mango/module/definition/msg/DeleteUnusedParametersMsg.java branches/mango/Mango/Mango/src/mango/module/definition/trap/CloseCaseConnector.java branches/mango/Mango/Mango/src/mango/module/definition/trap/HarvestParametersTrap.java branches/mango/Mango/Mango/src/mango/module/definition/trap/ScriptedCloseCaseConnector.java branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/GetVirtualRunTimeMethod.java branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/MakeComponentClass.java branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/string/GetCanonicalTypeName.java branches/mango/Mango/Mango/src/mango/ruleAction/translate/engine/Quotes.java branches/mango/Mango/Mango/src/mango/script/gui/action/ScriptOpenAction.java branches/mango/Mango/Mango/src/mango/script/gui/action/ScriptSaveAction.java branches/mango/Mango/Mango/src/mango/worker/Worker.java branches/mango/Mango/Mango/src/mango/worker/msg/NewWorkerMsg.java branches/mango/Mango/Mango/src/mango/worker/msg/RulebaseMsg.java branches/mango/Mango/Mango/src/mango/worker/workFlow/invariant/trap/BuildInvariantNamesConnector.java branches/mango/Mango/Mango/src/mango/worker/workFlow/invariant/trap/BuildInvariantNamesTrap.java branches/mango/Mango/Mango/src/mango/worker/workFlow/translate/agent/TranslateModuleAgent.java branches/mango/Mango/Mango/src/mango/worker/workFlow/translate/sym/TranslationSym.java branches/mango/Mango/Mango/src/mango/worker/workFlow/translate/trap/ScriptedTranslateTrap.java branches/mango/Mango/Mango/src/mango/worker/workFlow/translate/trap/TranslateTrap.java branches/mango/Mango/mangoUserHome/frank/rules/rulebase.zip branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/forName(Ljava.lang.String_MangoFormal;)Ljava.lang.Class_MangoFormal;/className is defined.zip branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/isAssignableFrom(Ljava.lang.Class_MangoFormal;)Z/cls is defined.zip branches/mango/Mango/mangoUserHome/system/SystemTests/src/systemTests/ClassTests.java branches/mango/Mango/src/mango/views/GenSpecWindow.java Added Paths: ----------- branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Boolean_MangoFormal/ branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Boolean_MangoFormal/booleanValue()Z/ branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Boolean_MangoFormal/booleanValue()Z/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Boolean_MangoFormal/equals(Ljava.lang.Object_MangoFormal;)Z/ branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Boolean_MangoFormal/equals(Ljava.lang.Object_MangoFormal;)Z/obj is undefined.zip branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Boolean_MangoFormal/equals(Ljava.lang.Object_MangoFormal;)Z/obj may not be cast to java.lang.Boolean_MangoFormal.zip branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Boolean_MangoFormal/equals(Ljava.lang.Object_MangoFormal;)Z/this._value does not equal obj._value.zip branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Boolean_MangoFormal/equals(Ljava.lang.Object_MangoFormal;)Z/this._value equals obj._value.zip branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/<init>()V/ branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/<init>()V/Final case.zip branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/forName(Ljava.lang.String_MangoFormal;)Ljava.lang.Class_MangoFormal;/Final case. className is undefined.zip branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/getComponentType()Ljava.lang.Class_MangoFormal;/Final case. this is not an array.zip branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/getComponentType()Ljava.lang.Class_MangoFormal;/this is an array.zip branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/isAssignableFrom(Ljava.lang.Class_MangoFormal;)Z/Final case. cls is undefined.zip branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Integer_MangoFormal/ branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Integer_MangoFormal/equals(Ljava.lang.Object_MangoFormal;)Z/ branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Integer_MangoFormal/equals(Ljava.lang.Object_MangoFormal;)Z/obj is undefined.zip branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Integer_MangoFormal/equals(Ljava.lang.Object_MangoFormal;)Z/obj may not be cast to java.lang.Integer_MangoFormal.zip branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Integer_MangoFormal/equals(Ljava.lang.Object_MangoFormal;)Z/this._value does not equal obj._value.zip branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Integer_MangoFormal/equals(Ljava.lang.Object_MangoFormal;)Z/this._value equals obj._value.zip branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Integer_MangoFormal/intValue()I/ branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Integer_MangoFormal/intValue()I/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/<init>()V/Final case.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/compatibleFalse()Z/Final case.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/compatibleFalse(Ljava.lang.Class_MangoFormal;Ljava.lang.Class_MangoFormal;)Z/Final case. x is defined, y is defined.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/compatibleTrue()Z/Final case.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getComponentType()Ljava.lang.Class_MangoFormal;/Final case.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getComponentType(Ljava.lang.Class_MangoFormal;)Ljava.lang.Class_MangoFormal;/Final case. clazz is an array.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getComponentType(Ljava.lang.Class_MangoFormal;)Ljava.lang.Class_MangoFormal;/clazz is not an array.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getComponentType(Ljava.lang.Class_MangoFormal;)Ljava.lang.Class_MangoFormal;/clazz is undefined.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getComponentType2()Ljava.lang.Class_MangoFormal;/Final case.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getName()Ljava.lang.String_MangoFormal;/Final case.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/intComponentTest()Ljava.lang.String_MangoFormal;/ branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/intComponentTest()Ljava.lang.String_MangoFormal;/Final case.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/intComponentTest2()Ljava.lang.String_MangoFormal;/ branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/intComponentTest2()Ljava.lang.String_MangoFormal;/Final case.zip Removed Paths: ------------- branches/mango/Mango/mangoUserHome/frank/sessions/a.zip branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/forName(Ljava.lang.String_MangoFormal;)Ljava.lang.Class_MangoFormal;/className is undefined.zip branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/getComponentType()Ljava.lang.Class_MangoFormal;/Class name of this is an array.zip branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/getComponentType()Ljava.lang.Class_MangoFormal;/Class name of this is not a loadable class.zip branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/isAssignableFrom(Ljava.lang.Class_MangoFormal;)Z/cls is undefined.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/compatibleFalse()Z/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/compatibleFalse(Ljava.lang.Class_MangoFormal;Ljava.lang.Class_MangoFormal;)Z/x is defined, y is defined.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/compatibleTrue()Z/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getComponentType()Ljava.lang.Class_MangoFormal;/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getComponentType(Ljava.lang.Class_MangoFormal;)Ljava.lang.Class_MangoFormal;/Class name of clazz is an array.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getComponentType2()Ljava.lang.Class_MangoFormal;/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getName()Ljava.lang.String_MangoFormal;/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isInterface(Ljava.lang.Class_MangoFormal;)Z/clazz is defined.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isInterface(Ljava.lang.Class_MangoFormal;)Z/clazz is undefined.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isInterfaceIsFalse()Z/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isInterfaceIsTrue()Z/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isPrimitiveFalse()Z/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isPrimitiveTrue()Z/a.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isPrimitiveTrue()Z/case.zip This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <fra...@us...> - 2009-08-27 03:52:02
|
Revision: 1860 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1860&view=rev Author: frankrimlinger Date: 2009-08-27 03:51:56 +0000 (Thu, 27 Aug 2009) Log Message: ----------- As usual, "_MangoFormal" suprressed. Preliminary to rehab of Object class, devised a tricky test of Class.getComponent: public String intComponentTest(){ Class<?> clazz=int[].class.getComponentType(); boolean test=(clazz.equals(Integer.TYPE)); if(test){ return clazz.getName(); } return "failed"; } In order to specify this, assuming that Class.equals() just delegates to Object.equals(). BUG: the zen question, is equals(Ljava/lang/Object)Z accessible to the class int, is causing some trouble. Modified Paths: -------------- branches/mango/Mango/Mango/src/mango/ruleAction/typeAssignment/AssignNotObjectValue.java branches/mango/Mango/Mango/src/mango/worker/Worker.java branches/mango/Mango/mangoUserHome/frank/rules/rulebase.zip branches/mango/Mango/mangoUserHome/frank/sessions/a.zip branches/mango/Mango/mangoUserHome/system/System/java/lang/Object_MangoFormal.java branches/mango/Mango/mangoUserHome/system/System/java/lang/reflect/Array_MangoFormal.java branches/mango/Mango/mangoUserHome/system/SystemTests/src/systemTests/ClassTests.java Added Paths: ----------- branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Byte_MangoFormal/ branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Byte_MangoFormal/byteValue()B/ branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Byte_MangoFormal/byteValue()B/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Byte_MangoFormal/equals(Ljava.lang.Object_MangoFormal;)Z/ branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Byte_MangoFormal/equals(Ljava.lang.Object_MangoFormal;)Z/obj is undefined.zip branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Byte_MangoFormal/equals(Ljava.lang.Object_MangoFormal;)Z/obj may not be cast to java.lang.Byte_MangoFormal.zip branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Byte_MangoFormal/equals(Ljava.lang.Object_MangoFormal;)Z/this._value does not equal obj._value.zip branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Byte_MangoFormal/equals(Ljava.lang.Object_MangoFormal;)Z/this._value equals obj._value.zip This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <fra...@us...> - 2009-08-27 02:47:50
|
Revision: 1859 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1859&view=rev Author: frankrimlinger Date: 2009-08-27 02:47:43 +0000 (Thu, 27 Aug 2009) Log Message: ----------- Fixed bug in ATRHOWCREATOR that cause a thrown exception to be placed on the called frame instead of the caller frame. Fixed "special" subaddress translation bug. Completed testing of Class_MangoFormal. Modified Paths: -------------- branches/mango/Mango/Mango/src/mango/control/action/input/RuleBaseAction.java branches/mango/Mango/Mango/src/mango/core/CoreMangoActiveObject.java branches/mango/Mango/Mango/src/mango/core/CoreRule.java branches/mango/Mango/Mango/src/mango/core/CoreRuleBase.java branches/mango/Mango/Mango/src/mango/core/gui/action/NewCoreRuleAction.java branches/mango/Mango/Mango/src/mango/module/model/ModuleManager.java branches/mango/Mango/Mango/src/mango/ruleAction/translate/engine/TranslateValueH.java branches/mango/Mango/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashEnterpriseAndTranslation.java branches/mango/Mango/Mango/src/mango/worker/engine/sym/Sym.java branches/mango/Mango/Mango/src/mango/worker/msg/NewWorkerMsg.java branches/mango/Mango/Mango/src/mango/worker/msg/RulebaseMsg.java branches/mango/Mango/Mango/src/mango/worker/workFlow/translate/sym/TranslationSym.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROWCREATOR.java branches/mango/Mango/mangoUserHome/frank/rules/rulebase.zip Added Paths: ----------- branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isInterface(Ljava.lang.Class_MangoFormal;)Z/ branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isInterface(Ljava.lang.Class_MangoFormal;)Z/clazz is defined.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isInterface(Ljava.lang.Class_MangoFormal;)Z/clazz is undefined.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isInterfaceIsFalse()Z/ branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isInterfaceIsFalse()Z/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isInterfaceIsTrue()Z/ branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isInterfaceIsTrue()Z/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isPrimitive(Ljava.lang.Class_MangoFormal;)Z/clazz is defined.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isPrimitive(Ljava.lang.Class_MangoFormal;)Z/clazz is undefined.zip This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <fra...@us...> - 2009-08-26 22:42:49
|
Revision: 1858 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1858&view=rev Author: frankrimlinger Date: 2009-08-26 22:42:39 +0000 (Wed, 26 Aug 2009) Log Message: ----------- Fixed numerous bugs in implicit rule generation mechanism. Added feature to force generation of rules with a given arity even if there is no core rule pattern witness for that arity. This is necessary for a few passive rulekeys like "replace", which is used by the ExpLevelSym mechanism. Tracked down several troublesome rulekeys while replaying and bound them to their arities. Also made the new template types non-minimal, as they certainly don't need to be minimal and this was interfering with typing mechanism, in accordance with the law of unintended side-effects. Because the typing system is so powerful, it is likely it will speciate somewhere down the line. But for now it's based on a flat namespace. Getting away from flat introduces very complex issues, because ultimately all typing systems are flat, so what are you really doing? Added final rules to convert static access: ( getstatic #Smango.worker.engine.sym.ImmutableSym java.lang.Integer_MangoFormal.TYPE stat ) --> #Smango.worker.engine.sym.ClassObjectSym int for each of the 9 primitive types, as documented in Class.isPrimitive(). With this in place, Class_MangoFormal native implementation of isPrimitive tests correctly public boolean isPrimitiveTrue(){ return Integer.TYPE.isPrimitive(); } specified as Close Case: Returns boolean: true. public boolean isPrimitiveFalse(){ return Integer.class.isPrimitive(); } specified as Close Case: Returns boolean: false. This is particularly satisfying because never could get this right in the past. Next bug: for some reason, ClassTests.isPrimitive() for null input is putting the NullPointerException on the called frame instead of the caller frame. Use a.zip. Modified Paths: -------------- branches/mango/Mango/Mango/src/mango/control/action/input/RuleBaseAction.java branches/mango/Mango/Mango/src/mango/core/mfl/CoreMFLCreator.java branches/mango/Mango/Mango/src/mango/module/definition/loop/msg/LoopDefinitionRequestMsg.java branches/mango/Mango/Mango/src/mango/module/definition/method/msg/MethodDefinitionRequestMsg.java branches/mango/Mango/Mango/src/mango/module/definition/model/DefinitionManager.java branches/mango/Mango/Mango/src/mango/module/definition/msg/ManualDefinitionMsg.java branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/IsPrimitiveClass.java branches/mango/Mango/Mango/src/mango/worker/Worker.java branches/mango/Mango/Mango/src/mango/worker/engine/events/RewriteEvent.java branches/mango/Mango/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashRecent.java branches/mango/Mango/Mango/src/mango/worker/engine/rule/Rule.java branches/mango/Mango/Mango/src/mango/worker/engine/rule/RuleBase.java branches/mango/Mango/Mango/src/mango/worker/engine/rule/TemplateRule.java branches/mango/Mango/Mango/src/mango/worker/engine/rule/synthetic/CompositionRule.java branches/mango/Mango/Mango/src/mango/worker/engine/rule/synthetic/ImplicitRule.java branches/mango/Mango/Mango/src/mango/worker/engine/rule/synthetic/StableRule.java branches/mango/Mango/Mango/src/mango/worker/engine/rule/synthetic/SyntheticRule.java branches/mango/Mango/Mango/src/mango/worker/engine/rule/synthetic/TemplateBindingRule.java branches/mango/Mango/Mango/src/mango/worker/engine/rule/synthetic/TemplateInstanceRule.java branches/mango/Mango/Mango/src/mango/worker/mangoModel/agent/ValueHAgent.java branches/mango/Mango/Mango/src/mango/worker/msg/NewWorkerMsg.java branches/mango/Mango/Mango/src/mango/worker/msg/RulebaseMsg.java branches/mango/Mango/javapathfinder-mango-bridge/mango/CompositionImplication.java branches/mango/Mango/javapathfinder-mango-bridge/mango/FormalTypes.java branches/mango/Mango/javapathfinder-mango-bridge/mango/StableImplication.java branches/mango/Mango/javapathfinder-mango-bridge/mango/TemplateImplication.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/MangoClassPeer.java branches/mango/Mango/mangoUserHome/frank/rules/rulebase.zip branches/mango/Mango/mangoUserHome/frank/sessions/Casting/<init>()V/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/Casting/cast(DFILI;)LI;/Class name of objI may be cast to I.zip branches/mango/Mango/mangoUserHome/frank/sessions/Casting/cast(DFILI;)LI;/Class name of objI may not be cast to I.zip branches/mango/Mango/mangoUserHome/frank/sessions/Casting/cast(DFILI;)LI;/objI is undefined.zip branches/mango/Mango/mangoUserHome/frank/sessions/I/<init>()V/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/I/compareTo(LI;)I/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/I/compareTo(Ljava.lang.Object_MangoFormal;)I/Class name of compareTo_LocalVar_at_offset_1_lineNumber_1 may be cast to I.zip branches/mango/Mango/mangoUserHome/frank/sessions/I/compareTo(Ljava.lang.Object_MangoFormal;)I/Class name of compareTo_LocalVar_at_offset_1_lineNumber_1 may not be cast to I.zip branches/mango/Mango/mangoUserHome/frank/sessions/I/compareTo(Ljava.lang.Object_MangoFormal;)I/compareTo_LocalVar_at_offset_1_lineNumber_1 is undefined.zip branches/mango/Mango/mangoUserHome/frank/sessions/I/whatHappens()Ljava.lang.Class_MangoFormal;/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/I/whatHappens1()Ljava.lang.Class_MangoFormal;/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/I/whatHappens2()Ljava.lang.Class_MangoFormal;/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/I/whatHappens3()Ljava.lang.Class_MangoFormal;/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/baseline/itsAWrap/clear([I)V/Array length of x is greater than or equal to 10.zip branches/mango/Mango/mangoUserHome/frank/sessions/baseline/itsAWrap/main([I)Z/x[5] equals x[6].zip branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/forName(Ljava.lang.String_MangoFormal;)Ljava.lang.Class_MangoFormal;/className is defined.zip branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/forName(Ljava.lang.String_MangoFormal;)Ljava.lang.Class_MangoFormal;/className is undefined.zip branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/getComponentType()Ljava.lang.Class_MangoFormal;/Class name of this is an array.zip branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/getComponentType()Ljava.lang.Class_MangoFormal;/Class name of this is not a loadable class.zip branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/isAssignableFrom(Ljava.lang.Class_MangoFormal;)Z/cls is defined.zip branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/isAssignableFrom(Ljava.lang.Class_MangoFormal;)Z/cls is undefined.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/<init>()V/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/compatibleFalse()Z/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/compatibleFalse(Ljava.lang.Class_MangoFormal;Ljava.lang.Class_MangoFormal;)Z/x is defined, y is defined.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/compatibleTrue()Z/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getComponentType()Ljava.lang.Class_MangoFormal;/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getComponentType(Ljava.lang.Class_MangoFormal;)Ljava.lang.Class_MangoFormal;/Class name of clazz is an array.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getComponentType2()Ljava.lang.Class_MangoFormal;/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getName()Ljava.lang.String_MangoFormal;/case.zip branches/mango/Mango/mangoUserHome/system/SystemTests/src/systemTests/ClassTests.java branches/mango/Mango/src/mango/views/LogWindow.java Added Paths: ----------- branches/mango/Mango/mangoUserHome/frank/sessions/a.zip branches/mango/Mango/mangoUserHome/frank/sessions/baseline/itsAWrap/clear([I)V/loops/-baseline.itsAWrap.clear([I)V#8- dload_i_Code_01/a.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isPrimitive(Ljava.lang.Class_MangoFormal;)Z/ branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isPrimitiveFalse()Z/ branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isPrimitiveFalse()Z/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isPrimitiveTrue()Z/a.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isPrimitiveTrue()Z/case.zip Removed Paths: ------------- branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getName()Ljava.lang.String;/ This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <ppa...@us...> - 2009-08-26 12:43:32
|
Revision: 1857 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1857&view=rev Author: pparizek Date: 2009-08-26 12:43:23 +0000 (Wed, 26 Aug 2009) Log Message: ----------- support for static initializers and correct propagation of exceptions over boundaries of memory scopes Modified Paths: -------------- trunk/extensions/rtembed/env/jpf/javax/realtime/Clock.java trunk/extensions/rtembed/env/jpf/javax/realtime/LTMemory.java trunk/extensions/rtembed/env/jpf/javax/realtime/MemoryArea.java trunk/extensions/rtembed/env/jpf/javax/realtime/ScopedMemory.java trunk/extensions/rtembed/env/jvm/gov/nasa/jpf/rtembed/JPF_javax_realtime_MemoryArea.java trunk/extensions/rtembed/src/gov/nasa/jpf/rtembed/memory/MemoryAreasChecker.java Added Paths: ----------- trunk/extensions/rtembed/env/jpf/javax/realtime/ThrowBoundaryError.java trunk/extensions/rtembed/test/gov/nasa/jpf/rtembed/memory/ExceptionPropagation1.java trunk/extensions/rtembed/test/gov/nasa/jpf/rtembed/memory/ExceptionPropagation2.java trunk/extensions/rtembed/test/gov/nasa/jpf/rtembed/memory/MemoryAreaArgsError.java This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <fra...@us...> - 2009-08-25 22:13:31
|
Revision: 1856 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1856&view=rev Author: frankrimlinger Date: 2009-08-25 22:13:22 +0000 (Tue, 25 Aug 2009) Log Message: ----------- Completed implementation of implicit rule generation. Testing underway. Opted for new extensions of the Rule class to characterize stable rules, composition rules, template binding rules, and template instantiated rules. The four corresponding classes now extend the abstract class SyntheticRule. The SyntheticRule class implements the ProxyRule interface, which contains the method getProxy(). Using getProxy(), SyntheticRule can bounce a lot of routine rule requests to the proxy, which is a Rule. The four concrete SyntheticRule classes implement getProxy() as appropriate, and can concentrate on initializing their fields correctly. This new breakout relieves a lot of complexity in the Rule class, and obviates the need for RuleManager classes, which have been deleted. Also introduced TemplateRule class to model the concrete template rules. The TemplateRuleManager has not been folded into TemplateRule because this manager really has some complex tasks to perform. The point of the TemplateRule class is just to enable handling of creation, destruction and indexing issues in a more uniform manner. Modified Paths: -------------- branches/mango/Mango/Mango/src/mango/core/CoreRule.java branches/mango/Mango/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashCoreParser.java branches/mango/Mango/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashRecent.java branches/mango/Mango/Mango/src/mango/worker/engine/rule/ActiveObject.java branches/mango/Mango/Mango/src/mango/worker/engine/rule/Rule.java branches/mango/Mango/Mango/src/mango/worker/engine/rule/TemplateRuleManager.java branches/mango/Mango/Mango/src/mango/worker/msg/NewWorkerMsg.java branches/mango/Mango/javapathfinder-mango-bridge/mango/StableImplication.java Added Paths: ----------- branches/mango/Mango/Mango/src/mango/worker/engine/rule/TemplateRule.java branches/mango/Mango/Mango/src/mango/worker/engine/rule/synthetic/ branches/mango/Mango/Mango/src/mango/worker/engine/rule/synthetic/CompositionRule.java branches/mango/Mango/Mango/src/mango/worker/engine/rule/synthetic/ImplicitRule.java branches/mango/Mango/Mango/src/mango/worker/engine/rule/synthetic/ProxyRule.java branches/mango/Mango/Mango/src/mango/worker/engine/rule/synthetic/StableRule.java branches/mango/Mango/Mango/src/mango/worker/engine/rule/synthetic/SyntheticRule.java branches/mango/Mango/Mango/src/mango/worker/engine/rule/synthetic/TemplateBindingRule.java branches/mango/Mango/Mango/src/mango/worker/engine/rule/synthetic/TemplateInstanceRule.java Removed Paths: ------------- branches/mango/Mango/Mango/src/mango/worker/engine/rule/CompositionRuleManager.java branches/mango/Mango/Mango/src/mango/worker/engine/rule/StableRuleManager.java branches/mango/Mango/Mango/src/mango/worker/engine/rule/TemplateRuleKeyBindingManager.java This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <fra...@us...> - 2009-08-25 04:58:51
|
Revision: 1855 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1855&view=rev Author: frankrimlinger Date: 2009-08-25 04:58:44 +0000 (Tue, 25 Aug 2009) Log Message: ----------- Implementation of automatic rule generation managers in progress, per 1853 Modified Paths: -------------- branches/mango/Mango/Mango/src/mango/core/CoreRule.java branches/mango/Mango/Mango/src/mango/worker/engine/rule/Rule.java branches/mango/Mango/Mango/src/mango/worker/engine/rule/StableRuleManager.java branches/mango/Mango/Mango/src/mango/worker/engine/rule/TemplateRuleKeyBindingManager.java Added Paths: ----------- branches/mango/Mango/Mango/src/mango/worker/engine/rule/CompositionRuleManager.java Removed Paths: ------------- branches/mango/Mango/Mango/src/mango/worker/engine/rule/ComposeRuleManager.java This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <fra...@us...> - 2009-08-25 01:48:51
|
Revision: 1854 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1854&view=rev Author: frankrimlinger Date: 2009-08-25 01:48:34 +0000 (Tue, 25 Aug 2009) Log Message: ----------- Replaces all Hashtables with HashMaps. The distinction is unimportant for Mango since the code is (supposedly) thread safe anyway, but HashMaps are more modern and have better syntax. Modified Paths: -------------- branches/mango/Mango/Mango/src/mango/control/window/WorkstationFindWindow.java branches/mango/Mango/Mango/src/mango/core/CoreKonsFactory.java branches/mango/Mango/Mango/src/mango/core/CoreMFLexportProxySymFactory.java branches/mango/Mango/Mango/src/mango/core/CoreSymFactory.java branches/mango/Mango/Mango/src/mango/core/CoreVariableFactory.java branches/mango/Mango/Mango/src/mango/core/RuleResourceManager.java branches/mango/Mango/Mango/src/mango/core/gui/window/CoreRuleBaseWindowFactory.java branches/mango/Mango/Mango/src/mango/core/numbers/CoreNumberFactory.java branches/mango/Mango/Mango/src/mango/core/statistic/StatisticManager.java branches/mango/Mango/Mango/src/mango/core/statistic/StatisticUpdateFactory.java branches/mango/Mango/Mango/src/mango/core/util/CoreUtilities.java branches/mango/Mango/Mango/src/mango/deprecatedPackage/DeprecatedMethods.java branches/mango/Mango/Mango/src/mango/enterprise/locator/LocatableFolderViewer.java branches/mango/Mango/Mango/src/mango/enterprise/locator/MFLocator.java branches/mango/Mango/Mango/src/mango/enterprise/sym/ExpLevelSym.java branches/mango/Mango/Mango/src/mango/enterprise/workerID/WorkerID.java branches/mango/Mango/Mango/src/mango/graph/msg/MultiGraph3DViewCreateRequestMsg.java branches/mango/Mango/Mango/src/mango/gumboModel/ColorDataBinding.java branches/mango/Mango/Mango/src/mango/gumboModel/factory/EmbeddedJVMFactory.java branches/mango/Mango/Mango/src/mango/gumboModel/factory/ListModelFactory.java branches/mango/Mango/Mango/src/mango/gumboModel/factory/MultiGraphModelFactory.java branches/mango/Mango/Mango/src/mango/gumboModel/window/DebugFlagsDialog.java branches/mango/Mango/Mango/src/mango/merge/tree/MangoMergeTreeModel.java branches/mango/Mango/Mango/src/mango/module/definition/model/CheckBoxVectorModel.java branches/mango/Mango/Mango/src/mango/module/definition/model/DefinitionManager.java branches/mango/Mango/Mango/src/mango/module/definition/msg/ApplyCondMapMsg.java branches/mango/Mango/Mango/src/mango/module/definition/sym/ParamSym.java branches/mango/Mango/Mango/src/mango/module/instance/loop/agent/LoopInstanceAgent.java branches/mango/Mango/Mango/src/mango/module/instance/method/agent/MethodInstanceAgent.java branches/mango/Mango/Mango/src/mango/module/instance/model/InstanceManager.java branches/mango/Mango/Mango/src/mango/module/instance/model/InstanceUtil.java branches/mango/Mango/Mango/src/mango/module/model/ModuleManager.java branches/mango/Mango/Mango/src/mango/module/model/RuleModel.java branches/mango/Mango/Mango/src/mango/module/sym/ModuleLevelSym.java branches/mango/Mango/Mango/src/mango/module/sym/ModuleReadOnlySym.java branches/mango/Mango/Mango/src/mango/rmi/file/MangoJarDirectory.java branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/conditional/Generalize.java branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/conditional/Match.java branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/conditional/MatchAssumptionList.java branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/conditional/SubType.java branches/mango/Mango/Mango/src/mango/ruleAction/form/binder/BindBoot.java branches/mango/Mango/Mango/src/mango/ruleRequirement/naturalLanguage/Automatic.java branches/mango/Mango/Mango/src/mango/ruleRequirement/naturalLanguage/Contextual.java branches/mango/Mango/Mango/src/mango/source/agent/SourceViewAgent.java branches/mango/Mango/Mango/src/mango/source/data/SourceModel.java branches/mango/Mango/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashEngine.java branches/mango/Mango/Mango/src/mango/worker/engine/rule/Rule.java branches/mango/Mango/Mango/src/mango/worker/engine/rule/RuleBase.java branches/mango/Mango/Mango/src/mango/worker/engine/rule/TemplateRuleManager.java branches/mango/Mango/Mango/src/mango/worker/engine/sym/ObjMap.java branches/mango/Mango/Mango/src/mango/worker/mangoModel/agent/ValueHAgent.java branches/mango/Mango/Mango/src/mango/worker/mangoModel/backupDelegate/AlphaDelegate.java branches/mango/Mango/Mango/src/mango/worker/mangoModel/backupDelegate/BackupDelegate.java branches/mango/Mango/Mango/src/mango/worker/mangoModel/backupDelegate/CodeDelegate.java branches/mango/Mango/Mango/src/mango/worker/mangoModel/backupDelegate/EdgeDelegate.java branches/mango/Mango/Mango/src/mango/worker/mangoModel/backupDelegate/GraphDelegate.java branches/mango/Mango/Mango/src/mango/worker/mangoModel/backupDelegate/OmegaDelegate.java branches/mango/Mango/Mango/src/mango/worker/mangoModel/backupDelegate/UconDelegate.java branches/mango/Mango/Mango/src/mango/worker/mangoModel/graph/Graph.java branches/mango/Mango/Mango/src/mango/worker/mangoModel/vertex/Vertex.java branches/mango/Mango/Mango/src/mango/worker/msg/NewWorkerMsg.java branches/mango/Mango/Mango/src/mango/worker/workFlow/coreTechniques/agent/BackchainAgent.java branches/mango/Mango/Mango/src/mango/worker/workFlow/coreTechniques/agent/GeneralizeAgent.java branches/mango/Mango/Mango/src/mango/worker/workFlow/coreTechniques/agent/OverAgent.java branches/mango/Mango/Mango/src/mango/worker/workFlow/coreTechniques/model/HeapPointer.java branches/mango/Mango/Mango/src/mango/worker/workFlow/coreTechniques/model/HeapTracer.java branches/mango/Mango/Mango/src/mango/worker/workFlow/coreTechniques/sym/FoundationSym.java branches/mango/Mango/Mango/src/mango/worker/workFlow/coreTechniques/trap/CellUpdateTrap.java branches/mango/Mango/Mango/src/mango/worker/workFlow/form/agent/ConvertCharArrayToStringAgent.java branches/mango/Mango/Mango/src/mango/worker/workFlow/form/model/HeapItemModel.java branches/mango/Mango/Mango/src/mango/worker/workFlow/form/model/HeapModel.java branches/mango/Mango/Mango/src/mango/worker/workFlow/functionSpace/sym/ModuleHypothesisSym.java branches/mango/Mango/Mango/src/mango/worker/workFlow/functionSpace/sym/ModuleInvocationSym.java branches/mango/Mango/Mango/src/mango/worker/workFlow/invariant/agent/InvariantHypoAgent.java branches/mango/Mango/Mango/src/mango/worker/workFlow/invariant/model/FactorizationModel.java branches/mango/Mango/Mango/src/mango/worker/workFlow/invariant/model/InvariantModel.java branches/mango/Mango/Mango/src/mango/worker/workFlow/invariant/model/InvariantStatus.java branches/mango/Mango/Mango/src/mango/worker/workFlow/model/HitemUtil.java branches/mango/Mango/Mango/src/mango/worker/workFlow/msg/InitSessionMsg.java branches/mango/Mango/Mango/src/mango/worker/workFlow/translate/agent/TranslateModuleAgent.java branches/mango/Mango/javapathfinder-mango-bridge/mango/FormalTypes.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/CodeSurvey.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/MangoClassPeer.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/MangoMethodPeer.java Added Paths: ----------- branches/mango/Mango/Mango/src/mango/worker/engine/rule/ComposeRuleManager.java branches/mango/Mango/Mango/src/mango/worker/engine/rule/StableRuleManager.java branches/mango/Mango/Mango/src/mango/worker/engine/rule/TemplateRuleKeyBindingManager.java This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <fra...@us...> - 2009-08-24 23:13:05
|
Revision: 1853 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1853&view=rev Author: frankrimlinger Date: 2009-08-24 21:38:27 +0000 (Mon, 24 Aug 2009) Log Message: ----------- Auto-generation of stable rules, composition rules, and template-rulekey bindings in progress. The corresponding static rules have been removed from the rulebase, and all requisite implications for dynamic instantiation been introduced into the type system. It remains to create the new RuleManager classes and implement dynamic rule instantiation. The design is as follows. The StableRuleManager will generate the rules required for stability. 1. Each rulekey that wants to participate will imply the <stableExp> type. 2. When a rule is initialized, if the lead rulekey has the <stableExp> type, then the rulekey together with the number of arguments n is passed to the StableRuleManager. 3. If necessary, the stable rule manager instantiates a stable rule: Name "<rulekey>_stableExp<n>" Pattern: (rulekey x1 ... x_n) Action: Substitution Requirement: x1 Stable ... x_n Stable Substitution: (rulekey x1 ... x_n) The ComposeRuleManager will generate the rules required for composition. 1. Each rulekey that wants to participate will imply the <composeExp> type. 2. When a rule is initialized, if the lead rulekey has the <stableExp> type, then the rulekey together with the number of arguments is n passed to the ComposeRuleManager. 3. If necessary, the stable rule manager instantiates a compose rule: Name: "<rulekey>_composeExp<n>" Pattern: (o (rulekey x1 ...x_n) state) Action: Substitution Requirement: x1 Stable ... x_n Stable state Stable Substitution: (rulekey (o x1 state) ... (o x_n state)) The TemplateRuleKeyBindingManager will generate the rules requirement for template-rulekey binding 1. For each family of template rule-key binding actions Template.XXXn, introduce the formal type <Template.XXX>. Each such type implies the formal type <templateRuleKeyBinding>. Each rulekey that wants a Template.XXX binding will imply the <Template.XXX> type. 2. When a rule is initialized, if the lead rulekey has the <templateRuleKeyBinding> type, then the rulekey together with the number of arguments is n passed to the TemplateRuleKeyBindingManager. 3. If necessary, for each detected type <Template.XXX> of the rulekey, the TemplateRuleKeyBindingManager will generate the following rule: Name: "<rulekey>_Template.XXX<n>" Pattern: (rulekey 'Template) Action: Template.XXX<n> Modified Paths: -------------- branches/mango/Mango/Mango/src/mango/core/CoreRule.java branches/mango/Mango/Mango/src/mango/core/util/CoreUtilities.java branches/mango/Mango/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashMangoModel.java branches/mango/Mango/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashRecent.java branches/mango/Mango/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashTyping.java branches/mango/Mango/javapathfinder-mango-bridge/mango/FormalTypes.java branches/mango/Mango/mangoUserHome/frank/rules/rulebase.zip branches/mango/Mango/mangoUserHome/frank/sessions/baseline/itsAWrap/<init>()V/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/baseline/itsAWrap/clear([I)V/Array length of x is greater than or equal to 10.zip branches/mango/Mango/mangoUserHome/frank/sessions/baseline/itsAWrap/clear([I)V/loops/-baseline.itsAWrap.clear([I)V#8- dload_i_Code_01/op0 is less than 10.zip branches/mango/Mango/mangoUserHome/frank/sessions/baseline/itsAWrap/main([I)Z/x[5] equals x[6].zip Added Paths: ----------- branches/mango/Mango/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashStable.java branches/mango/Mango/javapathfinder-mango-bridge/mango/CompositionImplication.java branches/mango/Mango/javapathfinder-mango-bridge/mango/StableImplication.java branches/mango/Mango/javapathfinder-mango-bridge/mango/TemplateImplication.java Removed Paths: ------------- branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/conditional/GetFreeVariableName.java This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <fra...@us...> - 2009-08-24 05:12:21
|
Revision: 1852 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1852&view=rev Author: frankrimlinger Date: 2009-08-24 05:12:08 +0000 (Mon, 24 Aug 2009) Log Message: ----------- Completed specification for Class_MangoFormal. Testing in progress. Modified Paths: -------------- branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/IsPrimitiveClass.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/MangoClassPeer.java branches/mango/Mango/mangoUserHome/frank/rules/rulebase.zip branches/mango/Mango/mangoUserHome/frank/sessions/Casting/<init>()V/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/Casting/cast(DFILI;)LI;/Class name of objI may be cast to I.zip branches/mango/Mango/mangoUserHome/frank/sessions/Casting/cast(DFILI;)LI;/Class name of objI may not be cast to I.zip branches/mango/Mango/mangoUserHome/frank/sessions/Casting/cast(DFILI;)LI;/objI is undefined.zip branches/mango/Mango/mangoUserHome/frank/sessions/I/<init>()V/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/I/whatHappens()Ljava.lang.Class_MangoFormal;/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/I/whatHappens1()Ljava.lang.Class_MangoFormal;/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/I/whatHappens2()Ljava.lang.Class_MangoFormal;/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/I/whatHappens3()Ljava.lang.Class_MangoFormal;/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/compatibleTrue()Z/case.zip branches/mango/Mango/mangoUserHome/system/SystemTests/src/systemTests/ClassTests.java Added Paths: ----------- branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/IsInterface.java branches/mango/Mango/Mango/src/mango/ruleAction/translate/semantics/AddSemanticsForIsInterface.java branches/mango/Mango/Mango/src/mango/ruleAction/translate/semantics/AddSemanticsForIsPrimitiveClass.java branches/mango/Mango/Mango/src/mango/worker/workFlow/translate/model/semantics/SemanticsForIsInterface.java branches/mango/Mango/Mango/src/mango/worker/workFlow/translate/model/semantics/SemanticsForIsPrimitiveClass.java branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/isInterface()Z/ branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/isInterface()Z/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/compatibleFalse(Ljava.lang.Class_MangoFormal;Ljava.lang.Class_MangoFormal;)Z/ branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/compatibleFalse(Ljava.lang.Class_MangoFormal;Ljava.lang.Class_MangoFormal;)Z/x is defined, y is defined.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getComponentType(Ljava.lang.Class_MangoFormal;)Ljava.lang.Class_MangoFormal;/ branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getComponentType(Ljava.lang.Class_MangoFormal;)Ljava.lang.Class_MangoFormal;/Class name of clazz is an array.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isPrimitiveTrue()Z/ branches/mango/Mango/mangoUserHome/system/System/java/lang/Worksheet for isPrimitive.txt This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <fra...@us...> - 2009-08-24 00:50:39
|
Revision: 1851 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1851&view=rev Author: frankrimlinger Date: 2009-08-24 00:50:29 +0000 (Mon, 24 Aug 2009) Log Message: ----------- session update Modified Paths: -------------- branches/mango/Mango/mangoUserHome/frank/sessions/I/<init>()V/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/I/compareTo(LI;)I/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/I/compareTo(Ljava.lang.Object_MangoFormal;)I/Class name of compareTo_LocalVar_at_offset_1_lineNumber_1 may be cast to I.zip branches/mango/Mango/mangoUserHome/frank/sessions/I/compareTo(Ljava.lang.Object_MangoFormal;)I/Class name of compareTo_LocalVar_at_offset_1_lineNumber_1 may not be cast to I.zip branches/mango/Mango/mangoUserHome/frank/sessions/I/compareTo(Ljava.lang.Object_MangoFormal;)I/compareTo_LocalVar_at_offset_1_lineNumber_1 is undefined.zip branches/mango/Mango/mangoUserHome/frank/sessions/I/whatHappens()Ljava.lang.Class_MangoFormal;/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/I/whatHappens1()Ljava.lang.Class_MangoFormal;/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/I/whatHappens2()Ljava.lang.Class_MangoFormal;/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/I/whatHappens3()Ljava.lang.Class_MangoFormal;/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/baseline/itsAWrap/<init>()V/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/baseline/itsAWrap/clear([I)V/Array length of x is greater than or equal to 10.zip branches/mango/Mango/mangoUserHome/frank/sessions/baseline/itsAWrap/clear([I)V/loops/-baseline.itsAWrap.clear([I)V#8- dload_i_Code_01/op0 is less than 10.zip branches/mango/Mango/mangoUserHome/frank/sessions/baseline/itsAWrap/main([I)Z/x[5] equals x[6].zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/<init>()V/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/compatibleFalse()Z/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getComponentType()Ljava.lang.Class_MangoFormal;/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getComponentType2()Ljava.lang.Class_MangoFormal;/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getName()Ljava.lang.String_MangoFormal;/case.zip Added Paths: ----------- branches/mango/Mango/mangoUserHome/frank/sessions/Casting/ branches/mango/Mango/mangoUserHome/frank/sessions/Casting/<init>()V/ branches/mango/Mango/mangoUserHome/frank/sessions/Casting/<init>()V/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/Casting/cast(DFILI;)LI;/ branches/mango/Mango/mangoUserHome/frank/sessions/Casting/cast(DFILI;)LI;/Class name of objI may be cast to I.zip branches/mango/Mango/mangoUserHome/frank/sessions/Casting/cast(DFILI;)LI;/Class name of objI may not be cast to I.zip branches/mango/Mango/mangoUserHome/frank/sessions/Casting/cast(DFILI;)LI;/objI is undefined.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/compatibleTrue()Z/case.zip This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <fra...@us...> - 2009-08-24 00:29:18
|
Revision: 1850 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1850&view=rev Author: frankrimlinger Date: 2009-08-24 00:29:11 +0000 (Mon, 24 Aug 2009) Log Message: ----------- fixed erros in system source code Modified Paths: -------------- branches/mango/Mango/mangoUserHome/system/System/java/lang/Class_MangoFormal.java branches/mango/Mango/mangoUserHome/system/SystemTests/src/systemTests/ClassTests.java This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <fra...@us...> - 2009-08-24 00:17:53
|
Revision: 1849 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1849&view=rev Author: frankrimlinger Date: 2009-08-24 00:16:33 +0000 (Mon, 24 Aug 2009) Log Message: ----------- Deleted all obsolete mango.util.Util code and dispersed the rest of the methods. Deleted all the "J" classes, originally introduced to deal with the trickier questions of JVM interpretation. Specifically, JclassSym, JnonclassSym, JmethodSym, and JfieldSym are gone, resulting in a significant simplification of the javapathfinder-mango-bridge. The pipeline from .class files to mango level is now strictly bcel->jpf-> formal peer. Restricted the meaning ClassNameSym and the formal type <classNameSymbol>. To avoid unsoundness, introduced ClassObjectSym and <classObject>. A ClassObjectSym simultaneously represents the name of a Class and the Class object representing that class, so we have the rule (valueH (loc classObjectSym ^className) heap) --> classObjectSym (We suppress the implicit "_MangoFormal" suffix throughout this discussion.) A ClassNameSym simply represents the name of a Class, so (valueH (loc obj ^className) heap) is evaluated by examining heap for a heap item of the form [obj,^className]= classNameSym. Since there is never an item on the heap of the form [classObjectSym, ^className]=... there is no conflict between these rules. To appreciate the distinction, consider (getVirtualRunTimeMethod classNameSym uniqueName) which evaluates by forming the ClassInfo with the same name as classNameSym and performing the lookup on uniqueName. However, (getVirtualRunTimeMethod classObjectSym uniqueName) evaluates by forming the ClassInfo for Class and looking up uniqueName. Now consider the real world example ClassTests.class.getName(); which generates First LDC will produce a String "ClassTests" of type CLASS, which is interpreted as a ClassObjectSym. Then INVOKEVIRTUAL, formally interpreted, leads to (getVirtualRunTimeMethod "ClassTests" getName()Ljava.lang.String; ) Here is the punch line: since "ClassTests" is a ClassObjectSym, we use Class.getName(), which native implementation returns (valueH (loc "ClassTests" ^className) heap) --> "ClassTests" as desired. To support, native implementation for Object.getClass() must create a ClassObjectSym. Replayed all sessions. Modified Paths: -------------- branches/mango/Mango/Mango/src/mango/control/action/control/StopWorkerAction.java branches/mango/Mango/Mango/src/mango/control/action/control/WorkerAction.java branches/mango/Mango/Mango/src/mango/control/action/editor/NameAction.java branches/mango/Mango/Mango/src/mango/control/action/editor/PostAction.java branches/mango/Mango/Mango/src/mango/control/action/input/RuleBaseAction.java branches/mango/Mango/Mango/src/mango/control/action/window/ResetPopupAction.java branches/mango/Mango/Mango/src/mango/control/editor/MFLEditorWindow.java branches/mango/Mango/Mango/src/mango/control/msg/OpenMFLEditorRequestMsg.java branches/mango/Mango/Mango/src/mango/control/msg/OpenMFLasAxiomRequestMsg.java branches/mango/Mango/Mango/src/mango/control/msg/ReplayedMsg.java branches/mango/Mango/Mango/src/mango/core/CoreKons.java branches/mango/Mango/Mango/src/mango/core/CoreKonsFactory.java branches/mango/Mango/Mango/src/mango/core/CoreMangoObject.java branches/mango/Mango/Mango/src/mango/core/CoreRule.java branches/mango/Mango/Mango/src/mango/core/CoreTier.java branches/mango/Mango/Mango/src/mango/core/ProxyActiveObject.java branches/mango/Mango/Mango/src/mango/core/RuleResourceManager.java branches/mango/Mango/Mango/src/mango/core/gui/action/ApplyCoreRuleAction.java branches/mango/Mango/Mango/src/mango/core/gui/action/CloneCoreRuleAction.java branches/mango/Mango/Mango/src/mango/core/gui/action/CoreCutAction.java branches/mango/Mango/Mango/src/mango/core/gui/action/CorePasteAction.java branches/mango/Mango/Mango/src/mango/core/gui/action/DownloadCoreRuleAction.java branches/mango/Mango/Mango/src/mango/core/gui/action/EnforceTierSettingsAction.java branches/mango/Mango/Mango/src/mango/core/gui/action/ImportCoreRuleAction.java branches/mango/Mango/Mango/src/mango/core/gui/action/ImportCoreTierAction.java branches/mango/Mango/Mango/src/mango/core/gui/action/NewCoreRuleAction.java branches/mango/Mango/Mango/src/mango/core/gui/action/NewCoreTierAction.java branches/mango/Mango/Mango/src/mango/core/gui/action/SaveCoreRuleBaseAction.java branches/mango/Mango/Mango/src/mango/core/gui/action/SaveCoreRuleBaseOutlineAction.java branches/mango/Mango/Mango/src/mango/core/gui/action/ScriptedActivateAction.java branches/mango/Mango/Mango/src/mango/core/gui/action/ScriptedDeactivateAction.java branches/mango/Mango/Mango/src/mango/core/gui/tablemodel/CoreRuleBaseTableModel.java branches/mango/Mango/Mango/src/mango/core/gui/tablemodel/CoreTierTableModel.java branches/mango/Mango/Mango/src/mango/core/gui/tablemodel/CoreVariableTableModel.java branches/mango/Mango/Mango/src/mango/core/gui/window/CoreRuleEditorWindow.java branches/mango/Mango/Mango/src/mango/core/io/MangoEncoder.java branches/mango/Mango/Mango/src/mango/core/mfl/CoreMFLBuilder.java branches/mango/Mango/Mango/src/mango/core/mfl/CoreMFLTokenizer.java branches/mango/Mango/Mango/src/mango/core/sym/RuleBaseSym.java branches/mango/Mango/Mango/src/mango/coreserver/file/FileManager.java branches/mango/Mango/Mango/src/mango/debugger/BreakPointWindow.java branches/mango/Mango/Mango/src/mango/debugger/DebuggerViewManager.java branches/mango/Mango/Mango/src/mango/debugger/DebuggerWindow.java branches/mango/Mango/Mango/src/mango/debugger/action/BreakPointTypeAction.java branches/mango/Mango/Mango/src/mango/debugger/action/ClearAllBreakPointsAction.java branches/mango/Mango/Mango/src/mango/debugger/action/RuleKeyBreakPointAction.java branches/mango/Mango/Mango/src/mango/debugger/action/StepAction.java branches/mango/Mango/Mango/src/mango/debugger/action/StopRewritingAction.java branches/mango/Mango/Mango/src/mango/debugger/model/SingleStep.java branches/mango/Mango/Mango/src/mango/debugger/model/SingleStepTracker.java branches/mango/Mango/Mango/src/mango/debugger/model/StepAll.java branches/mango/Mango/Mango/src/mango/debugger/msg/ClearBreakPointMsg.java branches/mango/Mango/Mango/src/mango/debugger/msg/ContinueRewritingMsg.java branches/mango/Mango/Mango/src/mango/debugger/msg/SetBreakPointMsg.java branches/mango/Mango/Mango/src/mango/debugger/msg/SetBreakPointTypeMsg.java branches/mango/Mango/Mango/src/mango/debugger/msg/SetRuleKeyBreakPointMsg.java branches/mango/Mango/Mango/src/mango/debugger/msg/SingleOffMsg.java branches/mango/Mango/Mango/src/mango/debugger/msg/SingleOnMsg.java branches/mango/Mango/Mango/src/mango/debugger/msg/SingleStepMsg.java branches/mango/Mango/Mango/src/mango/debugger/msg/StopRewritingMsg.java branches/mango/Mango/Mango/src/mango/enterprise/locator/LocatorManager.java branches/mango/Mango/Mango/src/mango/enterprise/model/GetPredicateTransformer.java branches/mango/Mango/Mango/src/mango/enterprise/model/HiddenObject.java branches/mango/Mango/Mango/src/mango/enterprise/model/MethodProxy.java branches/mango/Mango/Mango/src/mango/enterprise/sym/ExpLevelSym.java branches/mango/Mango/Mango/src/mango/enterprise/workerID/PersistentParityID.java branches/mango/Mango/Mango/src/mango/enterprise/workerID/SourceAspectID.java branches/mango/Mango/Mango/src/mango/enterprise/workerID/TransientParityID.java branches/mango/Mango/Mango/src/mango/enterprise/workerID/WorkerID.java branches/mango/Mango/Mango/src/mango/graph/Graph2DViewWindow.java branches/mango/Mango/Mango/src/mango/graph/agent/CoarseGraphViewAgent.java branches/mango/Mango/Mango/src/mango/graph/agent/GraphViewAgent.java branches/mango/Mango/Mango/src/mango/graph/msg/Graph3DViewCreateCommandMsg.java branches/mango/Mango/Mango/src/mango/gumboModel/ColorDataBinding.java branches/mango/Mango/Mango/src/mango/gumboModel/ViewBuilder.java branches/mango/Mango/Mango/src/mango/gumboModel/action/ActionManager.java branches/mango/Mango/Mango/src/mango/gumboModel/action/MangoActionMenuItem.java branches/mango/Mango/Mango/src/mango/gumboModel/action/SingleSelectAction.java branches/mango/Mango/Mango/src/mango/gumboModel/agent/ActionAgent.java branches/mango/Mango/Mango/src/mango/gumboModel/agent/AspectModelAgent.java branches/mango/Mango/Mango/src/mango/gumboModel/factory/TreeModelFactory.java branches/mango/Mango/Mango/src/mango/gumboModel/interaction/MangoViewManager.java branches/mango/Mango/Mango/src/mango/gumboModel/interaction/PopupMenuManager.java branches/mango/Mango/Mango/src/mango/gumboModel/msg/GumboCommand.java branches/mango/Mango/Mango/src/mango/gumboModel/msg/PopupMenuCommand.java branches/mango/Mango/Mango/src/mango/gumboModel/window/ChildWindow.java branches/mango/Mango/Mango/src/mango/merge/action/SelectCoreRuleBaseAction.java branches/mango/Mango/Mango/src/mango/module/ModuleWindowManager.java branches/mango/Mango/Mango/src/mango/module/definition/AbstractEquivalenceWindow.java branches/mango/Mango/Mango/src/mango/module/definition/action/AddEquivalenceAction.java branches/mango/Mango/Mango/src/mango/module/definition/action/GenericPopupAction.java branches/mango/Mango/Mango/src/mango/module/definition/action/ShowCaseAction.java branches/mango/Mango/Mango/src/mango/module/definition/loop/LoopDefinitionManager.java branches/mango/Mango/Mango/src/mango/module/definition/loop/msg/LoopDefinitionRequestMsg.java branches/mango/Mango/Mango/src/mango/module/definition/method/MethodDefinitionManager.java branches/mango/Mango/Mango/src/mango/module/definition/method/msg/CreateMethodStubMsg.java branches/mango/Mango/Mango/src/mango/module/definition/method/msg/MethodDefinitionRequestMsg.java branches/mango/Mango/Mango/src/mango/module/definition/model/DefinitionManager.java branches/mango/Mango/Mango/src/mango/module/definition/msg/AddConjectureLocatorMsg.java branches/mango/Mango/Mango/src/mango/module/definition/msg/AddConjectureRequestMsg.java branches/mango/Mango/Mango/src/mango/module/definition/msg/AddConjectureTranslateMsg.java branches/mango/Mango/Mango/src/mango/module/definition/msg/AddEquivalenceAutoRequestMsg.java branches/mango/Mango/Mango/src/mango/module/definition/msg/AddEquivalenceConjectureLocatorMsg.java branches/mango/Mango/Mango/src/mango/module/definition/msg/AddEquivalenceConjectureRequestMsg.java branches/mango/Mango/Mango/src/mango/module/definition/msg/AddEquivalenceRequestMsg.java branches/mango/Mango/Mango/src/mango/module/definition/msg/AddHypothesisAutoRequestMsg.java branches/mango/Mango/Mango/src/mango/module/definition/msg/AddHypothesisLocatorMsg.java branches/mango/Mango/Mango/src/mango/module/definition/msg/AddHypothesisRequestMsg.java branches/mango/Mango/Mango/src/mango/module/definition/msg/AddHypothesisTranslateMsg.java branches/mango/Mango/Mango/src/mango/module/definition/msg/CloseCaseMsg.java branches/mango/Mango/Mango/src/mango/module/definition/msg/CloseCaseTranslateMsg.java branches/mango/Mango/Mango/src/mango/module/definition/msg/CloseDefinitionMsg.java branches/mango/Mango/Mango/src/mango/module/definition/msg/EliminateHypothesisRequestMsg.java branches/mango/Mango/Mango/src/mango/module/definition/msg/FinalizeStatusMsg.java branches/mango/Mango/Mango/src/mango/module/definition/sym/ParamSym.java branches/mango/Mango/Mango/src/mango/module/definition/trap/ConsistentHypoConnector.java branches/mango/Mango/Mango/src/mango/module/definition/trap/EliminateHypoTrap.java branches/mango/Mango/Mango/src/mango/module/instance/loop/agent/LoopInstanceAgent.java branches/mango/Mango/Mango/src/mango/module/instance/loop/model/LoopInstanceManager.java branches/mango/Mango/Mango/src/mango/module/instance/method/agent/MethodInstanceAgent.java branches/mango/Mango/Mango/src/mango/module/instance/method/model/MethodInstanceManager.java branches/mango/Mango/Mango/src/mango/module/instance/method/msg/CloseMethodInstanceMsg.java branches/mango/Mango/Mango/src/mango/module/instance/model/InstanceManager.java branches/mango/Mango/Mango/src/mango/module/instance/msg/MergeRequestMsg.java branches/mango/Mango/Mango/src/mango/module/instance/msg/SubmitStandingHypothesisMsg.java branches/mango/Mango/Mango/src/mango/module/instance/sym/InstanceManagerProxySym.java branches/mango/Mango/Mango/src/mango/module/instance/sym/InstanceManagerSym.java branches/mango/Mango/Mango/src/mango/module/model/ModuleManager.java branches/mango/Mango/Mango/src/mango/module/model/RuleModel.java branches/mango/Mango/Mango/src/mango/module/msg/ApplyInvarianceRulesMsg.java branches/mango/Mango/Mango/src/mango/module/msg/ApplyLinearRequestMsg.java branches/mango/Mango/Mango/src/mango/module/msg/ContainsTestMsg.java branches/mango/Mango/Mango/src/mango/module/msg/GarbageCollectRequestMsg.java branches/mango/Mango/Mango/src/mango/module/msg/GeneralizeRequestMsg.java branches/mango/Mango/Mango/src/mango/module/msg/MapToScopeRequestMsg.java branches/mango/Mango/Mango/src/mango/module/msg/MatchMakerRequestMsg.java branches/mango/Mango/Mango/src/mango/module/msg/TranslateMsg.java branches/mango/Mango/Mango/src/mango/module/sym/ModuleReadOnlySym.java branches/mango/Mango/Mango/src/mango/module/trap/GeneralizeCaseRewriteTrap.java branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/conditional/OverDisambiguation.java branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/conditional/SHOW.java branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/conditional/StabilizeArguments.java branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/conditional/SyntacticEquals.java branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/conditional/WithDiveCommutes.java branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/linear/BuildEquation.java branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/BuildInvocationUcon.java branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/Checkcast.java branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/GetInterfaceRunTimeException.java branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/GetInterfaceRunTimeMethod.java branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/GetVirtualRunTimeException.java branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/GetVirtualRunTimeMethod.java branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/IsArray.java branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/IsPrimitiveClass.java branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/IsSuperClass.java branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/MakeComponentClass.java branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/clinit/ComposePrependedClinits.java branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/clinit/HasCommutingClinit.java branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/comparison/InequivalentRef.java branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/garbageCollection/GarbageCollect.java branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/mango_math/IsDigit.java branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/mango_math/IsLetter.java branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/mango_math/IsLetterOrDigit.java branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/mango_math/IsSpaceChar.java branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/numerical/Power.java branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/sorting/SORT.java branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/string/IndexOf.java branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/string/QualifiedMember2Member.java branches/mango/Mango/Mango/src/mango/ruleAction/form/binder/StatTransitionToFunctionalContext.java branches/mango/Mango/Mango/src/mango/ruleAction/form/binder/ValueH.java branches/mango/Mango/Mango/src/mango/ruleAction/function/engine/BindFunctionSym.java branches/mango/Mango/Mango/src/mango/ruleAction/invariant/Invariant.java branches/mango/Mango/Mango/src/mango/ruleAction/module/definition/HarvestParameters.java branches/mango/Mango/Mango/src/mango/ruleAction/module/instance/BuildLoopInstanceManager.java branches/mango/Mango/Mango/src/mango/ruleAction/module/instance/BuildMethodInstanceManager.java branches/mango/Mango/Mango/src/mango/ruleAction/module/instance/IsLoopDefinitionClosed.java branches/mango/Mango/Mango/src/mango/ruleAction/module/instance/IsMethodDefinitionClosed.java branches/mango/Mango/Mango/src/mango/ruleAction/simpleSubstitution/AutomaticSubstitution.java branches/mango/Mango/Mango/src/mango/ruleAction/translate/automatic/ThisIsNotNull.java branches/mango/Mango/Mango/src/mango/ruleAction/translate/engine/TranslateLocation.java branches/mango/Mango/Mango/src/mango/ruleAction/translate/engine/TranslateModuleHypothesisSym.java branches/mango/Mango/Mango/src/mango/ruleAction/translate/engine/TranslateNotUserInvocationSym.java branches/mango/Mango/Mango/src/mango/ruleAction/translate/engine/TranslateReturnValue.java branches/mango/Mango/Mango/src/mango/ruleAction/translate/engine/TranslateUserInvocationSym.java branches/mango/Mango/Mango/src/mango/ruleAction/translate/semantics/AddSemanticsForEquality.java branches/mango/Mango/Mango/src/mango/ruleAction/translate/semantics/AddSemanticsForIsArray.java branches/mango/Mango/Mango/src/mango/ruleAction/translate/semantics/AddSemanticsForIsClassLoadable.java branches/mango/Mango/Mango/src/mango/ruleAction/translate/semantics/AddSemanticsForIsSuperClass.java branches/mango/Mango/Mango/src/mango/ruleAction/typeAssignment/AssignNotObjectValue.java branches/mango/Mango/Mango/src/mango/ruleRequirement/binder/BinderHeap.java branches/mango/Mango/Mango/src/mango/ruleRequirement/binder/ConjunctionSymReq.java branches/mango/Mango/Mango/src/mango/ruleRequirement/binder/EquationSymReq.java branches/mango/Mango/Mango/src/mango/ruleRequirement/binder/HeapObjectSymReq.java branches/mango/Mango/Mango/src/mango/ruleRequirement/binder/InequationSymReq.java branches/mango/Mango/Mango/src/mango/ruleRequirement/binder/OpStack.java branches/mango/Mango/Mango/src/mango/ruleRequirement/binder/StatItemSymReq.java branches/mango/Mango/Mango/src/mango/ruleRequirement/function/BaseInvariantAgentProxySym.java branches/mango/Mango/Mango/src/mango/ruleRequirement/function/LoopInvocationSymReq.java branches/mango/Mango/Mango/src/mango/ruleRequirement/function/MethodInvocationSymReq.java branches/mango/Mango/Mango/src/mango/ruleRequirement/function/ModuleInvocationSymReq.java branches/mango/Mango/Mango/src/mango/ruleRequirement/function/ParamSymReq.java branches/mango/Mango/Mango/src/mango/ruleRequirement/function/UserInvocationSymReq.java branches/mango/Mango/Mango/src/mango/ruleRequirement/naturalLanguage/Instantiated.java branches/mango/Mango/Mango/src/mango/ruleRequirement/symbols/MethodInstanceSymReq.java branches/mango/Mango/Mango/src/mango/ruleRequirement/symbols/StringReq.java branches/mango/Mango/Mango/src/mango/ruleRequirement/typing/ClassNameSymbolReq.java branches/mango/Mango/Mango/src/mango/ruleRequirement/typing/FrameReq.java branches/mango/Mango/Mango/src/mango/ruleRequirement/typing/FunctionReq.java branches/mango/Mango/Mango/src/mango/ruleRequirement/typing/PredTransformerReq.java branches/mango/Mango/Mango/src/mango/ruleRequirement/typing/PredicateReq.java branches/mango/Mango/Mango/src/mango/ruleRequirement/typing/numerical/ArithmeticFieldType.java branches/mango/Mango/Mango/src/mango/ruleRequirement/typing/numerical/IntegralArrayFieldType.java branches/mango/Mango/Mango/src/mango/ruleRequirement/typing/numerical/IntegralFieldType.java branches/mango/Mango/Mango/src/mango/ruleRequirement/typing/variableLength/FreeVarsReq.java branches/mango/Mango/Mango/src/mango/script/MangoScriptSourceDirectory.java branches/mango/Mango/Mango/src/mango/script/gui/action/ScriptDownAction.java branches/mango/Mango/Mango/src/mango/script/gui/action/ScriptRemoveAction.java branches/mango/Mango/Mango/src/mango/script/gui/action/ScriptRunAction.java branches/mango/Mango/Mango/src/mango/script/gui/action/ScriptSelectAllAction.java branches/mango/Mango/Mango/src/mango/script/gui/action/ScriptUpAction.java branches/mango/Mango/Mango/src/mango/script/util/MangoScriptUtilities.java branches/mango/Mango/Mango/src/mango/script/util/ScriptAndPostAction.java branches/mango/Mango/Mango/src/mango/source/agent/SourceViewAgent.java branches/mango/Mango/Mango/src/mango/tree/TreeViewWindow.java branches/mango/Mango/Mango/src/mango/tree/agent/FolderViewAgent.java branches/mango/Mango/Mango/src/mango/tree/data/TreeNodeClientData.java branches/mango/Mango/Mango/src/mango/tree/model/FolderViewer.java branches/mango/Mango/Mango/src/mango/tree/msg/ChangeTreeRequestMsg.java branches/mango/Mango/Mango/src/mango/tree/msg/TreeNodeAddCommandMsg.java branches/mango/Mango/Mango/src/mango/tree/msg/TreeNodeCloseRequestMsg.java branches/mango/Mango/Mango/src/mango/tree/msg/UndoFormattingOpenRequestMsg.java branches/mango/Mango/Mango/src/mango/util/WorkerIDNotifier.java branches/mango/Mango/Mango/src/mango/worker/Mango.java branches/mango/Mango/Mango/src/mango/worker/Worker.java branches/mango/Mango/Mango/src/mango/worker/engine/events/CallBack.java branches/mango/Mango/Mango/src/mango/worker/engine/events/Event.java branches/mango/Mango/Mango/src/mango/worker/engine/events/LocalMessage.java branches/mango/Mango/Mango/src/mango/worker/engine/events/QueueableEvent.java branches/mango/Mango/Mango/src/mango/worker/engine/events/RewriteCallBack.java branches/mango/Mango/Mango/src/mango/worker/engine/events/RewriteEvent.java branches/mango/Mango/Mango/src/mango/worker/engine/hash/Cons.java branches/mango/Mango/Mango/src/mango/worker/engine/hash/Hash.java branches/mango/Mango/Mango/src/mango/worker/engine/hash/Hitem.java branches/mango/Mango/Mango/src/mango/worker/engine/hash/Kons.java branches/mango/Mango/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHash.java branches/mango/Mango/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashEngine.java branches/mango/Mango/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashLogicAndArithmetic.java branches/mango/Mango/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashMangoModel.java branches/mango/Mango/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashOpcodeSyms.java branches/mango/Mango/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashTyping.java branches/mango/Mango/Mango/src/mango/worker/engine/rule/ActiveObject.java branches/mango/Mango/Mango/src/mango/worker/engine/rule/AssumeHypoRule.java branches/mango/Mango/Mango/src/mango/worker/engine/rule/Rule.java branches/mango/Mango/Mango/src/mango/worker/engine/rule/RuleBase.java branches/mango/Mango/Mango/src/mango/worker/engine/sym/AgentSym.java branches/mango/Mango/Mango/src/mango/worker/engine/sym/ExpressionSym.java branches/mango/Mango/Mango/src/mango/worker/engine/sym/InterpretableSym.java branches/mango/Mango/Mango/src/mango/worker/engine/sym/Sym.java branches/mango/Mango/Mango/src/mango/worker/engine/unifier/ActionCallBack.java branches/mango/Mango/Mango/src/mango/worker/engine/unifier/UnifyEvent.java branches/mango/Mango/Mango/src/mango/worker/mangoModel/BackupAlg.java branches/mango/Mango/Mango/src/mango/worker/mangoModel/backupDelegate/AlphaDelegate.java branches/mango/Mango/Mango/src/mango/worker/mangoModel/backupDelegate/EdgeDelegate.java branches/mango/Mango/Mango/src/mango/worker/mangoModel/edge/EdgeIterator.java branches/mango/Mango/Mango/src/mango/worker/mangoModel/graph/StrataGraph.java branches/mango/Mango/Mango/src/mango/worker/mangoModel/graphic/Graphic.java branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/graphic/InvocationEdgeSym.java branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/graphic/MethodSym.java branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/graphic/PackageSym.java branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/graphic/SuperVertexClassSym.java branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/reflection/StateSym.java branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/return_terminator/ReturnTerminatorSym.java branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/sink_terminator/OSsinkSym.java branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/sink_terminator/SinkTerminatorSym.java branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/sink_terminator/ThrowSym.java branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/superVertex/SuperBlowUpSym.java branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/superVertex/SuperLoopSym.java branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/superVertex/SuperStrataSym.java branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/superVertex/SuperVertexSym.java branches/mango/Mango/Mango/src/mango/worker/mangoModel/vertex/AcyclicVertex.java branches/mango/Mango/Mango/src/mango/worker/mangoModel/vertex/BackupVertex.java branches/mango/Mango/Mango/src/mango/worker/mangoModel/vertex/CallVertex.java branches/mango/Mango/Mango/src/mango/worker/mangoModel/vertex/CpnVertex.java branches/mango/Mango/Mango/src/mango/worker/mangoModel/vertex/LoopVertex.java branches/mango/Mango/Mango/src/mango/worker/mangoModel/vertex/MethodVertex.java branches/mango/Mango/Mango/src/mango/worker/mangoModel/vertex/SuperCpnVertex.java branches/mango/Mango/Mango/src/mango/worker/mangoModel/vertex/SuperVertex.java branches/mango/Mango/Mango/src/mango/worker/msg/AckPermCommand.java branches/mango/Mango/Mango/src/mango/worker/msg/AutoResetMsg.java branches/mango/Mango/Mango/src/mango/worker/msg/NewWorkerMsg.java branches/mango/Mango/Mango/src/mango/worker/msg/RulebaseMsg.java branches/mango/Mango/Mango/src/mango/worker/utilities/MutableArray.java branches/mango/Mango/Mango/src/mango/worker/workFlow/coreTechniques/agent/BackchainAgent.java branches/mango/Mango/Mango/src/mango/worker/workFlow/coreTechniques/agent/FreeVarsAgent.java branches/mango/Mango/Mango/src/mango/worker/workFlow/coreTechniques/agent/MatchAssumptionsAgent.java branches/mango/Mango/Mango/src/mango/worker/workFlow/coreTechniques/agent/SimplifyAndAgent.java branches/mango/Mango/Mango/src/mango/worker/workFlow/coreTechniques/agent/SimplifyOrAgent.java branches/mango/Mango/Mango/src/mango/worker/workFlow/coreTechniques/agent/WithAgent.java branches/mango/Mango/Mango/src/mango/worker/workFlow/coreTechniques/model/HeapPointer.java branches/mango/Mango/Mango/src/mango/worker/workFlow/coreTechniques/model/HeapTracer.java branches/mango/Mango/Mango/src/mango/worker/workFlow/coreTechniques/msg/RewriteLocatorMsg.java branches/mango/Mango/Mango/src/mango/worker/workFlow/coreTechniques/msg/RewriteRequestMsg.java branches/mango/Mango/Mango/src/mango/worker/workFlow/coreTechniques/msg/StableRewriteLocator.java branches/mango/Mango/Mango/src/mango/worker/workFlow/coreTechniques/sym/FoundationSym.java branches/mango/Mango/Mango/src/mango/worker/workFlow/coreTechniques/sym/InequationSym.java branches/mango/Mango/Mango/src/mango/worker/workFlow/coreTechniques/trap/ApplyLinearTrap.java branches/mango/Mango/Mango/src/mango/worker/workFlow/coreTechniques/trap/CellUpdateTrap.java branches/mango/Mango/Mango/src/mango/worker/workFlow/coreTechniques/trap/GarbageCollectTrap.java branches/mango/Mango/Mango/src/mango/worker/workFlow/coreTechniques/trap/RewriteTrap.java branches/mango/Mango/Mango/src/mango/worker/workFlow/form/model/FrameModel.java branches/mango/Mango/Mango/src/mango/worker/workFlow/form/model/HeapItemModel.java branches/mango/Mango/Mango/src/mango/worker/workFlow/form/model/HeapModel.java branches/mango/Mango/Mango/src/mango/worker/workFlow/form/model/HeapObjectModel.java branches/mango/Mango/Mango/src/mango/worker/workFlow/form/model/LocalArrayModel.java branches/mango/Mango/Mango/src/mango/worker/workFlow/form/model/LocalItemModel.java branches/mango/Mango/Mango/src/mango/worker/workFlow/form/model/OpItemModel.java branches/mango/Mango/Mango/src/mango/worker/workFlow/form/model/OperandStackModel.java branches/mango/Mango/Mango/src/mango/worker/workFlow/form/model/StackModel.java branches/mango/Mango/Mango/src/mango/worker/workFlow/form/model/StatModel.java branches/mango/Mango/Mango/src/mango/worker/workFlow/form/sym/binder/BinderSym.java branches/mango/Mango/Mango/src/mango/worker/workFlow/form/sym/binder/ContextBinderSym.java branches/mango/Mango/Mango/src/mango/worker/workFlow/form/sym/binder/executable/FrameSym.java branches/mango/Mango/Mango/src/mango/worker/workFlow/form/sym/binder/executable/HeapSym.java branches/mango/Mango/Mango/src/mango/worker/workFlow/form/sym/binder/executable/LocalVarSym.java branches/mango/Mango/Mango/src/mango/worker/workFlow/form/sym/binder/executable/StatSym.java branches/mango/Mango/Mango/src/mango/worker/workFlow/form/sym/binder/revealed/LocalSym.java branches/mango/Mango/Mango/src/mango/worker/workFlow/functionSpace/agent/EvaluatePredicateAgent.java branches/mango/Mango/Mango/src/mango/worker/workFlow/functionSpace/agent/StabilizeParameterAgent.java branches/mango/Mango/Mango/src/mango/worker/workFlow/functionSpace/sym/FunctionSym.java branches/mango/Mango/Mango/src/mango/worker/workFlow/functionSpace/sym/ModuleHypothesisSym.java branches/mango/Mango/Mango/src/mango/worker/workFlow/functionSpace/sym/ModuleInvocationSym.java branches/mango/Mango/Mango/src/mango/worker/workFlow/functionSpace/sym/UserInvocationSym.java branches/mango/Mango/Mango/src/mango/worker/workFlow/invariant/agent/BaseInvariantAgent.java branches/mango/Mango/Mango/src/mango/worker/workFlow/invariant/agent/ConditionalInvariantTestAgent.java branches/mango/Mango/Mango/src/mango/worker/workFlow/invariant/agent/ConditionalMethodTestAgent.java branches/mango/Mango/Mango/src/mango/worker/workFlow/invariant/agent/InvariantFactorizationAgent.java branches/mango/Mango/Mango/src/mango/worker/workFlow/invariant/agent/InvariantHypoAgent.java branches/mango/Mango/Mango/src/mango/worker/workFlow/invariant/agent/InvariantTestAgent.java branches/mango/Mango/Mango/src/mango/worker/workFlow/invariant/agent/MethodInvariantTestAgent.java branches/mango/Mango/Mango/src/mango/worker/workFlow/invariant/model/FactorizationModel.java branches/mango/Mango/Mango/src/mango/worker/workFlow/invariant/model/InvariantModel.java branches/mango/Mango/Mango/src/mango/worker/workFlow/model/EventLoopCmd.java branches/mango/Mango/Mango/src/mango/worker/workFlow/model/EventLoopTrap.java branches/mango/Mango/Mango/src/mango/worker/workFlow/model/HitemUtil.java branches/mango/Mango/Mango/src/mango/worker/workFlow/model/WorkFlowUtil.java branches/mango/Mango/Mango/src/mango/worker/workFlow/msg/AckCommand.java branches/mango/Mango/Mango/src/mango/worker/workFlow/msg/AddActiveObjectMsg.java branches/mango/Mango/Mango/src/mango/worker/workFlow/msg/ClearStatisticsRequestMsg.java branches/mango/Mango/Mango/src/mango/worker/workFlow/msg/DestroyActiveObjectMsg.java branches/mango/Mango/Mango/src/mango/worker/workFlow/msg/EnforceTierSettingsRequestMsg.java branches/mango/Mango/Mango/src/mango/worker/workFlow/msg/InitSessionMsg.java branches/mango/Mango/Mango/src/mango/worker/workFlow/msg/NameChangeActiveObjectMsg.java branches/mango/Mango/Mango/src/mango/worker/workFlow/msg/RedoLocatorMsg.java branches/mango/Mango/Mango/src/mango/worker/workFlow/msg/RedoRequestMsg.java branches/mango/Mango/Mango/src/mango/worker/workFlow/msg/ReplaceRequestMsg.java branches/mango/Mango/Mango/src/mango/worker/workFlow/msg/ReplaceRewriteLocatorMsg.java branches/mango/Mango/Mango/src/mango/worker/workFlow/msg/ReplaceRewriteRequestMsg.java branches/mango/Mango/Mango/src/mango/worker/workFlow/msg/ScheduleRequestMsg.java branches/mango/Mango/Mango/src/mango/worker/workFlow/msg/SetActiveCoreMangoObjectMsg.java branches/mango/Mango/Mango/src/mango/worker/workFlow/msg/ShowTypeRequestMsg.java branches/mango/Mango/Mango/src/mango/worker/workFlow/msg/TrapCommand.java branches/mango/Mango/Mango/src/mango/worker/workFlow/msg/UpdateStatisticsRequestMsg.java branches/mango/Mango/Mango/src/mango/worker/workFlow/translate/agent/AutoAssumeEquivalenceAgent.java branches/mango/Mango/Mango/src/mango/worker/workFlow/translate/trap/ScriptedTranslateTrap.java branches/mango/Mango/Mango/src/mango/worker/workFlow/translate/trap/ScriptedTrapConnector.java branches/mango/Mango/ThreadSupport/src/threadTest/ParentCommand.java branches/mango/Mango/ThreadSupport/src/threadTest/ScriptTest.java branches/mango/Mango/ThreadSupport/src/threadTest/script/ScriptRunAction.java branches/mango/Mango/ThreadSupport/src/threadTest/script/ScriptWindow.java branches/mango/Mango/javapathfinder-mango-bridge/mango/FormalTypes.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/BranchChoiceGenerator.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/Invocation.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/MangoClassPeer.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/MangoFieldPeer.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/MangoInvokeInstruction.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/MangoMethodPeer.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/ARETURN.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROW.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/DRETURN.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/FRETURN.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/GOTO.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/GOTO_W.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEINTERFACE.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKESTATIC.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKETARGET.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEVIRTUAL.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/IRETURN.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/JSR.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/JSR_W.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/LDC.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/LRETURN.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/NEWARRAY.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/RET.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/RETURN.java branches/mango/Mango/src/mango/intro/ApplicationWorkbenchAdvisor.java branches/mango/Mango/src/mango/intro/ApplicationWorkbenchWindowAdvisor.java branches/mango/Mango/src/mango/intro/LoginDialog.java branches/mango/Mango/src/mango/views/GenSpecWindow.java branches/mango/Mango/src/mango/views/GlobalViewWindow.java branches/mango/Mango/src/mango/views/LogWindow.java branches/mango/Mango/src/mango/views/MangoScriptWindow.java Added Paths: ----------- branches/mango/Mango/Mango/src/mango/ruleRequirement/typing/ClassObjectReq.java branches/mango/Mango/Mango/src/mango/worker/engine/sym/ClassObjectSym.java branches/mango/Mango/Mango/src/mango/worker/workFlow/coreTechniques/trap/MapToScopeTrap.java Removed Paths: ------------- branches/mango/Mango/Mango/src/mango/module/trap/MapToScopeTrap.java branches/mango/Mango/Mango/src/mango/worker/utilities/Util.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/sym/JclassSym.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/sym/JfieldSym.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/sym/JmethodSym.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/sym/JnonclassSym.java This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <fra...@us...> - 2009-08-21 21:29:58
|
Revision: 1848 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1848&view=rev Author: frankrimlinger Date: 2009-08-21 21:29:49 +0000 (Fri, 21 Aug 2009) Log Message: ----------- Eliminated assignmentCompatible utility that was used by AASTORE, because it is exactly the same as checkcast. Rewrote AASTORE accordingly. All coreRewriter.classModel actions are now JclassSym free. TODO: eliminate JclassSym altogether. Modified Paths: -------------- branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/IsPrimitiveClass.java branches/mango/Mango/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashMangoModel.java branches/mango/Mango/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashRewriter.java branches/mango/Mango/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/ReturnInstruction.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/AALOAD.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/AASTORE.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/ANEWARRAY.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/ARRAYLENGTH.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROWCREATOR.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/BALOAD.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/BASTORE.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/CALOAD.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/CASTORE.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/DALOAD.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/DASTORE.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/FALOAD.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/FASTORE.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/GETFIELD.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/IALOAD.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/IASTORE.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/IDIV.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/IFEQ.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/IFGE.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/IFGT.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/IFLE.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/IFLT.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/IFNE.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/IFNONNULL.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/IFNULL.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ACMPEQ.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ACMPNE.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ICMPEQ.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ICMPGE.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ICMPGT.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ICMPLE.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ICMPLT.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ICMPNE.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/IREM.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/LALOAD.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/LASTORE.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/LDIV.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/LOOKUPSWITCH.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/LREM.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/MULTIANEWARRAY.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/NEWARRAY.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/PUTFIELD.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/RET.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/SALOAD.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/SASTORE.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/TABLESWITCH.java branches/mango/Mango/mangoUserHome/frank/rules/rulebase.zip Removed Paths: ------------- branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/IsAssignmentCompatible.java branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/IsInterface.java This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <fra...@us...> - 2009-08-21 19:36:06
|
Revision: 1847 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1847&view=rev Author: frankrimlinger Date: 2009-08-21 19:35:54 +0000 (Fri, 21 Aug 2009) Log Message: ----------- Changes to checkcast and instanceof broke equals() and compareTo() specs in String_MangoFormal. Rebuilt the broken specs, which revealed a lot of interesting issues. Discovered fun fact about interface templates. Suppose you have the following class public class I implements Comparable<I>{ @Override public int compareTo(I o) { // TODO Auto-generated method stub return 0; } } Then the compiler generates the following, as expected: Method: MethodInfo[I.compareTo(LI;)I] instructions: iconst_0 ireturn I.compareTo(LI;)I BUT, you also get the following, FREE OF CHARGE Method: MethodInfo[I.compareTo(Ljava/lang/Object;)I] instructions: aload_0 aload_1 checkcast invokevirtual I.compareTo(LI;)I ireturn I.compareTo(Ljava/lang/Object;)I Similar code kept appearing during clean up of specification of String_MangoFormal class. This was really really puzzling, as the code just seemed to appear out of nowhere by magic. This is in fact the case, but not to worry. Its just compiler glue to help templates ease their way into the java world. Here is the specification generated by Mango for this glue: Hypothesis: compareTo_LocalVar_at_offset_1_lineNumber_1 is undefined Close Case: Returns int: 0. Hypothesis: compareTo_LocalVar_at_offset_1_lineNumber_1 is defined Hypothesis: Class name of compareTo_LocalVar_at_offset_1_lineNumber_1 may be cast to I Close Case: Returns int: 0. Hypothesis: compareTo_LocalVar_at_offset_1_lineNumber_1 is defined Hypothesis: Class name of compareTo_LocalVar_at_offset_1_lineNumber_1 may not be cast to I Close Case: Throws: java.lang.ClassCastException. The spec is not pretty because there is no source code for this method. I bring this up because you can ask following question, is this spec "wrong"? A wrong answer is, "yes, because the second case is brain-dead." And the correct answer is, "the question is meaningless since it depends on the incorrect method I.compareTo(LI;)I." The point is that specification errors propagate upwards until at last somebody spots an inconsistency. This is one of the great strengths of the mango method. Actually, case 1 is also brain-dead. For what its worth, executing "this".compareTo(null); throws NullPointerException, but you would never know it from reading the java doc for the Comparable interface. Mango is also very good at exposing all the boring cases. Modified Paths: -------------- branches/mango/Mango/Mango/src/mango/worker/Mango.java branches/mango/Mango/Mango/src/mango/worker/Worker.java branches/mango/Mango/Mango/src/mango/worker/utilities/MutableHitem.java branches/mango/Mango/Mango/src/mango/worker/utilities/MutableSet.java branches/mango/Mango/Mango/src/mango/worker/workFlow/form/model/HeapItemModel.java branches/mango/Mango/Mango/src/mango/worker/workFlow/form/model/HeapObjectModel.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROWCREATOR.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKECLINIT.java branches/mango/Mango/mangoUserHome/frank/rules/rulebase.zip branches/mango/Mango/mangoUserHome/system/System/java/lang/String_MangoFormal.java branches/mango/Mango/mangoUserHome/system/SystemTests/src/I.java Added Paths: ----------- branches/mango/Mango/mangoUserHome/frank/sessions/I/compareTo(LI;)I/ branches/mango/Mango/mangoUserHome/frank/sessions/I/compareTo(LI;)I/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/I/compareTo(Ljava.lang.Object_MangoFormal;)I/ branches/mango/Mango/mangoUserHome/frank/sessions/I/compareTo(Ljava.lang.Object_MangoFormal;)I/Class name of compareTo_LocalVar_at_offset_1_lineNumber_1 may be cast to I.zip branches/mango/Mango/mangoUserHome/frank/sessions/I/compareTo(Ljava.lang.Object_MangoFormal;)I/Class name of compareTo_LocalVar_at_offset_1_lineNumber_1 may not be cast to I.zip branches/mango/Mango/mangoUserHome/frank/sessions/I/compareTo(Ljava.lang.Object_MangoFormal;)I/compareTo_LocalVar_at_offset_1_lineNumber_1 is undefined.zip branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/compareTo(Ljava.lang.Object_MangoFormal;)I/Class name of compareTo_LocalVar_at_offset_1_lineNumber_1 may be cast to java.lang.String_MangoFormal.zip branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/compareTo(Ljava.lang.Object_MangoFormal;)I/Class name of compareTo_LocalVar_at_offset_1_lineNumber_1 may not be cast to java.lang.String_MangoFormal.zip branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/compareTo(Ljava.lang.Object_MangoFormal;)I/compareTo_LocalVar_at_offset_1_lineNumber_1 is undefined.zip branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/equals(Ljava.lang.Object_MangoFormal;)Z/Class name of anObject may not be cast to java.lang.String_MangoFormal.zip branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/equals(Ljava.lang.Object_MangoFormal;)Z/String objects _this.value_ and _anObject.value_ are lexicographically equivalent.zip branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/equals(Ljava.lang.Object_MangoFormal;)Z/String objects _this.value_ and _anObject.value_ are lexicographically inequivalent.zip branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/equals(Ljava.lang.Object_MangoFormal;)Z/anObject is undefined.zip Removed Paths: ------------- branches/mango/Mango/mangoUserHome/frank/sessions/a.zip branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/compareTo(Ljava.lang.Object_MangoFormal;)I/'x' is an instance of Class java.lang.String_MangoFormal.zip branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/compareTo(Ljava.lang.Object_MangoFormal;)I/'x' is not an instance of Class java.lang.String_MangoFormal.zip branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/equals(Ljava.lang.Object_MangoFormal;)Z/'anObject' equals null reference.zip branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/equals(Ljava.lang.Object_MangoFormal;)Z/'anObject' is not an instance of Class java.lang.String_MangoFormal.zip branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/equals(Ljava.lang.Object_MangoFormal;)Z/String objects _'this'.value_ and _'anObject'.value_ are lexicographically equivalent.zip branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/equals(Ljava.lang.Object_MangoFormal;)Z/String objects _'this'.value_ and _'anObject'.value_ are lexicographically inequivalent.zip This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <fra...@us...> - 2009-08-21 15:59:47
|
Revision: 1846 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1846&view=rev Author: frankrimlinger Date: 2009-08-21 15:59:32 +0000 (Fri, 21 Aug 2009) Log Message: ----------- The instanceof utility is now obsolete. As null cases are handled separately now anyway, we can use the checkcast utility. To get return value, we wrap the checkcast expression using the new pred2bool utility of type boolean. This relieves a lot of predicate-versus-boolean anxiety for the user. Moreover, we get to introduce the wonderful rule (= (pred2bool x) 0 ) --> (not x) which causes pred2bool to evaporate when forming hypotheses. It only shows up in value expressions, where it can just be dropped on translation. Lesson learned: Initially thought to introduce pred2bool as a formal type, with <pred2bool> -> boolean. But now boolean is no longer minimal, which fouls the rewriter. So, don't go "type happy". Not everything needs to be a type. If timing is not an issue, in that the rewriter has a chance to brand a kons with its type before it needs to know the type, then use a utility rulekey instead. There are probably a few types out there that should be demoted to utilities already. Modified Paths: -------------- branches/mango/Mango/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashOpcodeSyms.java branches/mango/Mango/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashTyping.java branches/mango/Mango/Mango/src/mango/worker/engine/rule/Rule.java branches/mango/Mango/Mango/src/mango/worker/engine/rule/Tier.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/CHECKCAST.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/INSTANCEOF.java branches/mango/Mango/mangoUserHome/frank/rules/rulebase.zip Removed Paths: ------------- branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/Instanceof.java branches/mango/Mango/mangoUserHome/frank/bin/ branches/mango/Mango/mangoUserHome/marc/bin/ branches/mango/Mango/mangoUserHome/rkrug/bin/ branches/mango/Mango/mangoUserHome/system/bin/ This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <fra...@us...> - 2009-08-21 15:50:18
|
Revision: 1845 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1845&view=rev Author: frankrimlinger Date: 2009-08-21 15:50:11 +0000 (Fri, 21 Aug 2009) Log Message: ----------- Fixed declaration. Modified Paths: -------------- branches/mango/Mango/mangoUserHome/system/System/java/lang/String_MangoFormal.java This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <fra...@us...> - 2009-08-21 03:59:00
|
Revision: 1844 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1844&view=rev Author: frankrimlinger Date: 2009-08-21 03:58:54 +0000 (Fri, 21 Aug 2009) Log Message: ----------- Completed checkcast rehab, precisely implementing Jvm2ed checkcast semantics. TODO instanceof rehab just like checkcast isAssignableFrom With the much more precise understanding of types, JclassSym really needs to be weeded out entirely. Modified Paths: -------------- branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/Checkcast.java branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/GetInterfaceRunTimeException.java branches/mango/Mango/Mango/src/mango/worker/Worker.java branches/mango/Mango/javapathfinder-mango-bridge/mango/FormalTypes.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/MangoClassPeer.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/CHECKCAST.java branches/mango/Mango/mangoUserHome/frank/rules/rulebase.zip Added Paths: ----------- branches/mango/Mango/mangoUserHome/system/SystemTests/src/Casting.java This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <fra...@us...> - 2009-08-20 22:49:37
|
Revision: 1843 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1843&view=rev Author: frankrimlinger Date: 2009-08-20 22:49:31 +0000 (Thu, 20 Aug 2009) Log Message: ----------- checkcast rehab in progress. Requires the "mango theory of types". jpf likes to deliver "canonical type" in instructions like checkcast. The issue for mango is, does canonical type contain all the information required to translate to "source code level format". And the answer is yes. The algorithm is simple. Say x is in canonical type. If x does not contain "[", then x is source code level. If x does contain "[", then Types.getTypeName(x) will be source code level. End of story. Examples: int --> int I --> I [I --> int[] [LI; --> I[] At the source code level, the names of types, classes, and arrays all blur together in a uniform syntax identifier[] ...[] where the bracket(s) are optional. Strings satisfying this syntax are referred by mango as "class names". We stretch the identifier concept to allow for <xxx>. This allows <init>, <clinit>, and the mango formal types to join the club. So questions like, given a class name x, is x primitive?, is x an array?, is x a non-array class?, is x mango formal? are all meaningful and can be answered deterministically by parsing the name. This unravels the mystery connection between "int" and "java.lang.Integer.TYPE". These are different class names, one representing a primitive java type, and one representing a non-array class. We definitely DO NOT use mango class names to directly represent field descriptors (JVM2ed 4.3.2). The reason is that field descriptors for Object type and Array type do not even satisfy the syntax of mango class name. Worse, the field descriptor "I" has the semantics of the class name "int", NOT the class name "I". And most horribly, field descriptors use "internal form", i.e., "/" instead of "." Ditto for method descriptors. Nevertheless, all descriptors have a natural translation I --> int LI; --> I V --> void and so on. So, canonical type is a good thing, but we stick with source code level "class names", because they faithfully represent all the semantics, and are pleasing to the eye. Moreover, the mango theory of types may be admitted to ACL2, and allows us to distinguish all the exotica placed in the heap, using class names in the subaddress of a location. This is critical for garbage collection. Modified Paths: -------------- branches/mango/Mango/Mango/src/mango/worker/Worker.java branches/mango/Mango/javapathfinder-mango-bridge/mango/FormalTypes.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/CHECKCAST.java This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <fra...@us...> - 2009-08-20 04:16:00
|
Revision: 1842 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1842&view=rev Author: frankrimlinger Date: 2009-08-20 04:15:54 +0000 (Thu, 20 Aug 2009) Log Message: ----------- Complete rewrite of accessibility code and get virtual and interface method and exception. NEXT: revamp checkcast, starting with formal bytecode. You want first to set up the instruction to access the className from the heap. This allows the heap to get garbage collected in the standard way. Also, jpf gives you "canonical type", which must be converted to a ClassInfo. You know you can do this because the JVM spec says we have "a class, array, or interface". All bytecodes involving a heap access to get a class name or whatever need to be set up in this manner, as this vastly simplifies garbage collection. Modified Paths: -------------- branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/GetInterfaceRunTimeException.java branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/GetInterfaceRunTimeMethod.java branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/GetVirtualRunTimeException.java branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/GetVirtualRunTimeMethod.java branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/IsSuperClass.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/Invocation.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/MangoClassPeer.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/MangoFieldPeer.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/MangoMethodPeer.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/CHECKCAST.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEINTERFACE.java branches/mango/Mango/mangoUserHome/frank/rules/rulebase.zip This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <fra...@us...> - 2009-08-19 21:24:47
|
Revision: 1841 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1841&view=rev Author: frankrimlinger Date: 2009-08-19 21:24:40 +0000 (Wed, 19 Aug 2009) Log Message: ----------- The following methods of MethodInfo dealing with the signature now have formal counterparts to munge the signature. As long as nobody accesses the signature directly, we should be good-2-go. The new methods are all in MangoMethodPeer String getCompleteName () --> getFormalCompleteName String getFullName () --> getFormalFullName String getReturnTypeName () --> getFormalReturnTypeName String getSignature () --> getFormalSignature public String getUniqueName () --> getFormalUniqueName Routed all code dealing with formal execution through the new methods. As far as "Instruction.getInstructionName" mentioned in 1840, there is no such method. This is actually part of the MangoInterface, so what happens is that implementations used the above methods and so were re-routed accordingly. With this in place, decided to take the hit now and eliminate JclassSym. This is an artifact from C++ that is now increasingly difficult to support. As methods are deleted from JclassSym, broken dependents are hollowed out, and the code rewritten using ClassInfo and MangoFormalClass methods. Finish writing new accessibility methods in MangoClassPeer, which consult bcel as needed. Then wire up the broken actions. Modified Paths: -------------- branches/mango/Mango/Mango/src/mango/graph/data/supervertex/SuperVertexData.java branches/mango/Mango/Mango/src/mango/graph/data/ucon/UconData.java branches/mango/Mango/Mango/src/mango/module/definition/loop/LoopDefinitionManager.java branches/mango/Mango/Mango/src/mango/module/definition/method/MethodDefinitionManager.java branches/mango/Mango/Mango/src/mango/module/definition/method/msg/CreateMethodStubMsg.java branches/mango/Mango/Mango/src/mango/module/definition/method/msg/MethodDefinitionLocatorMsg.java branches/mango/Mango/Mango/src/mango/module/definition/model/DefinitionManager.java branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/Checkcast.java branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/GetInterfaceRunTimeException.java branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/GetInterfaceRunTimeMethod.java branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/GetVirtualRunTimeException.java branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/GetVirtualRunTimeMethod.java branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/Instanceof.java branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/IsAssignmentCompatible.java branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/IsSuperClass.java branches/mango/Mango/Mango/src/mango/worker/WorkerControl.java branches/mango/Mango/Mango/src/mango/worker/engine/rule/AssumeEquivRule.java branches/mango/Mango/Mango/src/mango/worker/engine/sym/Sym.java branches/mango/Mango/Mango/src/mango/worker/mangoModel/BackupAlg.java branches/mango/Mango/Mango/src/mango/worker/mangoModel/graph/LoopGraph.java branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/graphic/MethodSym.java branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/graphic/SuperVertexClassSym.java branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/superVertex/SuperCpnSym.java branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/ucon/MethodEntrySym.java branches/mango/Mango/Mango/src/mango/worker/workFlow/model/HitemUtil.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/Invocation.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/MangoClassPeer.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/MangoInstruction.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/MangoInvokeInstruction.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/MangoMethodPeer.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROWHANDLER.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKECLINIT.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/sym/JclassSym.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/sym/JmethodSym.java branches/mango/Mango/mangoUserHome/frank/rules/rulebase.zip branches/mango/Mango/mangoUserHome/frank/sessions/baseline/itsAWrap/<init>()V/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/baseline/itsAWrap/clear([I)V/Array length of x is greater than or equal to 10.zip branches/mango/Mango/mangoUserHome/frank/sessions/baseline/itsAWrap/clear([I)V/loops/-baseline.itsAWrap.clear([I)V#8- dload_i_Code_01/op0 is less than 10.zip branches/mango/Mango/mangoUserHome/frank/sessions/baseline/itsAWrap/main([I)Z/x[5] equals x[6].zip branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/forName(Ljava.lang.String_MangoFormal;)Ljava.lang.Class_MangoFormal;/className is defined.zip branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/forName(Ljava.lang.String_MangoFormal;)Ljava.lang.Class_MangoFormal;/className is undefined.zip branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/getComponentType()Ljava.lang.Class_MangoFormal;/Class name of this is an array.zip branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/getComponentType()Ljava.lang.Class_MangoFormal;/Class name of this is not a loadable class.zip branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/isAssignableFrom(Ljava.lang.Class_MangoFormal;)Z/cls is defined.zip branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/isAssignableFrom(Ljava.lang.Class_MangoFormal;)Z/cls is undefined.zip Added Paths: ----------- branches/mango/Mango/mangoUserHome/frank/sessions/I/ branches/mango/Mango/mangoUserHome/frank/sessions/I/<init>()V/ branches/mango/Mango/mangoUserHome/frank/sessions/I/<init>()V/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/I/whatHappens()Ljava.lang.Class_MangoFormal;/ branches/mango/Mango/mangoUserHome/frank/sessions/I/whatHappens()Ljava.lang.Class_MangoFormal;/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/I/whatHappens1()Ljava.lang.Class_MangoFormal;/ branches/mango/Mango/mangoUserHome/frank/sessions/I/whatHappens1()Ljava.lang.Class_MangoFormal;/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/I/whatHappens2()Ljava.lang.Class_MangoFormal;/ branches/mango/Mango/mangoUserHome/frank/sessions/I/whatHappens2()Ljava.lang.Class_MangoFormal;/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/I/whatHappens3()Ljava.lang.Class_MangoFormal;/ branches/mango/Mango/mangoUserHome/frank/sessions/I/whatHappens3()Ljava.lang.Class_MangoFormal;/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/<init>()V/ branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/<init>()V/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/compatibleFalse()Z/ branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/compatibleFalse()Z/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/compatibleTrue()Z/ branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getComponentType()Ljava.lang.Class_MangoFormal;/ branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getComponentType()Ljava.lang.Class_MangoFormal;/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getComponentType2()Ljava.lang.Class_MangoFormal;/ branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getComponentType2()Ljava.lang.Class_MangoFormal;/case.zip branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getName()Ljava.lang.String_MangoFormal;/ branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getName()Ljava.lang.String_MangoFormal;/case.zip Removed Paths: ------------- branches/mango/Mango/Mango/src/mango/worker/mangoModel/agent/CheckCast_getValueAgent.java branches/mango/Mango/Mango/src/mango/worker/mangoModel/agent/InstanceOfAgent.java branches/mango/Mango/Mango/src/mango/worker/mangoModel/agent/IsAssignmentCompatibleAgent.java branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getComponentType()Ljava.lang.Class;/ branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getComponentType2()Ljava.lang.Class;/ branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getName()Ljava.lang.String;/case.zip This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <fra...@us...> - 2009-08-19 04:45:23
|
Revision: 1840 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1840&view=rev Author: frankrimlinger Date: 2009-08-19 04:45:17 +0000 (Wed, 19 Aug 2009) Log Message: ----------- Punched in MangoFieldPeer per 1839. However, what else is out there? Who knows all the subtle places where the compiler generates instructions with literal class names? To mitigate, all calls to gov.nasa.jpf.jvm.bytecode.Instruction.getMethodInfo() from within buildFormaPeer() methods are now piped through MangoMethodPeer.getFormalPeer(). Undoubtedly, there are still other leaks to plug, but we must catch them as we may. To help avoid contamination of nominal jpf execution, we introduce MangoInterface.getFormalMethodInfo(), implemented within MangoInstruction and MangoInvokeInstruction. Since all formal bytecode classes extend from these points, changed getMethodInfo() to getFormalMethodInfo() as appropriate NEXT BUG: More leaks: MethodInfo.getFullName, getDescriptor, etc. All of these need to have the signature munged. Instruction.getInstructionName ditto The reason this is a problem is like so, you have a class X that does not have a formal counterpart. So Mango must model X. But then you have a method y in X like so String y(){} so the MethodInfo is for X.y()Ljava.lang.String; and you don't automatically get munged signatures. This happens automatically if the class is munged, but if not, you have to run the ball out on the ground. Modified Paths: -------------- branches/mango/Mango/Mango/src/mango/graph/data/ucon/UconData.java branches/mango/Mango/Mango/src/mango/module/definition/loop/LoopDefinitionManager.java branches/mango/Mango/Mango/src/mango/module/instance/loop/model/LoopInstanceManager.java branches/mango/Mango/Mango/src/mango/worker/mangoModel/BackupAlg.java branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/graphic/MethodSym.java branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/ucon/MethodEntrySym.java branches/mango/Mango/Mango/src/mango/worker/mangoModel/vertex/CpnVertex.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/Invocation.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/MangoClassPeer.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/MangoFormalInterface.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/MangoInstruction.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/MangoInvokeInstruction.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/MangoMethodPeer.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/ACATCHHANDLER.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROW.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROWCREATOR.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROWHANDLER.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/GETFIELD.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/GETSTATIC.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKECLINIT.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKESTATIC.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/NEW.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/PUTFIELD.java branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/PUTSTATIC.java Added Paths: ----------- branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/MangoFieldPeer.java This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |