Menu
▾
▴
javapathfinder-svn
|
From: <fra...@us...> - 2009-06-10 15:13:23
|
Revision: 1607
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1607&view=rev
Author: frankrimlinger
Date: 2009-06-10 15:13:17 +0000 (Wed, 10 Jun 2009)
Log Message:
-----------
Auto reset now works hot when the definition window is closed if the auto reset preference is set. This involved some delicate negotiation to avoid deadlock. But what is really cool is that running a session will close the definition window, which kicks the auto-reset, which creates a new rulebase worker image and fires up jpf, which gets all the way to the INVOKETARGET bug. Thus with just a roster of session names, regression testing can be automated using the existing auto threads. So all the old rmi database stuff can be disposed of.
In other news, there is a crash when you alter preferences in the login window. It is actually a race condition, sometimes resulting in access of inconsistent preference state (it can't be duplicated if you step through with debugger- a fun bug). The workaround is just turn on auto-login from the preference panel after you make your change. Then start again after crash and all-is-well. Clearly this should be fixed someday, or hopefully this bug will go away in a future RCP update.
At this point, we should honor the auto-save preference, saving both rulebase and session (if dirty) when auto reset kicks. The rulebase save must block, to avoid issues, so make it its own PermCommand on the auto thread.
Since the session save is much faster than the rulebase, and more important, probably want two separate preferences here.
Finally, fix the INVOKETARGET bug and start some serious testing.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/control/action/control/StopWorkerAction.java
branches/mango/MangoJPF/Mango/src/mango/control/action/control/WorkerAction.java
branches/mango/MangoJPF/Mango/src/mango/module/definition/msg/CoalesceStandingHypothesesMsg.java
branches/mango/MangoJPF/Mango/src/mango/worker/Worker.java
branches/mango/MangoJPF/Mango/src/mango/worker/msg/NewWorkerMsg.java
branches/mango/MangoJPF/ThreadSupport/src/threadModel/CommandState.java
branches/mango/MangoJPF/ThreadSupport/src/threadModel/SystemBuilder.java
Added Paths:
-----------
branches/mango/MangoJPF/Mango/src/mango/worker/msg/AutoResetMsg.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-06-10 17:01:58
|
Revision: 1608
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1608&view=rev
Author: frankrimlinger
Date: 2009-06-10 17:01:44 +0000 (Wed, 10 Jun 2009)
Log Message:
-----------
Auto rulebase save after the session closes is now working, and the jpf scan completes. However, jpf didn't visit all the places it was supposed to, which causes a crash in phase1. Probably there is some stale data controlling backtracking that needs to be reinitialized prior to the scan.
Need to have ObjectDirtinessManager keep track of the script, and split the auto save preference into two different preferences. There is significant latency, about 5 or ten seconds, to save the rulebase, so may want to opt out.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/core/CoreMangoObject.java
branches/mango/MangoJPF/Mango/src/mango/core/gui/action/SaveCoreRuleBaseAction.java
branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java
branches/mango/MangoJPF/Mango/src/mango/worker/msg/RulebaseMsg.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ClassUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MethodUtil.java
branches/mango/MangoJPF/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-06-11 04:15:10
|
Revision: 1612
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1612&view=rev
Author: frankrimlinger
Date: 2009-06-11 04:14:05 +0000 (Thu, 11 Jun 2009)
Log Message:
-----------
Converted script file dialogs to SWT, which has very nice native look-and-feel. Got auto-save of scripts working properly, so now the automation of session tear down and start up is complete. Regression testing will now be much more pleasant and full automation of regression testing is easily within reach. But for now, just want to regenerate all the existing baseline sessions.
So, back to the rewriting bug. Why doesn't ItsAWrap.clear work? Just compare Mango versus MangoJPF to figure this out. Something is slightly wrong here.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/core/gui/action/SaveCoreRuleBaseAction.java
branches/mango/MangoJPF/Mango/src/mango/script/gui/action/ScriptSaveAction.java
branches/mango/MangoJPF/Mango/src/mango/worker/msg/SaveScriptMsg.java
branches/mango/MangoJPF/mangoUserHome/frank/rules/rulebase.zip
branches/mango/MangoJPF/mangoUserHome/frank/sessions/baseline/itsAWrap/clear([I)V/loops/-baseline.itsAWrap.clear([I)V#8:iload_1_Code_01/op0 is less than 10.zip
Added Paths:
-----------
branches/mango/MangoJPF/Mango/src/mango/worker/PayloadRunnable.java
Removed Paths:
-------------
branches/mango/MangoJPF/mangoUserHome/frank/sessions/a.zip
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-06-12 19:20:26
|
Revision: 1618
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1618&view=rev
Author: frankrimlinger
Date: 2009-06-12 19:19:55 +0000 (Fri, 12 Jun 2009)
Log Message:
-----------
Added dirty session save to quit handler.
Wired in the new HasCommutingClinit rule to the corresponding action to fix rewriting problem in ItsAWrap.main(). But this only works because ItsAWrap does not trigger any clinit invocation. To handle the problem more generally, introduced preference to suppress clinit invocation. This in itself does not cause unsoundness. What is unsound is to introduce rules to resolve references to non-final static fields in an ad-hoc manner. When this issue comes up, we can turn off the preference and implement the rest of the new clinit mechanism.
Specifically, the rule HasCommutingClinit just returns (dualp 'f) if the "Suppress clinit invocation" preference is on. For now, we leave this turned off.
Next bug, ItsAWrap.main thinks x[5] and x[6] are loop invariant. Technically, this is true, but shouldn't be able to know this. YIKES!
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/ruleAction/coreRewriter/clinit/HasCommutingClinit.java
branches/mango/MangoJPF/Mango/src/mango/script/model/MangoScriptModel.java
branches/mango/MangoJPF/Mango/src/mango/worker/Worker.java
branches/mango/MangoJPF/mangoUserHome/frank/rules/rulebase.zip
branches/mango/MangoJPF/src/mango/preferences/GeneralPreferencePage.java
Added Paths:
-----------
branches/mango/MangoJPF/mangoUserHome/frank/sessions/a.zip
Removed Paths:
-------------
branches/mango/MangoJPF/mangoUserHome/frank/sessions/baseline/a.zip
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-06-13 22:16:32
|
Revision: 1624
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1624&view=rev
Author: frankrimlinger
Date: 2009-06-13 22:15:54 +0000 (Sat, 13 Jun 2009)
Log Message:
-----------
Fixed two bugs: The "fake methods" bad method, abstraction ucon method, and OSmethod were not being modelled, and the routine hasMangoModel was returning false when passed these methods. This set in motion a sequence of events with the unhappy result that clear() never gets invoked by main(). The cause was again just the result of code that got shifted around during the port to MangoJPF.
With this fix, observed the correct stratification and component graph for itsAWrap.main.
Unfortunately, itsAWrap.main is still exhibiting the original problem, that is x[5] and x[6] are not functions of loop output heap. However, the loop output heap does appear as the itsAWrap.main output heap.
So, something else is going on here.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/BackupAlg.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/edge/Edge.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/Invocation.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MethodUtil.java
branches/mango/MangoJPF/mangoUserHome/frank/sessions/a.zip
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-06-15 12:03:01
|
Revision: 1627
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1627&view=rev
Author: frankrimlinger
Date: 2009-06-15 12:01:59 +0000 (Mon, 15 Jun 2009)
Log Message:
-----------
still working on invariant bug
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/functionSpace/sym/ModuleInvocationSym.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/invariant/agent/BaseInvariantAgent.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/invariant/agent/InvariantTestAgent.java
branches/mango/MangoJPF/mangoUserHome/frank/sessions/a.zip
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-06-17 14:35:04
|
Revision: 1637
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1637&view=rev
Author: frankrimlinger
Date: 2009-06-17 14:35:02 +0000 (Wed, 17 Jun 2009)
Log Message:
-----------
The idea that jpf was not loading exception tables is wrong. These tables only apply to checked exceptions thrown by a method, which is not the situation I am in. So the immediate problem of dropped exception branch conditions lies elsewhere. To address this whole issue more systematically, have reinstanted Marc's exception handler tests, which for the most part are taken from the old IBM jikes test suite.
Modified Paths:
--------------
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ExceptionHandlerUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MethodUtil.java
Added Paths:
-----------
branches/mango/MangoJPF/mangoUserHome/marc/
branches/mango/MangoJPF/mangoUserHome/marc/arrayCopyShell/
branches/mango/MangoJPF/mangoUserHome/marc/arrayCopyShell/src/
branches/mango/MangoJPF/mangoUserHome/marc/arrayCopyShell/src/arrayCopyShell.java
branches/mango/MangoJPF/mangoUserHome/marc/hypo2/
branches/mango/MangoJPF/mangoUserHome/marc/hypo2/src/
branches/mango/MangoJPF/mangoUserHome/marc/hypo2/src/hypo2.java
branches/mango/MangoJPF/mangoUserHome/marc/lptry1/
branches/mango/MangoJPF/mangoUserHome/marc/lptry1/lptry1.java
branches/mango/MangoJPF/mangoUserHome/marc/lptry2/
branches/mango/MangoJPF/mangoUserHome/marc/lptry2/src/
branches/mango/MangoJPF/mangoUserHome/marc/lptry2/src/lptry2.java
branches/mango/MangoJPF/mangoUserHome/marc/try1/
branches/mango/MangoJPF/mangoUserHome/marc/try1/try1.java
branches/mango/MangoJPF/mangoUserHome/marc/try2/
branches/mango/MangoJPF/mangoUserHome/marc/try2/try2.java
branches/mango/MangoJPF/mangoUserHome/marc/try3/
branches/mango/MangoJPF/mangoUserHome/marc/try3/try3.java
branches/mango/MangoJPF/mangoUserHome/marc/trychk1/
branches/mango/MangoJPF/mangoUserHome/marc/trychk1/trychk1.java
branches/mango/MangoJPF/mangoUserHome/marc/trychk2/
branches/mango/MangoJPF/mangoUserHome/marc/trychk2/trychk2.java
branches/mango/MangoJPF/mangoUserHome/marc/trychk3/
branches/mango/MangoJPF/mangoUserHome/marc/trychk3/trychk3.java
branches/mango/MangoJPF/mangoUserHome/marc/trychk6/
branches/mango/MangoJPF/mangoUserHome/marc/trychk6/trychk6.java
branches/mango/MangoJPF/mangoUserHome/marc/trychk7/
branches/mango/MangoJPF/mangoUserHome/marc/trychk7/trychk7.java
branches/mango/MangoJPF/mangoUserHome/marc/trychk8/
branches/mango/MangoJPF/mangoUserHome/marc/trychk8/trychk8.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-06-17 20:13:57
|
Revision: 1645
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1645&view=rev
Author: frankrimlinger
Date: 2009-06-17 20:13:54 +0000 (Wed, 17 Jun 2009)
Log Message:
-----------
Fixed dropped branch condition bug for Exception Handlers. This was actually an EZ bug. As exception handling now works correctly in the bread-and-butter case of no handlers, punting on Marc's stuff for now. Fixed source code display bugs. There are probably more of these out there. This subject requires mastery of
***Zen and the art of line numbers***
When Method.getLineNumber is passed an Instruction, it returns the source code line number of that instruction. When Instruction.getLineNumber is called, it returns the index of this instruction in the corresponding Instruction[] code array. This is also called the "position" by jpf. Mango uses the word "lineNumber" to refer to what a jpf instruction would call "pc" or "offset", and this is the offset into the jvm codeblock in the Code attribute of an instruction. For example, the following returns a source code line number of a mango lineNumber:
method.getLineNumber(method.getInstructionAt(lineNumber));
To simplify usage, the gem is encapsulated as
MethodUtil.getSourceCodeLineNumber(method,lineNumber)
Replayed all itsAWrap sessions successfully. Moving on to other baseline loop tests.
Modified Paths:
--------------
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ExceptionHandlerUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MethodUtil.java
branches/mango/MangoJPF/mangoUserHome/frank/rules/rulebase.zip
branches/mango/MangoJPF/mangoUserHome/frank/sessions/baseline/itsAWrap/clear([I)V/length of the Array 'x' is greater than or equal to 10.zip
branches/mango/MangoJPF/mangoUserHome/frank/sessions/baseline/itsAWrap/clear([I)V/loops/-baseline.itsAWrap.clear([I)V#8:iload_1_Code_01/op0 is less than 10.zip
branches/mango/MangoJPF/mangoUserHome/frank/sessions/baseline/itsAWrap/main([I)Z/length of the Array 'x' is greater than or equal to 10.zip
Removed Paths:
-------------
branches/mango/MangoJPF/mangoUserHome/frank/sessions/a.zip
branches/mango/MangoJPF/mangoUserHome/frank/sessions/baseline/itsAWrap/main([I)Z/a.zip
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-06-20 16:44:52
|
Revision: 1670
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1670&view=rev
Author: frankrimlinger
Date: 2009-06-20 16:44:51 +0000 (Sat, 20 Jun 2009)
Log Message:
-----------
Port of rulebase to correspond to the mangoUserHome/system port, except for some new native model rules required to support the Object versus Object_MangoFormal issue. These must be modelled "by hand".
Ported the mango native interface rules. Mostly just had to change signatures, but mango.lang.Mango_Class.forName actually puts an "java.lang.Class_MangoFormal" on the heap, and this literal is burned into the rule. Also, many instances of the "java.lang.String" changed to "java.lang.String_MangoFormal"
Deleted all the java package rules. These can be rebuilt using MangoJPF and should be anyway to get good sessions for replay.
Rulebase searches turned up numerous instances of "java.lang.Class" and "java.lang.String", for example, in the rulebase theory rules. These were all converted. Most of this stuff has to do with formal garbage collection.
Seach rulebase for references to all the other names requiring the _MangoFormal suffix. This turned up lots of support for the io package that I had forgotten about. This stuff probably still works.
The "specialHeapAddress" is still "Boolean", not "Boolean_MangoFormal". This device is only used to distinguish the static Boolean_MangoFormal objects representing true and false, and is not logically a class name.
So, with all this in place, can finally start MangoJPF code modifications to call ClassUtil.getFormalPeer and MangoUtil.getFormalPeer as appropriate.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/coreTechniques/model/HeapPointer.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ClassUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MethodUtil.java
branches/mango/MangoJPF/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-06-29 05:06:50
|
Revision: 1699
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1699&view=rev
Author: frankrimlinger
Date: 2009-06-29 05:06:49 +0000 (Mon, 29 Jun 2009)
Log Message:
-----------
Rewiring of MangoJPF to call ClassUtil.getFormalPeer and MethodUtil.getFormalPeer in progress. As expected, a number of subtle issues are involved. The ideal of aliasing the class names of System classes is ugly, and will stunt the growth of the formal system code. A much better solution would be to have a separate class loader for loading the formal system classes, so that the namespace collision problem goes away. However, jpf would have to be aware of this classloader as a critical requirement is that the formal system classes are also interpreted and processed at the jpf level. So for now just plow ahead with the stop-gap solution with a view to developing a precise feature request for jpf.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ClassUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/CodeSurvey.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/InvocationUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MethodUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEVIRTUAL.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-06-29 18:48:55
|
Revision: 1700
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1700&view=rev
Author: frankrimlinger
Date: 2009-06-29 18:48:51 +0000 (Mon, 29 Jun 2009)
Log Message:
-----------
Fixed various bugs. Scanner now survives both rkrug and system mangoUserHome code. However, in the system, none of the java package XXX_MangoFormal classes are modeled. Don't know why yet, but surely has something to do with the formal peer method stuff. The rest of the code appears to be modeled.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/BackupAlg.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/InvocationUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInvokeInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MethodUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROW.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEVIRTUAL.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-06-30 04:22:10
|
Revision: 1701
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1701&view=rev
Author: frankrimlinger
Date: 2009-06-30 04:21:40 +0000 (Tue, 30 Jun 2009)
Log Message:
-----------
Fixed various code survey bugs, so that only formal peer methods and methods which have no formal peer are added to the survey. The formal java code is still not being modeled, so this bug is still outstanding. Need to investigate the target launcher to see what is going wrong.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ClassUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/CodeSurvey.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MethodUtil.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-06-30 15:40:44
|
Revision: 1703
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1703&view=rev
Author: frankrimlinger
Date: 2009-06-30 15:40:38 +0000 (Tue, 30 Jun 2009)
Log Message:
-----------
TheMangoFormal aliased classes in the java package were not being modeled because the java package was specified as a "mango native" package. This feature was originally introduced to allow selective modeling of a "blended" jpf/formal environment. Since blending is not a good idea, the jpf environment should always be masked in its entirety, so this feature has been eliminated. Instead, all packages in the bootclasspath are designated as mango native, and then classes within a native class are modeled if they contain "_MangoFormal" in their name. This is a temporary solution. A better solution is to introduce a "user class loader" to jpf to allow for a "user environment" that can occupy the same namespace as the boot loader. Then it will not be necessary to alias the class names and many nasty technical issues will go away. But moving on for now.
Next bug, for some reason, the total vertex for an ASTORE fails to get created during phase1. Maybe some kind of exception handler bug??
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/worker/Worker.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/BackupAlg.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/CodeSurvey.java
branches/mango/MangoJPF/src/mango/intro/ConfigurationDetails.java
branches/mango/MangoJPF/src/mango/intro/LoginDialog.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-06-30 20:50:39
|
Revision: 1704
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1704&view=rev
Author: frankrimlinger
Date: 2009-06-30 20:50:37 +0000 (Tue, 30 Jun 2009)
Log Message:
-----------
ATHROWHANDLER is not branching correctly, so that instructions (like ASTORE) that handlers normally flow into are unreachable. The problem is that the ReturnPointLinkSym mechanism is not implemented. Probably need to go back to the original C++ to figure out what is going on here. The place to start is ClassParsingAlg::linkAthrowHandler. Working with marc's hypo2 test code.
Looking ahead, some details of the jpf rewriter are becoming clear. Phase2 will terminate prior to stratification, just emitting a set of components. The component selection algorithm will pick the "best" independent component, meaning a component "near" the target method which does not depend on any non-abstracted module. A synthetic MethodInfo will be created whose "instructions" are just proxies for the vertices of this component. A new extension of JPF, called REWRITER, will be instantiated. REWRITER will just act directly on the instructions of the synthetic MethodInfo, bypassing the class loading phase altogether. The different types of component vertices will give rise to different instructions, so that component connectors can be properly interpreted and loop vertices can orchestrate the "look-behind" strategy for invariant computation. Since this strategy only involves looking backward along a single execution path, it doesn't really need the full weight of the backtracking mechanism. But the backtracking mechanism will still have its traditional role of exhausting all paths, or at least all "interesting" paths, so that targeted module will be specified in a single REWRITER pass. This will make the process much more efficient as common initial paths no longer require re-tracing for each case. An "ordinary" instruction will just handle composition with the forward predicate transformer B* ^ I*. For non-trivial non-loop-dependent branch predicates B=b1 v .. V bn, the branch condition bi can just be automatically translated and assumed, displaying automatically in the specification window. The updated state can also be translated to check for a "translation halt". Whenever there is a translation halt, the user will intervene with appropriate definitions and translation rules. Once the situation is rectified, then REWRITER will fire back up and continue generating the specification. For loop-dependent branches B, REWRITER will first try invariant look-behind to eliminate the loops. If this fails, there will be an "invariance halt". In the case of loop termination, B will consist of a set of alternative ways to exit a loop, and the user then must choose the nominal exit condition as the "termination conjecture". (In the uncommon case of more than one nominal exit, the user can declare a backtracking point to get the opportunity to explore it later.) In any case, the user must formulate a conjecture that ensures deterministic forward execution, so that mango knows what branch to take. The user must also volunteer hypotheses on the module input parameters that make the conjecture true. This is on a best-effort basis, proof of conjectures is sub-contracted to a theorem prover. Since at all times REWRITER "knows where we are", context can be zippered on as needed for computations which require context. In particular, context does not need to be present during state composition, so the whole "context resolution" issue goes away. There will also be the existing halt for module instantiation. Note that the strategies which require halting should be handled by listeners so that the instructions can concentrate on the basic issue of state transition.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/BackupAlg.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/CodeSurvey.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ExceptionHandlerUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MethodUtil.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-07-01 21:03:13
|
Revision: 1710
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1710&view=rev
Author: frankrimlinger
Date: 2009-07-01 21:03:05 +0000 (Wed, 01 Jul 2009)
Log Message:
-----------
Each invocation is followed by an ACATCHHANDLER which handles exceptions thrown by callee but not caught in callee. Each instruction which potentially throws and exception directly is followed by an ATHROWCREATOR. The purpose of these synthetic instructions is to route the exception to the correct handler instuctions embedded in the code block, or to the synthetic ATHROWHANDLER instruction to handle the finally clause and/or uncaught exceptions.
Fix in progress so that the ACATCHHANLDER and ATHROWCREATORs are
a) created before referenced
b) passed to the choice generator of the instruction which invokes, in the case of ACATCHHANDLER, or throws, in the case of ATHROWCREATOR, and,
c) endowed with their branches prior to scanner execution, so that scanner flow through all the handlers is accomplished.
INVOKEINTERFACE conforms to the new scheme, remains to rewire the rest of the invocations and then all the other methods throwing exceptions.
Some comments to clear up the vast cloud of confusion that has accompanied this issue.
The theory of return points is thus: each invocation in the modeled code determines which methods it potentially calls. So we get a map invocation --> {potentially_called_method}. Inverting this map gives method --> {potential_invocation_point}. By considering the next instruction after the point of invocation, we get method-->{potential_return_point}.
There are two tricky observations to make:
1) The universal connector (ucon) for a return instruction has the form OR_i (and invocation_i return_point_i). In a flat calling space, this ucon is never actually applied, because the state transition of the invoked method is already known, and so it is just applied along the branch from invocation to next instruction. However, in the case of mutual co-recursion, the return branch condition is in play. To resolve this condition the invocation point became part of the "context" of the callee frame. This context was then dragged along ball-and-chain style as the state transitions of the callee were composed, vastly increasing the complexity of the rewrite rules. But in the brave new jpf world, we have look-behind, so we can go *get* the invocation point in the rare event we need to resolve a return condition. Otherwise, we don't trouble ourselves about it at all.
2) The logic of the return point system implements (1). The reason some of this logic is commented out is historical. ATHROWCREATOR creates the branch conditions required to route an exception thrown by a non-invocation instruction. Ditto ACATCHHANDLER for invoke instructions. Originally, ATHROWCREATOR and ACATCHHANDLER folded in the return branch condition of (1) in the case of an uncaught exception. But then Marc thought, "we need to implement finally". So the return logic was commented out and replaced by a branch to the unique ATHROWHANDLER for the method.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ExceptionHandlerUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/Invocation.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/InvocationUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInterface.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInvokeInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKECLINIT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEINTERFACE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKESPECIAL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKESTATIC.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEVIRTUAL.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-07-02 05:38:48
|
Revision: 1716
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1716&view=rev
Author: frankrimlinger
Date: 2009-07-02 05:38:46 +0000 (Thu, 02 Jul 2009)
Log Message:
-----------
Cleanup up of invocation instructions, finally resolving the exception handler chicken-and-egg. The solution is to uncouple *creation* of ACATCHHANLDER and ATHROWCREATOR, required by the execute() routine to set up scanner branching, from the formal construction, which takes place as it should in buildFormalPeer. These two different activities have finally been teased apart correctly.
Rehab must be propagated to all the other instructions which branch in the scanner. Also, ATHROWCREATOR is not playing well with BranchChoiceGenerator, need to investigate this.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/BackupAlg.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/CodeSurvey.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ExceptionHandlerUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/Invocation.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInterface.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInvokeInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ACATCHHANDLER.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IDIV.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEINTERFACE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKESPECIAL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKESTATIC.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEVIRTUAL.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-07-02 19:22:55
|
Revision: 1720
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1720&view=rev
Author: frankrimlinger
Date: 2009-07-02 19:21:51 +0000 (Thu, 02 Jul 2009)
Log Message:
-----------
Finished updated all instructions that throw. Pointed marc's project at all its test code. The scanner survives all the code, but component graph build fails. A big chunk is missing from extest.try2(). Start with this bug.
Modified Paths:
--------------
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ExceptionHandlerUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/Invocation.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/AALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/AASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ANEWARRAY.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ARRAYLENGTH.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROW.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/BALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/BASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/CALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/CASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/CHECKCAST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/GETFIELD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IDIV.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IREM.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LDIV.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LREM.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/MULTIANEWARRAY.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/NEWARRAY.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/PUTFIELD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/SALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/SASTORE.java
branches/mango/MangoJPF/mangoUserHome/marc/.classpath
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-07-03 18:41:53
|
Revision: 1721
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1721&view=rev
Author: frankrimlinger
Date: 2009-07-03 18:41:52 +0000 (Fri, 03 Jul 2009)
Log Message:
-----------
Fixed code survey bug which confused the beginningo of the *range* of an exception handler with the beginning of the exception handler. This cleared up a lot of missing code issues. Next bug in tryck2.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/CodeSurvey.java
branches/mango/MangoJPF/mangoUserHome/marc/.classpath
branches/mango/MangoJPF/mangoUserHome/marc/try1/extest/try1.java
Removed Paths:
-------------
branches/mango/MangoJPF/mangoUserHome/marc/try2/extest/
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-07-06 02:10:25
|
Revision: 1722
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1722&view=rev
Author: frankrimlinger
Date: 2009-07-06 02:10:18 +0000 (Mon, 06 Jul 2009)
Log Message:
-----------
Entire backup algorithm now completes normally for all marc's exceptionhandler test code. Now need to generated the specifications to make sure all related formal semantics are correct. Also cleanup of 2D graphics display in progress
Fixed athrow creator bug. Each exception thrown by an instruction is supposed to have its own athrow creator to figure out how to route the exception to the various handlers supplied in the code block of the method. All such athrow creator instructions have to be available to the scanner for scheduling in the branch choice generator, so that they are properly scanned. At a different execution point, the handlers need to be available to the buildFormalPeer method of the throwing instruction, so that the proper formal semantics can be wired in.
The brain-dead bug was that all exceptions for an instruction were being routed through the same athrow creator. Even though the athrow creators were being stockpiled in advance, they were not being used. To fix this problem, the creation of athrow creators is now the responsibility of the individual instruction classes. An instruction which throws now implements the ThrowsException interface. The creators are created during the initialization of the instruction. The new design binds an athrow creator to the Exception class it represents in much more sane, type safe way.
NOTE: The flag "mustPop2" appears to be obsolete in the C++ code, and so has been dropped in MangoJPF. The original comment for this flag was "Also, if the parameter mustPop2 is TRUE, then this athrowcreator follows an invocation, and must pop the extra frame."
Historical note: The original C++ had a one-size-fits-all instruction class, so no sane design for the athrow creators was possible in that world.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java
branches/mango/MangoJPF/Mango/src/mango/worker/Worker.java
branches/mango/MangoJPF/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashEngine.java
branches/mango/MangoJPF/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashOpcodeSyms.java
branches/mango/MangoJPF/Mango/src/mango/worker/flags/ExceptionHandlerDebuggingFlags.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/BackupAlg.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/vertex/CpnVertex.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/LocalVariableInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ExceptionHandlerUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/Invocation.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInterface.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInvokeInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/AALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/AASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ACATCHHANDLER.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ANEWARRAY.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ARRAYLENGTH.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROW.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROWCREATOR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROWHANDLER.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/BALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/BASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/CALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/CASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/CHECKCAST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DCONST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DLOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FCONST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/GETFIELD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ICONST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IDIV.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEINTERFACE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKESPECIAL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEVIRTUAL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IREM.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LCONST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LDIV.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LREM.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/MULTIANEWARRAY.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/NEWARRAY.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/PUTFIELD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/SALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/SASTORE.java
branches/mango/MangoJPF/mangoUserHome/marc/.classpath
branches/mango/MangoJPF/mangoUserHome/marc/trychk6/extest/trychk6.java
Added Paths:
-----------
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ThrowsException.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-07-06 06:42:16
|
Revision: 1723
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1723&view=rev
Author: frankrimlinger
Date: 2009-07-06 06:42:12 +0000 (Mon, 06 Jul 2009)
Log Message:
-----------
Exception handler code cleanup. Also ran the copyright stamp.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/core/gui/action/CloseCoreRuleBaseAction.java
branches/mango/MangoJPF/Mango/src/mango/core/sym/UntypedVariable.java
branches/mango/MangoJPF/Mango/src/mango/enterprise/model/ClassProxy.java
branches/mango/MangoJPF/Mango/src/mango/enterprise/model/ClassProxyPersistenceDelegate.java
branches/mango/MangoJPF/Mango/src/mango/enterprise/model/MethodProxy.java
branches/mango/MangoJPF/Mango/src/mango/enterprise/model/MethodProxyPersistenceDelegate.java
branches/mango/MangoJPF/Mango/src/mango/gumboModel/msg/GumboCommand.java
branches/mango/MangoJPF/Mango/src/mango/gumboModel/msg/PopupMenuCommand.java
branches/mango/MangoJPF/Mango/src/mango/module/definition/loop/LoopDefinitionManager.java
branches/mango/MangoJPF/Mango/src/mango/module/definition/model/DefinitionManager.java
branches/mango/MangoJPF/Mango/src/mango/module/definition/msg/RestoreContextMsg.java
branches/mango/MangoJPF/Mango/src/mango/module/instance/model/InstanceUtil.java
branches/mango/MangoJPF/Mango/src/mango/ruleAction/conditionalTechniques/conditional/GetFreeVariableName.java
branches/mango/MangoJPF/Mango/src/mango/ruleAction/conditionalTechniques/conditional/OverDisambiguation.java
branches/mango/MangoJPF/Mango/src/mango/ruleAction/conditionalTechniques/conditional/SyntacticEquals.java
branches/mango/MangoJPF/Mango/src/mango/ruleAction/coreRewriter/clinit/HasCommutingClinit.java
branches/mango/MangoJPF/Mango/src/mango/ruleAction/translate/engine/TranslateFreeVariableSym.java
branches/mango/MangoJPF/Mango/src/mango/ruleAction/translate/engine/TranslateOver.java
branches/mango/MangoJPF/Mango/src/mango/ruleAction/translate/engine/TranslateValueH.java
branches/mango/MangoJPF/Mango/src/mango/ruleRequirement/function/OverReq.java
branches/mango/MangoJPF/Mango/src/mango/ruleRequirement/symbols/UntypedVariableReq.java
branches/mango/MangoJPF/Mango/src/mango/source/agent/msg/SourceViewCreateRequestMsg.java
branches/mango/MangoJPF/Mango/src/mango/worker/GlobalViewModel.java
branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java
branches/mango/MangoJPF/Mango/src/mango/worker/PayloadRunnable.java
branches/mango/MangoJPF/Mango/src/mango/worker/TreeViewPopUpBinding.java
branches/mango/MangoJPF/Mango/src/mango/worker/Worker.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/BackupAlg.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/graphic/MethodSym.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/ucon/MethodEntrySym.java
branches/mango/MangoJPF/Mango/src/mango/worker/msg/AckPermCommand.java
branches/mango/MangoJPF/Mango/src/mango/worker/msg/AutoResetMsg.java
branches/mango/MangoJPF/Mango/src/mango/worker/msg/GenerateSpecificationMsg.java
branches/mango/MangoJPF/Mango/src/mango/worker/msg/NewWorkerMsg.java
branches/mango/MangoJPF/Mango/src/mango/worker/msg/OpenDefinitionMsg.java
branches/mango/MangoJPF/Mango/src/mango/worker/msg/RulebaseMsg.java
branches/mango/MangoJPF/Mango/src/mango/worker/msg/SaveMsg.java
branches/mango/MangoJPF/Mango/src/mango/worker/msg/SaveScriptMsg.java
branches/mango/MangoJPF/Mango/src/mango/worker/msg/ScheduleAutoCommand.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/coreTechniques/agent/OverAgent.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/coreTechniques/model/HeapTracer.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/coreTechniques/msg/StableRewriteLocator.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/coreTechniques/msg/StableRewriteMsg.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/coreTechniques/trap/StableRewriteConnector.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/form/sym/LineNumberSym.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/form/sym/binder/ContextBinderSym.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/form/sym/binder/executable/LocalVarSym.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/model/AckConnector.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/model/HitemUtil.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/model/UniversalTerminator.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/msg/WorkerCommand.java
branches/mango/MangoJPF/ThreadSupport/src/threadModel/PermCommand.java
branches/mango/MangoJPF/ThreadSupport/src/threadModel/PermCommander.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/SCANNER.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/JPF_mango_scanner_ScannerMJI.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/ARRAYLENGTH.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/ATHROW.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/ArrayInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/BIPUSH.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/CHECKCAST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/D2F.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/D2I.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/D2L.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/DADD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/DCMPG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/DCMPL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/DCONST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/DDIV.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/DMUL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/DNEG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/DREM.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/DSUB.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/DUP.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/DUP2.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/DUP2_X1.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/DUP2_X2.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/DUP_X1.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/DUP_X2.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/F2D.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/F2I.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/F2L.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/FADD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/FCMPG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/FCMPL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/FCONST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/FDIV.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/FMUL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/FNEG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/FREM.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/FSUB.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/FieldInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/GOTO.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/I2B.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/I2C.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/I2D.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/I2F.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/I2L.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/I2S.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/IADD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/IAND.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/ICONST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/IDIV.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/IINC.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/IMUL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/INEG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/INSTANCEOF.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/IOR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/IREM.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/ISHL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/ISHR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/ISUB.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/IUSHR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/IXOR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/IfInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/JSR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/JSR_W.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/L2D.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/L2F.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/L2I.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/LADD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/LAND.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/LCMP.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/LCONST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/LDC.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/LDC2_W.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/LDIV.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/LMUL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/LNEG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/LOR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/LREM.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/LSHL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/LSHR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/LSUB.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/LUSHR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/LXOR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/LockInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/MONITORENTER.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/MONITOREXIT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/MULTIANEWARRAY.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/NEW.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/NEWARRAY.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/NOP.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/POP.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/POP2.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/RET.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/RUNSTART.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/ReturnInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/SIPUSH.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/SWAP.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/SwitchInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/AbstractUconMethod.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/BadMethod.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/BranchChoiceGenerator.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/BranchListener.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/CodeSurvey.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/FakeMethod.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/Invocation.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoFormalInterface.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInstructionFactory.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInterface.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInvokeInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoTargetLauncher.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/OSmethod.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/Package.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ReturnPointLink.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ScannerMJI.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/TargetChoiceGenerator.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/TargetListener.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ThrowsException.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/AALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/AASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ACATCHHANDLER.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ACONST_NULL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ANEWARRAY.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ARETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ARRAYLENGTH.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROW.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROWCREATOR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROWHANDLER.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/AbstractUconPlace.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/BALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/BASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/BIPUSH.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/BadPlace.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/BeginningOfTime.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/CALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/CASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/CHECKCAST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/D2F.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/D2I.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/D2L.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DADD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DCMPG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DCMPL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DCONST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DDIV.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DLOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DMUL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DNEG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DREM.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DRETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DSTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DSUB.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DUP.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DUP2.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DUP2_X1.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DUP2_X2.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DUP_X1.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DUP_X2.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/F2D.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/F2I.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/F2L.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FADD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FCMPG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FCMPL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FCONST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FDIV.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FLOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FMUL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FNEG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FREM.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FRETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FSTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FSUB.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/GETFIELD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/GETSTATIC.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/GOTO.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/GOTO_W.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/I2B.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/I2C.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/I2D.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/I2F.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/I2L.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/I2S.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IADD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IAND.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ICONST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IDIV.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFEQ.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFGE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFGT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFLE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFLT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFNE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFNONNULL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFNULL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ACMPEQ.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ACMPNE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ICMPEQ.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ICMPGE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ICMPGT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ICMPLE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ICMPLT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ICMPNE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IINC.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ILOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IMUL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INEG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INSTANCEOF.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKECG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKECLINIT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEINTERFACE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKESPECIAL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKESTATIC.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKETARGET.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEVIRTUAL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IOR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IREM.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IRETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ISHL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ISHR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ISTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ISUB.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IUSHR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IXOR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/JSR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/JSR_W.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/L2D.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/L2F.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/L2I.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LADD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LAND.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LCMP.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LCONST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LDC.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LDC2_W.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LDC_W.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LDIV.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LLOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LMUL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LNEG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LOOKUPSWITCH.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LOR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LREM.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LRETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LSHL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LSHR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LSTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LSUB.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LUSHR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LXOR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/MONITORENTER.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/MONITOREXIT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/MULTIANEWARRAY.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/NEW.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/NEWARRAY.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/NOP.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/OSplace.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/POP.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/POP2.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/PUTFIELD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/PUTSTATIC.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/RET.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/RETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/RUNSTART.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/SALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/SASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/SIPUSH.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/SWAP.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/SyntheticInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/TABLESWITCH.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/sym/InstructionSym.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/sym/JmethodSym.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/sym/ReturnPointLinkSym.java
branches/mango/MangoJPF/src/mango/Activator.java
branches/mango/MangoJPF/src/mango/intro/Application.java
branches/mango/MangoJPF/src/mango/intro/ApplicationActionBarAdvisor.java
branches/mango/MangoJPF/src/mango/intro/ApplicationWorkbenchAdvisor.java
branches/mango/MangoJPF/src/mango/intro/ApplicationWorkbenchWindowAdvisor.java
branches/mango/MangoJPF/src/mango/intro/ConfigurationDetails.java
branches/mango/MangoJPF/src/mango/intro/LoginDialog.java
branches/mango/MangoJPF/src/mango/intro/Perspective.java
branches/mango/MangoJPF/src/mango/preferences/GeneralPreferencePage.java
branches/mango/MangoJPF/src/mango/views/GenSpecWindow.java
branches/mango/MangoJPF/src/mango/views/GlobalViewWindow.java
branches/mango/MangoJPF/src/mango/views/LogWindow.java
branches/mango/MangoJPF/src/mango/views/MainPanel.java
branches/mango/MangoJPF/src/mango/views/MangoScriptWindow.java
branches/mango/MangoJPF/src/mango/views/SampleView.java
Added Paths:
-----------
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoClassPeer.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoMethodPeer.java
Removed Paths:
-------------
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ClassUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ExceptionHandlerUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/InvocationUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MethodUtil.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-07-06 20:09:05
|
Revision: 1725
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1725&view=rev
Author: frankrimlinger
Date: 2009-07-06 20:08:57 +0000 (Mon, 06 Jul 2009)
Log Message:
-----------
Fixed some EZ bugs. Added translation logic and rules for thrown exceptions, necessary for the specification of marc's exception handler test code. This feature is brand new for MangoJPF, the first of many.
hypo2.test2() now specifies correctly, throwing an exception after setting a static variable in a finally handler.
"Assumes 'input' equals 0. Sets extest.hypo2.checkPoint3=1. Throws : java.lang.ArithmeticException at #0."
Sweet.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/ruleAction/coreRewriter/classModel/Instanceof.java
branches/mango/MangoJPF/Mango/src/mango/ruleAction/translate/engine/BoolRecapture.java
branches/mango/MangoJPF/Mango/src/mango/ruleAction/translate/engine/TranslateLoopUcon.java
branches/mango/MangoJPF/Mango/src/mango/ruleAction/translate/engine/TranslateNoReturnUcon.java
branches/mango/MangoJPF/Mango/src/mango/ruleAction/translate/engine/TranslateReturnUcon.java
branches/mango/MangoJPF/Mango/src/mango/ruleRequirement/naturalLanguage/Instantiated.java
branches/mango/MangoJPF/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashEnterpriseAndTranslation.java
branches/mango/MangoJPF/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashLogicAndArithmetic.java
branches/mango/MangoJPF/Mango/src/mango/worker/engine/sym/ObjMap.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/agent/CheckCast_getValueAgent.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/agent/InstanceOfAgent.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/agent/IsAssignmentCompatibleAgent.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/agent/ValueHAgent.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/translate/model/TranslateLoopManager.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/translate/model/TranslateModuleManager.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/translate/model/TranslateReturnManager.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/translate/trap/TranslateTrap.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoMethodPeer.java
branches/mango/MangoJPF/mangoUserHome/frank/rules/rulebase.zip
branches/mango/MangoJPF/mangoUserHome/marc/.classpath
Added Paths:
-----------
branches/mango/MangoJPF/Mango/src/mango/ruleAction/translate/engine/TranslateThrownExceptionUcon.java
branches/mango/MangoJPF/mangoUserHome/frank/sessions/extest/
branches/mango/MangoJPF/mangoUserHome/frank/sessions/extest/hypo2/
branches/mango/MangoJPF/mangoUserHome/frank/sessions/extest/hypo2/test2(I)I/
branches/mango/MangoJPF/mangoUserHome/frank/sessions/extest/hypo2/test2(I)I/'input' equals 0.zip
branches/mango/MangoJPF/mangoUserHome/marc/try2/extest/
branches/mango/MangoJPF/mangoUserHome/marc/try2/extest/try2.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-07-06 21:32:33
|
Revision: 1726
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1726&view=rev
Author: frankrimlinger
Date: 2009-07-06 21:32:26 +0000 (Mon, 06 Jul 2009)
Log Message:
-----------
Fixed some EZ bugs. There is a problem in hypo2.test() after the call to test2(). In this case, an explicit handler is set up to catch exceptions at the source code level. However, the ArithmeticException thrown by test2() is not caught as it should be, and checkPoint2 is not set. Inspection of the graph reveals that the branch conditions for the ATHROWANDLER are brain-dead. Investigating.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/form/model/StatItemModel.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/form/model/StatModel.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInvokeInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ACATCHHANDLER.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROWCREATOR.java
branches/mango/MangoJPF/mangoUserHome/frank/rules/rulebase.zip
Added Paths:
-----------
branches/mango/MangoJPF/mangoUserHome/frank/sessions/a.zip
branches/mango/MangoJPF/mangoUserHome/frank/sessions/extest/hypo2/test()I/
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-07-07 14:38:56
|
Revision: 1728
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1728&view=rev
Author: frankrimlinger
Date: 2009-07-07 14:14:47 +0000 (Tue, 07 Jul 2009)
Log Message:
-----------
Fixed some EZ bugs, and now hypo2 test recognizes that ArithmeticException is indeed and Exception, sets the static variable checkpoint2, and returns the answer=0. At this point, all references to the ArithmeticException, which was created in the present, have vanished, so it should garbage collect. Unfortunately, it does not. Investigating.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/agent/InstanceOfAgent.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/form/model/HeapModel.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ACATCHHANDLER.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROWCREATOR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROWHANDLER.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/sym/JclassSym.java
branches/mango/MangoJPF/mangoUserHome/frank/rules/rulebase.zip
Added Paths:
-----------
branches/mango/MangoJPF/mangoUserHome/frank/sessions/extest/hypo2/test()I/a.zip
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-07-07 18:26:40
|
Revision: 1729
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1729&view=rev
Author: frankrimlinger
Date: 2009-07-07 18:26:39 +0000 (Tue, 07 Jul 2009)
Log Message:
-----------
hypo2 exception handler test now fully specified. Failure of garbage collection was just a symptom of a problem that went away upon re-specification of test2(). The original specification of test2() put the thrown exception on the wrong frame. Not entirely sure how this problem corrected itself, but oh well... onward.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/core/gui/window/CoreSuperWindow.java
branches/mango/MangoJPF/Mango/src/mango/ruleAction/translate/engine/TranslateStatItem.java
branches/mango/MangoJPF/Mango/src/mango/ruleAction/translate/engine/TranslateSubaddress.java
branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java
branches/mango/MangoJPF/Mango/src/mango/worker/flags/GarbageCollectionDebuggingFlags.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROWHANDLER.java
branches/mango/MangoJPF/mangoUserHome/frank/rules/rulebase.zip
branches/mango/MangoJPF/mangoUserHome/frank/sessions/extest/hypo2/test2(I)I/'input' equals 0.zip
branches/mango/MangoJPF/mangoUserHome/marc/hypo2/src/extest/hypo2.java
Added Paths:
-----------
branches/mango/MangoJPF/mangoUserHome/frank/sessions/extest/hypo2/test()I/case.zip
Removed Paths:
-------------
branches/mango/MangoJPF/mangoUserHome/frank/sessions/a.zip
branches/mango/MangoJPF/mangoUserHome/frank/sessions/extest/hypo2/test()I/a.zip
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-07-07 20:09:54
|
Revision: 1730
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1730&view=rev
Author: frankrimlinger
Date: 2009-07-07 20:09:51 +0000 (Tue, 07 Jul 2009)
Log Message:
-----------
Fixed a bug that was causing virtual invocation to fail.
Modified Paths:
--------------
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInvokeInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKECLINIT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEINTERFACE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKESPECIAL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEVIRTUAL.java
Added Paths:
-----------
branches/mango/MangoJPF/mangoUserHome/frank/sessions/a.zip
branches/mango/MangoJPF/mangoUserHome/frank/sessions/extest/try1/
branches/mango/MangoJPF/mangoUserHome/frank/sessions/extest/try1/<init>()V/
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
×
Want the latest updates on software, tech news, and AI?
Get latest updates about software, tech news, and AI from SourceForge directly in your inbox once a month.
Thanks for helping keep SourceForge clean.
X