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-05-13 19:25:30
|
Revision: 1509 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1509&view=rev Author: frankrimlinger Date: 2009-05-13 19:25:22 +0000 (Wed, 13 May 2009) Log Message: ----------- Simplified control for rulebase button. The rulebase button is now always enabled. If a rulebase has been loaded, pressing the rulebase button now just opens the top-level rulebase window. Otherwise, pressing the rulebase button loads a new rulebase. The trick is that to get rid of an existing rulebase, you now have to close it from the rulebase "File" menu. The close command is only enabled when there are no live worker threads. It is intentionally difficult to load a new rulebase, since this is not normally something a user would want to do. Rewired the quit listener for SWT so that the user gets queried to save rulebase if dirty. Now finally onto the buildWorkerImage selector for RulebaseMsg. With this in place we can kick the SCANNER and start building control flow graphs. Modified Paths: -------------- branches/mango/MangoJPF/Mango/src/mango/control/action/input/RuleBaseAction.java branches/mango/MangoJPF/Mango/src/mango/core/gui/action/SaveCoreRuleBaseAction.java branches/mango/MangoJPF/Mango/src/mango/core/gui/window/CoreRuleBaseWindow.java branches/mango/MangoJPF/Mango/src/mango/worker/Worker.java branches/mango/MangoJPF/Mango/src/mango/worker/WorkerControl.java branches/mango/MangoJPF/Mango/src/mango/worker/msg/RulebaseMsg.java branches/mango/MangoJPF/mangoUserHome/frank/rules/rulebase.zip branches/mango/MangoJPF/src/mango/views/GenSpecWindow.java Added Paths: ----------- branches/mango/MangoJPF/Mango/src/mango/core/gui/action/CloseCoreRuleBaseAction.java Removed Paths: ------------- branches/mango/MangoJPF/Mango/src/mango/core/gui/action/LoadCoreRuleBaseAction.java This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <pcm...@us...> - 2009-05-13 18:46:42
|
Revision: 1508 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1508&view=rev Author: pcmehlitz Date: 2009-05-13 18:46:28 +0000 (Wed, 13 May 2009) Log Message: ----------- * fixed bug in single choice CGs in ui and statechart, causing trace replay to fail * added a replay test * added a trace.verbose, which adds a commented out CG printout for each line. Just for debugging purposes of shorter traces, so it's off by default * statechart scripting can now use pathnames relative to *.jpf Modified Paths: -------------- trunk/extensions/statechart/env/jpf/gov/nasa/jpf/sc/PendingEventQueue.java trunk/extensions/statechart/env/jvm/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_sc_StateMachine.java trunk/extensions/statechart/env/jvm/gov/nasa/jpf/jvm/NativeStateMachine.java trunk/extensions/statechart/src/gov/nasa/jpf/jvm/choice/sc/SCEventSingleChoice.java trunk/extensions/ui/src/gov/nasa/jpf/jvm/choice/ui/UIActionSingleChoice.java trunk/src/gov/nasa/jpf/jvm/ChoicePoint.java trunk/src/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_jvm_Verify.java trunk/src/gov/nasa/jpf/jvm/JVM.java trunk/src/gov/nasa/jpf/tools/ChoiceSelector.java trunk/src/gov/nasa/jpf/tools/TraceStorer.java trunk/test/gov/nasa/jpf/mc/TestPartialTrace.java trunk/test/gov/nasa/jpf/mc/TestPartialTraceJPF.java This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <pc...@us...> - 2009-05-13 00:05:04
|
Revision: 1507 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1507&view=rev Author: pcorina Date: 2009-05-13 00:04:50 +0000 (Wed, 13 May 2009) Log Message: ----------- Modified Paths: -------------- trunk/.classpath This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <fra...@us...> - 2009-05-12 20:49:11
|
Revision: 1506 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1506&view=rev Author: frankrimlinger Date: 2009-05-12 20:48:56 +0000 (Tue, 12 May 2009) Log Message: ----------- Added perm commands to rough-out the sketch of the new automation system. Endowed the permanent thread group with the "ack" system, modeled after the tested ack system for TrapCommands. This required adding the Perm priority AUTOACK. The new ack system posts AckPermCommands to this thread in order to block. Coding for the STARTUP selector for RulebaseMsg. This involves porting various dialogs to SWT. A trick here is to use Worker.getDisplay().syncExec() to guarantee that the dialog comes up in the right thread. Modified Paths: -------------- branches/mango/MangoJPF/Mango/src/mango/core/gui/action/SaveCoreRuleBaseAction.java branches/mango/MangoJPF/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHash.java branches/mango/MangoJPF/Mango/src/mango/worker/msg/RulebaseMsg.java branches/mango/MangoJPF/Mango/src/mango/worker/msg/ScheduleAutoCommand.java branches/mango/MangoJPF/ThreadSupport/src/threadModel/Priority.java branches/mango/MangoJPF/ThreadSupport/src/threadModel/SystemBuilder.java Added Paths: ----------- branches/mango/MangoJPF/Mango/src/mango/worker/msg/AckPermCommand.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/ResetMsg.java branches/mango/MangoJPF/Mango/src/mango/worker/msg/SaveMsg.java This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <fra...@us...> - 2009-05-12 03:55:20
|
Revision: 1505 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1505&view=rev Author: frankrimlinger Date: 2009-05-12 03:55:19 +0000 (Tue, 12 May 2009) Log Message: ----------- Wiring for posting of AUTO commands in place. Rough-out of RulebaseMsg, which uses a selector to handle all aspects of the rulebase lifecycle. It is probably a good idea to sketch out all the AUTO rules involved in start up automation prior to detailed coding. Modified Paths: -------------- branches/mango/MangoJPF/Mango/src/mango/worker/Worker.java branches/mango/MangoJPF/Mango/src/mango/worker/msg/RulebaseMsg.java branches/mango/MangoJPF/Mango/src/mango/worker/msg/ScheduleAutoCommand.java branches/mango/MangoJPF/ThreadSupport/src/threadModel/SystemBuilder.java This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <pcm...@us...> - 2009-05-11 23:55:16
|
Revision: 1504 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1504&view=rev Author: pcmehlitz Date: 2009-05-11 23:55:06 +0000 (Mon, 11 May 2009) Log Message: ----------- * small change in ExecTracker/Step to avoid re-printing the same source line Modified Paths: -------------- trunk/src/gov/nasa/jpf/jvm/Step.java trunk/src/gov/nasa/jpf/tools/ExecTracker.java This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <wv...@us...> - 2009-05-11 21:36:53
|
Revision: 1503 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1503&view=rev Author: wvisser Date: 2009-05-11 21:36:45 +0000 (Mon, 11 May 2009) Log Message: ----------- Main class for handling String constraints, by either using JSA or HAMPI * for now this is a hard-coded decision, but will be read from an option in the future Modified Paths: -------------- trunk/extensions/symbc/src/gov/nasa/jpf/symbc/string/SymbolicStringConstraintsGeneral.java This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <wv...@us...> - 2009-05-11 21:35:50
|
Revision: 1502 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1502&view=rev Author: wvisser Date: 2009-05-11 21:35:42 +0000 (Mon, 11 May 2009) Log Message: ----------- Class to handle String constraints for JSA * for now this is broken since it does not include dependencies in the constraints Added Paths: ----------- trunk/extensions/symbc/src/gov/nasa/jpf/symbc/string/SymbolicStringConstraintsJSA.java This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <wv...@us...> - 2009-05-11 21:34:55
|
Revision: 1501 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1501&view=rev Author: wvisser Date: 2009-05-11 21:34:47 +0000 (Mon, 11 May 2009) Log Message: ----------- Class to handle String constraints for HAMPI * HAMPI only works on Linux Added Paths: ----------- trunk/extensions/symbc/src/gov/nasa/jpf/symbc/string/SymbolicStringConstraintsHAMPI.java This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <fra...@us...> - 2009-05-11 18:00:22
|
Revision: 1500 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1500&view=rev Author: frankrimlinger Date: 2009-05-11 18:00:12 +0000 (Mon, 11 May 2009) Log Message: ----------- Thread support for automation level (permanent) threads complete. These new threads have their own commander. The original threads are unaware of automation level, execpt that all threads share the same command completion lock. The point is that automation level threads can't fire if any normal thread activity is pending, and automation level threads never reset. Currently there is only one priority.Perm AUTO, but its possible that more priority levels could be added. The automation level threads fire up automatically when the SystemBuilder is created. Start with RulebaseMsg, posted on startup to figure out what the deal is with the rulebase. Modified Paths: -------------- branches/mango/MangoJPF/ThreadSupport/src/threadModel/Command.java branches/mango/MangoJPF/ThreadSupport/src/threadModel/SystemBuilder.java Added Paths: ----------- branches/mango/MangoJPF/Mango/src/mango/worker/msg/ branches/mango/MangoJPF/Mango/src/mango/worker/msg/RulebaseMsg.java branches/mango/MangoJPF/Mango/src/mango/worker/msg/ScheduleAutoCommand.java branches/mango/MangoJPF/ThreadSupport/src/threadModel/CommandState.java branches/mango/MangoJPF/ThreadSupport/src/threadModel/PermCommand.java branches/mango/MangoJPF/ThreadSupport/src/threadModel/PermCommander.java Removed Paths: ------------- branches/mango/MangoJPF/Mango/src/mango/workstation/ This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <fra...@us...> - 2009-05-11 11:03:26
|
Revision: 1499 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1499&view=rev Author: frankrimlinger Date: 2009-05-11 11:03:15 +0000 (Mon, 11 May 2009) Log Message: ----------- Modifications to TheadSupport for AUTO support in progress. Modified Paths: -------------- branches/mango/MangoJPF/Mango/src/mango/worker/Worker.java branches/mango/MangoJPF/ThreadSupport/src/threadModel/Priority.java branches/mango/MangoJPF/ThreadSupport/src/threadModel/SystemBuilder.java Removed Paths: ------------- branches/mango/MangoJPF/Mango/src/mango/workstation/impl/ This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <pcm...@us...> - 2009-05-11 04:52:35
|
Revision: 1498 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1498&view=rev Author: pcmehlitz Date: 2009-05-11 04:52:25 +0000 (Mon, 11 May 2009) Log Message: ----------- * added Milos Gligoric's & Tihomir Gvero's delayed CG extension - the general idea is to delay choice generation until the point where the choice value is used. See delayed/doc and the referenced paper http://infoscience.epfl.ch/record/128816 Modified Paths: -------------- trunk/.classpath Added Paths: ----------- trunk/extensions/delayed/ trunk/extensions/delayed/build.xml trunk/extensions/delayed/doc/ trunk/extensions/delayed/doc/index.html trunk/extensions/delayed/src/ trunk/extensions/delayed/src/gov/ trunk/extensions/delayed/src/gov/nasa/ trunk/extensions/delayed/src/gov/nasa/jpf/ trunk/extensions/delayed/src/gov/nasa/jpf/delayed/ trunk/extensions/delayed/src/gov/nasa/jpf/delayed/NCPInstructionFactory.java trunk/extensions/delayed/src/gov/nasa/jpf/delayed/ObjectPool.java trunk/extensions/delayed/src/gov/nasa/jpf/delayed/attr/ trunk/extensions/delayed/src/gov/nasa/jpf/delayed/attr/AnyObjNCPDelayedAttr.java trunk/extensions/delayed/src/gov/nasa/jpf/delayed/attr/BooleanNCPDelayedAttr.java trunk/extensions/delayed/src/gov/nasa/jpf/delayed/attr/IntNCPDelayedAttr.java trunk/extensions/delayed/src/gov/nasa/jpf/delayed/attr/NCPDelayedAttr.java trunk/extensions/delayed/src/gov/nasa/jpf/delayed/attr/NewObjNCPDelayedAttr.java trunk/extensions/delayed/src/gov/nasa/jpf/delayed/attr/ObjNCPDelayedAttr.java trunk/extensions/delayed/src/gov/nasa/jpf/delayed/bytecode/ trunk/extensions/delayed/src/gov/nasa/jpf/delayed/bytecode/AALOAD.java trunk/extensions/delayed/src/gov/nasa/jpf/delayed/bytecode/ALOAD.java trunk/extensions/delayed/src/gov/nasa/jpf/delayed/bytecode/BALOAD.java trunk/extensions/delayed/src/gov/nasa/jpf/delayed/bytecode/CHECKCAST.java trunk/extensions/delayed/src/gov/nasa/jpf/delayed/bytecode/GETFIELD.java trunk/extensions/delayed/src/gov/nasa/jpf/delayed/bytecode/GETSTATIC.java trunk/extensions/delayed/src/gov/nasa/jpf/delayed/bytecode/IALOAD.java trunk/extensions/delayed/src/gov/nasa/jpf/delayed/bytecode/IINC.java trunk/extensions/delayed/src/gov/nasa/jpf/delayed/bytecode/ILOAD.java trunk/extensions/delayed/src/gov/nasa/jpf/delayed/bytecode/INVOKESPECIAL.java trunk/extensions/delayed/src/gov/nasa/jpf/delayed/bytecode/INVOKESTATIC.java trunk/extensions/delayed/src/gov/nasa/jpf/delayed/bytecode/INVOKEVIRTUAL.java trunk/extensions/delayed/src/gov/nasa/jpf/delayed/bytecode/VirtualInvocation.java trunk/extensions/delayed/src/gov/nasa/jpf/delayed/cg/ trunk/extensions/delayed/src/gov/nasa/jpf/delayed/cg/DelayedCG.java trunk/extensions/delayed/src/gov/nasa/jpf/delayed/cg/ObjDelayedCG.java trunk/extensions/delayed/src/gov/nasa/jpf/delayed/state/ trunk/extensions/delayed/src/gov/nasa/jpf/delayed/state/AnyOrderEntry.java trunk/extensions/delayed/src/gov/nasa/jpf/delayed/state/NCPDelayedStateExtensionClient.java trunk/extensions/delayed/src/gov/nasa/jpf/delayed/state/NewOrderEntry.java trunk/extensions/delayed/src/gov/nasa/jpf/delayed/state/Order.java trunk/extensions/delayed/src/gov/nasa/jpf/delayed/state/OrderEntry.java trunk/extensions/delayed/src/gov/nasa/jpf/delayed/state/UnderlineObjectPool.java trunk/extensions/delayed/src/gov/nasa/jpf/delayed/util/ trunk/extensions/delayed/src/gov/nasa/jpf/delayed/util/NCPUtils.java trunk/extensions/delayed/src/gov/nasa/jpf/delayed/util/Pair.java trunk/extensions/delayed/src/gov/nasa/jpf/delayed/util/Roundtrip.java trunk/extensions/delayed/src/gov/nasa/jpf/jvm/ trunk/extensions/delayed/src/gov/nasa/jpf/jvm/NCPDelayedRestorer.java trunk/extensions/delayed/test/ trunk/extensions/delayed/test/gov/ trunk/extensions/delayed/test/gov/nasa/ trunk/extensions/delayed/test/gov/nasa/jpf/ trunk/extensions/delayed/test/gov/nasa/jpf/delayed/ trunk/extensions/delayed/test/gov/nasa/jpf/delayed/TestAALOAD.java trunk/extensions/delayed/test/gov/nasa/jpf/delayed/TestAALOADJPF.java trunk/extensions/delayed/test/gov/nasa/jpf/delayed/TestALOAD.java trunk/extensions/delayed/test/gov/nasa/jpf/delayed/TestALOADJPF.java trunk/extensions/delayed/test/gov/nasa/jpf/delayed/TestBALOAD.java trunk/extensions/delayed/test/gov/nasa/jpf/delayed/TestBALOADJPF.java trunk/extensions/delayed/test/gov/nasa/jpf/delayed/TestDefaultObjectPool.java trunk/extensions/delayed/test/gov/nasa/jpf/delayed/TestDefaultObjectPoolJPF.java trunk/extensions/delayed/test/gov/nasa/jpf/delayed/TestGETFIELD.java trunk/extensions/delayed/test/gov/nasa/jpf/delayed/TestGETFIELDJPF.java trunk/extensions/delayed/test/gov/nasa/jpf/delayed/TestGETSTATIC.java trunk/extensions/delayed/test/gov/nasa/jpf/delayed/TestGETSTATICJPF.java trunk/extensions/delayed/test/gov/nasa/jpf/delayed/TestIALOAD.java trunk/extensions/delayed/test/gov/nasa/jpf/delayed/TestIALOADJPF.java trunk/extensions/delayed/test/gov/nasa/jpf/delayed/TestILOAD.java trunk/extensions/delayed/test/gov/nasa/jpf/delayed/TestILOADJPF.java trunk/extensions/delayed/test/gov/nasa/jpf/delayed/test/ trunk/extensions/delayed/test/gov/nasa/jpf/delayed/test/conf/ trunk/extensions/delayed/test/gov/nasa/jpf/delayed/test/conf/ConfigurableTestJPF.java trunk/extensions/delayed/test/gov/nasa/jpf/delayed/test/conf/DefaultConfigurableTestJPF.java trunk/extensions/delayed/test/gov/nasa/jpf/delayed/test/conf/NCPConfigurableTestJPF.java trunk/extensions/delayed/test/gov/nasa/jpf/delayed/test/util/ trunk/extensions/delayed/test/gov/nasa/jpf/delayed/test/util/JPF_gov_nasa_jpf_delayed_test_util_TestUtils.java trunk/extensions/delayed/test/gov/nasa/jpf/delayed/test/util/TestUtils.java This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <fra...@us...> - 2009-05-10 16:27:43
|
Revision: 1497 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1497&view=rev Author: frankrimlinger Date: 2009-05-10 16:27:34 +0000 (Sun, 10 May 2009) Log Message: ----------- More Worker cleanup. The sense of the Worker as the main coordinating entity is now more apparent. I can't believe I just wrote that. Modified Paths: -------------- branches/mango/MangoJPF/Mango/src/mango/control/action/input/RuleBaseAction.java branches/mango/MangoJPF/Mango/src/mango/core/CoreMangoObject.java branches/mango/MangoJPF/Mango/src/mango/core/actions/ActionsManager.java branches/mango/MangoJPF/Mango/src/mango/core/gui/tablemodel/MangoModelUtilities.java branches/mango/MangoJPF/Mango/src/mango/core/gui/window/CoreRuleBaseWindow.java branches/mango/MangoJPF/Mango/src/mango/core/requirements/RequirementsManager.java branches/mango/MangoJPF/Mango/src/mango/deprecatedPackage/DeprecatedMethods.java branches/mango/MangoJPF/Mango/src/mango/merge/window/FindPatternWindow.java branches/mango/MangoJPF/Mango/src/mango/module/trap/MapToScopeTrap.java branches/mango/MangoJPF/Mango/src/mango/script/gui/action/ScriptRunAction.java branches/mango/MangoJPF/Mango/src/mango/script/gui/action/ScriptSaveAction.java branches/mango/MangoJPF/Mango/src/mango/script/model/MangoScriptModel.java branches/mango/MangoJPF/Mango/src/mango/script/util/MangoScriptUtilities.java branches/mango/MangoJPF/Mango/src/mango/util/LOG.java 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/WorkerControl.java branches/mango/MangoJPF/Mango/src/mango/worker/engine/rule/AssumeEquivRule.java branches/mango/MangoJPF/Mango/src/mango/worker/engine/sym/Sym.java branches/mango/MangoJPF/Mango/src/mango/worker/javaModel/classParser/ClassParsingAlg.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/backupAlg/BackupAlg.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/graph/StrataGraph.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/vertex/BackupVertex.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/vertex/CpnVertex.java branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/coreTechniques/msg/RewriteRequestMsg.java branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/coreTechniques/trap/ApplyLinearTrap.java branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/coreTechniques/trap/GarbageCollectTrap.java branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/msg/InitSessionMsg.java branches/mango/MangoJPF/src/mango/intro/ApplicationWorkbenchAdvisor.java branches/mango/MangoJPF/src/mango/views/GenSpecWindow.java branches/mango/MangoJPF/src/mango/views/LogWindow.java branches/mango/MangoJPF/src/mango/views/MangoScriptWindow.java Removed Paths: ------------- branches/mango/MangoJPF/Mango/src/mango/control/action/control/BackupAction.java branches/mango/MangoJPF/Mango/src/mango/control/action/control/StartAction.java branches/mango/MangoJPF/Mango/src/mango/control/msg/BackupRequestMsg.java branches/mango/MangoJPF/Mango/src/mango/control/msg/LoadClassFileDataRequestMsg.java branches/mango/MangoJPF/Mango/src/mango/control/msg/SetEntryPointRequestMsg.java branches/mango/MangoJPF/Mango/src/mango/control/msg/SetSourceDirectoryRequestMsg.java branches/mango/MangoJPF/Mango/src/mango/control/msg/StartRequestMsg.java This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <fra...@us...> - 2009-05-10 02:14:37
|
Revision: 1496 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1496&view=rev Author: frankrimlinger Date: 2009-05-10 01:34:24 +0000 (Sun, 10 May 2009) Log Message: ----------- Package level cleanup. The functionality of the Workstation package has been parceled out, as the Workstation no longer exists. The Worker class now becomes a more or less central hub for Mango, Gumbo, ThreadSupport, JPF and RCP integration. The code base has evolved through so many different operating systems, development systems, and design architectures that it is not very tidy, but oh well... Modified Paths: -------------- branches/mango/MangoJPF/Mango/src/mango/control/action/control/BackupAction.java branches/mango/MangoJPF/Mango/src/mango/control/action/control/DebugRewriterAction.java 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/control/action/editor/PostAction.java branches/mango/MangoJPF/Mango/src/mango/control/action/input/RuleBaseAction.java branches/mango/MangoJPF/Mango/src/mango/control/action/window/ResetPopupAction.java branches/mango/MangoJPF/Mango/src/mango/control/menu/WindowMenu.java branches/mango/MangoJPF/Mango/src/mango/control/msg/LoadClassFileDataRequestMsg.java branches/mango/MangoJPF/Mango/src/mango/control/msg/SetSourceDirectoryRequestMsg.java branches/mango/MangoJPF/Mango/src/mango/control/msg/StartRequestMsg.java branches/mango/MangoJPF/Mango/src/mango/control/window/HelpWindow.java branches/mango/MangoJPF/Mango/src/mango/core/CoreMangoObject.java branches/mango/MangoJPF/Mango/src/mango/core/gui/StaticFields.java branches/mango/MangoJPF/Mango/src/mango/core/gui/action/ClearStatisticsAction.java branches/mango/MangoJPF/Mango/src/mango/core/gui/action/CreateParametersAction.java branches/mango/MangoJPF/Mango/src/mango/core/gui/action/PrintAbstractionsAction.java branches/mango/MangoJPF/Mango/src/mango/core/gui/action/SaveCoreRuleBaseAction.java branches/mango/MangoJPF/Mango/src/mango/core/gui/tablemodel/MangoModelUtilities.java branches/mango/MangoJPF/Mango/src/mango/core/gui/window/CoreRuleBaseWindow.java branches/mango/MangoJPF/Mango/src/mango/core/gui/window/CoreRuleEditorWindow.java branches/mango/MangoJPF/Mango/src/mango/core/gui/window/CoreSuperWindow.java branches/mango/MangoJPF/Mango/src/mango/core/gui/window/CoreTierWindow.java branches/mango/MangoJPF/Mango/src/mango/core/util/CoreUtilities.java branches/mango/MangoJPF/Mango/src/mango/data/FontData.java branches/mango/MangoJPF/Mango/src/mango/data/MangoDataResolver.java branches/mango/MangoJPF/Mango/src/mango/debugger/BreakPointWindow.java branches/mango/MangoJPF/Mango/src/mango/debugger/DebuggerViewManager.java branches/mango/MangoJPF/Mango/src/mango/debugger/DebuggerWindow.java branches/mango/MangoJPF/Mango/src/mango/debugger/msg/ContinueRewritingMsg.java branches/mango/MangoJPF/Mango/src/mango/deprecatedPackage/DeprecatedMethods.java branches/mango/MangoJPF/Mango/src/mango/enterprise/locator/LocatorManager.java branches/mango/MangoJPF/Mango/src/mango/enterprise/workerID/PersistentParityID.java branches/mango/MangoJPF/Mango/src/mango/enterprise/workerID/SourceAspectID.java branches/mango/MangoJPF/Mango/src/mango/enterprise/workerID/TransientParityID.java branches/mango/MangoJPF/Mango/src/mango/graph/Graph2DViewManager.java branches/mango/MangoJPF/Mango/src/mango/graph/Graph2DViewWindow.java branches/mango/MangoJPF/Mango/src/mango/graph/Graph3DViewManager.java branches/mango/MangoJPF/Mango/src/mango/graph/Graph3DViewWindow.java branches/mango/MangoJPF/Mango/src/mango/graph/SuperGraph3DViewManager.java branches/mango/MangoJPF/Mango/src/mango/graph/SuperGraph3DViewWindow.java branches/mango/MangoJPF/Mango/src/mango/graph/agent/CoarseGraphViewAgent.java branches/mango/MangoJPF/Mango/src/mango/graph/agent/GraphViewAgent.java branches/mango/MangoJPF/Mango/src/mango/graph/msg/GraphViewCreateCommandMsg.java branches/mango/MangoJPF/Mango/src/mango/graph/msg/MultiGraph3DViewCreateCommandMsg.java branches/mango/MangoJPF/Mango/src/mango/list/ListNodeData.java branches/mango/MangoJPF/Mango/src/mango/list/ListViewManager.java branches/mango/MangoJPF/Mango/src/mango/list/dnd/JListDragSource.java branches/mango/MangoJPF/Mango/src/mango/list/dnd/JTextPaneDropHandler.java branches/mango/MangoJPF/Mango/src/mango/list/impl/LabelViewManager.java branches/mango/MangoJPF/Mango/src/mango/merge/action/SelectCoreRuleBaseAction.java branches/mango/MangoJPF/Mango/src/mango/merge/tree/MangoMergeTreeCellRenderer.java branches/mango/MangoJPF/Mango/src/mango/merge/window/FindPatternWindow.java branches/mango/MangoJPF/Mango/src/mango/module/ModuleWindowManager.java branches/mango/MangoJPF/Mango/src/mango/module/action/DebugGeneralizationAction.java branches/mango/MangoJPF/Mango/src/mango/module/action/DebugGeneralizationDetailsAction.java branches/mango/MangoJPF/Mango/src/mango/module/action/DebugInvariantsAction.java branches/mango/MangoJPF/Mango/src/mango/module/action/DebugInversionAction.java branches/mango/MangoJPF/Mango/src/mango/module/action/DebugLinearArithmeticAction.java branches/mango/MangoJPF/Mango/src/mango/module/action/ShowAssumptionMatchFailureAction.java branches/mango/MangoJPF/Mango/src/mango/module/action/ShowHitsAction.java branches/mango/MangoJPF/Mango/src/mango/module/action/ShowMatchMakerAction.java branches/mango/MangoJPF/Mango/src/mango/module/action/ShowMatchesAction.java branches/mango/MangoJPF/Mango/src/mango/module/action/ShowRewriteErrorAction.java branches/mango/MangoJPF/Mango/src/mango/module/action/ShowRewriterAssumptionsAction.java branches/mango/MangoJPF/Mango/src/mango/module/definition/AbstractAutoEquivalenceWindow.java branches/mango/MangoJPF/Mango/src/mango/module/definition/AbstractEquivalenceWindow.java branches/mango/MangoJPF/Mango/src/mango/module/definition/DefinitionWindowManager.java branches/mango/MangoJPF/Mango/src/mango/module/definition/action/AddEquivalenceAction.java branches/mango/MangoJPF/Mango/src/mango/module/definition/action/CloseCaseAction.java branches/mango/MangoJPF/Mango/src/mango/module/definition/model/DefinitionManager.java branches/mango/MangoJPF/Mango/src/mango/module/definition/msg/AddEquivalenceLocatorMsg.java branches/mango/MangoJPF/Mango/src/mango/module/instance/method/MethodInstanceWindowManager.java branches/mango/MangoJPF/Mango/src/mango/module/instance/method/model/MethodInstanceManager.java branches/mango/MangoJPF/Mango/src/mango/module/instance/model/InstanceManager.java branches/mango/MangoJPF/Mango/src/mango/module/model/ModuleManager.java branches/mango/MangoJPF/Mango/src/mango/rmi/file/MangoFilePacket.java branches/mango/MangoJPF/Mango/src/mango/script/MangoScriptSourceDirectory.java branches/mango/MangoJPF/Mango/src/mango/script/gui/MangoScriptMessageCellRenderer.java branches/mango/MangoJPF/Mango/src/mango/script/gui/action/ScriptRunAction.java branches/mango/MangoJPF/Mango/src/mango/script/gui/action/ScriptSaveAction.java branches/mango/MangoJPF/Mango/src/mango/script/model/MangoScriptModel.java branches/mango/MangoJPF/Mango/src/mango/script/util/MangoScriptUtilities.java branches/mango/MangoJPF/Mango/src/mango/script/util/ScriptAndPostAction.java branches/mango/MangoJPF/Mango/src/mango/source/SourceViewManager.java branches/mango/MangoJPF/Mango/src/mango/source/SourceViewWindow.java branches/mango/MangoJPF/Mango/src/mango/source/agent/SourceViewAgent.java branches/mango/MangoJPF/Mango/src/mango/source/agent/msg/SourceViewCreateCommandMsg.java branches/mango/MangoJPF/Mango/src/mango/tree/TreeViewManager.java branches/mango/MangoJPF/Mango/src/mango/tree/TreeViewWindow.java branches/mango/MangoJPF/Mango/src/mango/tree/agent/FolderViewAgent.java branches/mango/MangoJPF/Mango/src/mango/tree/agent/TreeViewAgent.java branches/mango/MangoJPF/Mango/src/mango/tree/data/TreeNodeClientData.java branches/mango/MangoJPF/Mango/src/mango/tree/msg/ChangeTreeCommandMsg.java branches/mango/MangoJPF/Mango/src/mango/tree/msg/MsgSendAspect.java branches/mango/MangoJPF/Mango/src/mango/tree/msg/TreeTabCreateCommandMsg.java branches/mango/MangoJPF/Mango/src/mango/tree/msg/TreeViewCreateCommandMsg.java branches/mango/MangoJPF/Mango/src/mango/tree/msg/UpdateParityModelsMsg.java branches/mango/MangoJPF/Mango/src/mango/util/FileSystem.java branches/mango/MangoJPF/Mango/src/mango/util/LOG.java branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java branches/mango/MangoJPF/Mango/src/mango/worker/WorkerControl.java branches/mango/MangoJPF/Mango/src/mango/worker/engine/rule/AssumeEquivRule.java branches/mango/MangoJPF/Mango/src/mango/worker/engine/rule/Rule.java branches/mango/MangoJPF/Mango/src/mango/worker/javaModel/classParser/ClassModel.java branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/coreTechniques/msg/RewriteLocatorMsg.java branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/coreTechniques/msg/StableRewriteLocator.java branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/model/EventLoopTrap.java branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/msg/InitSessionMsg.java branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/SCANNER.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/CodeSurvey.java branches/mango/MangoJPF/src/mango/intro/Application.java branches/mango/MangoJPF/src/mango/intro/ApplicationWorkbenchAdvisor.java branches/mango/MangoJPF/src/mango/intro/ApplicationWorkbenchWindowAdvisor.java branches/mango/MangoJPF/src/mango/intro/LoginDialog.java branches/mango/MangoJPF/src/mango/views/GenSpecWindow.java branches/mango/MangoJPF/src/mango/views/LogWindow.java branches/mango/MangoJPF/src/mango/views/MangoScriptWindow.java Added Paths: ----------- branches/mango/MangoJPF/Mango/src/mango/core/RuleResourceManager.java branches/mango/MangoJPF/Mango/src/mango/gumboModel/ColorDataBinding.java branches/mango/MangoJPF/Mango/src/mango/gumboModel/ContextManager.java branches/mango/MangoJPF/Mango/src/mango/gumboModel/PopUpResourceManager.java branches/mango/MangoJPF/Mango/src/mango/gumboModel/ViewBuilder.java branches/mango/MangoJPF/Mango/src/mango/gumboModel/action/ branches/mango/MangoJPF/Mango/src/mango/gumboModel/action/ActionCategory.java branches/mango/MangoJPF/Mango/src/mango/gumboModel/action/ActionCategoryMenu.java branches/mango/MangoJPF/Mango/src/mango/gumboModel/action/ActionCategoryTree.java branches/mango/MangoJPF/Mango/src/mango/gumboModel/action/ActionManager.java branches/mango/MangoJPF/Mango/src/mango/gumboModel/action/InternallyEnabledAction.java branches/mango/MangoJPF/Mango/src/mango/gumboModel/action/MangoAction.java branches/mango/MangoJPF/Mango/src/mango/gumboModel/action/MangoActionManager.java branches/mango/MangoJPF/Mango/src/mango/gumboModel/action/MangoActionMenuItem.java branches/mango/MangoJPF/Mango/src/mango/gumboModel/action/SingleSelectAction.java branches/mango/MangoJPF/Mango/src/mango/gumboModel/agent/ branches/mango/MangoJPF/Mango/src/mango/gumboModel/agent/ActionAgent.java branches/mango/MangoJPF/Mango/src/mango/gumboModel/agent/AspectModelAgent.java branches/mango/MangoJPF/Mango/src/mango/gumboModel/data/ branches/mango/MangoJPF/Mango/src/mango/gumboModel/data/AspectTableListener.java branches/mango/MangoJPF/Mango/src/mango/gumboModel/data/AspectTableModel.java branches/mango/MangoJPF/Mango/src/mango/gumboModel/data/ColorPool.java branches/mango/MangoJPF/Mango/src/mango/gumboModel/data/MangoTextStyle.java branches/mango/MangoJPF/Mango/src/mango/gumboModel/data/Primo.java branches/mango/MangoJPF/Mango/src/mango/gumboModel/factory/ branches/mango/MangoJPF/Mango/src/mango/gumboModel/factory/EmbeddedJVMFactory.java branches/mango/MangoJPF/Mango/src/mango/gumboModel/factory/GraphModelFactory.java branches/mango/MangoJPF/Mango/src/mango/gumboModel/factory/ListModelFactory.java branches/mango/MangoJPF/Mango/src/mango/gumboModel/factory/MultiGraphModelFactory.java branches/mango/MangoJPF/Mango/src/mango/gumboModel/factory/SourceModelFactory.java branches/mango/MangoJPF/Mango/src/mango/gumboModel/factory/TreeModelFactory.java branches/mango/MangoJPF/Mango/src/mango/gumboModel/impl/ branches/mango/MangoJPF/Mango/src/mango/gumboModel/impl/Swing/ branches/mango/MangoJPF/Mango/src/mango/gumboModel/impl/Swing/MangoSwingGraphVertex.java branches/mango/MangoJPF/Mango/src/mango/gumboModel/impl/Swing/MangoSwingGraphViewFactory.java branches/mango/MangoJPF/Mango/src/mango/gumboModel/interaction/ branches/mango/MangoJPF/Mango/src/mango/gumboModel/interaction/Actions.java branches/mango/MangoJPF/Mango/src/mango/gumboModel/interaction/BaseInput.java branches/mango/MangoJPF/Mango/src/mango/gumboModel/interaction/CenterViewManager.java branches/mango/MangoJPF/Mango/src/mango/gumboModel/interaction/GroupOverManager.java branches/mango/MangoJPF/Mango/src/mango/gumboModel/interaction/MangoViewManager.java branches/mango/MangoJPF/Mango/src/mango/gumboModel/interaction/PopUpMenuEnabler.java branches/mango/MangoJPF/Mango/src/mango/gumboModel/interaction/PopupMenuManager.java branches/mango/MangoJPF/Mango/src/mango/gumboModel/interaction/StandardInput.java branches/mango/MangoJPF/Mango/src/mango/gumboModel/interaction/WorkstationCheckBoxMenuItem.java branches/mango/MangoJPF/Mango/src/mango/gumboModel/interaction/WorkstationMenuItem.java branches/mango/MangoJPF/Mango/src/mango/gumboModel/msg/ 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/gumboModel/msg/SetAllActionsEnabledMsg.java branches/mango/MangoJPF/Mango/src/mango/gumboModel/msg/SetEnabledActionsMsg.java branches/mango/MangoJPF/Mango/src/mango/gumboModel/window/ branches/mango/MangoJPF/Mango/src/mango/gumboModel/window/AspectWindow.java branches/mango/MangoJPF/Mango/src/mango/gumboModel/window/ChildWindow.java branches/mango/MangoJPF/Mango/src/mango/gumboModel/window/CoarseGraphWindow.java branches/mango/MangoJPF/Mango/src/mango/gumboModel/window/DebugFlagsDialog.java branches/mango/MangoJPF/Mango/src/mango/gumboModel/window/FeatureWindow.java branches/mango/MangoJPF/Mango/src/mango/gumboModel/window/WindowMonitor.java branches/mango/MangoJPF/Mango/src/mango/gumboModel/window/Windows.java branches/mango/MangoJPF/Mango/src/mango/worker/TreeViewPopUpBinding.java branches/mango/MangoJPF/Mango/src/mango/worker/Worker.java Removed Paths: ------------- branches/mango/MangoJPF/Mango/src/mango/gumboModel/EmbeddedJVMFactory.java branches/mango/MangoJPF/Mango/src/mango/gumboModel/GraphModelFactory.java branches/mango/MangoJPF/Mango/src/mango/gumboModel/ListModelFactory.java branches/mango/MangoJPF/Mango/src/mango/gumboModel/MultiGraphModelFactory.java branches/mango/MangoJPF/Mango/src/mango/gumboModel/SourceModelFactory.java branches/mango/MangoJPF/Mango/src/mango/gumboModel/TreeModelFactory.java branches/mango/MangoJPF/Mango/src/mango/worker/Worker.java branches/mango/MangoJPF/Mango/src/mango/workstation/ContextManager.java branches/mango/MangoJPF/Mango/src/mango/workstation/PopUpResourceManager.java branches/mango/MangoJPF/Mango/src/mango/workstation/QueueReader.java branches/mango/MangoJPF/Mango/src/mango/workstation/RuleResourceManager.java branches/mango/MangoJPF/Mango/src/mango/workstation/ViewBuilder.java branches/mango/MangoJPF/Mango/src/mango/workstation/Workstation.java branches/mango/MangoJPF/Mango/src/mango/workstation/action/ branches/mango/MangoJPF/Mango/src/mango/workstation/agent/ branches/mango/MangoJPF/Mango/src/mango/workstation/data/ branches/mango/MangoJPF/Mango/src/mango/workstation/impl/swing/ branches/mango/MangoJPF/Mango/src/mango/workstation/interaction/ branches/mango/MangoJPF/Mango/src/mango/workstation/msg/ branches/mango/MangoJPF/Mango/src/mango/workstation/preferences/ branches/mango/MangoJPF/Mango/src/mango/workstation/window/ This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <fra...@us...> - 2009-05-09 19:35:38
|
Revision: 1495 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1495&view=rev Author: frankrimlinger Date: 2009-05-09 19:35:36 +0000 (Sat, 09 May 2009) Log Message: ----------- Removed the old input window and entrypoint window from the code base. This might have caused some damage to the old secondary and tertiary unblocking system, but this web of hacks will be completely subsumed by jpf driven rewriting anyway. Modified Paths: -------------- branches/mango/MangoJPF/Mango/src/mango/control/action/input/RuleBaseAction.java branches/mango/MangoJPF/Mango/src/mango/control/menu/WindowMenu.java branches/mango/MangoJPF/Mango/src/mango/core/gui/StaticFields.java branches/mango/MangoJPF/Mango/src/mango/core/gui/rendering/BooleanCellRenderer.java branches/mango/MangoJPF/Mango/src/mango/core/gui/rendering/CoreRuleCellRenderer.java branches/mango/MangoJPF/Mango/src/mango/core/gui/rendering/CoreTierCellRenderer.java branches/mango/MangoJPF/Mango/src/mango/core/gui/rendering/CoreVariableStringCellRenderer.java branches/mango/MangoJPF/Mango/src/mango/core/gui/rendering/StringCellRenderer.java branches/mango/MangoJPF/Mango/src/mango/core/gui/window/CoreRuleBaseWindow.java branches/mango/MangoJPF/Mango/src/mango/core/gui/window/CoreSuperWindow.java branches/mango/MangoJPF/Mango/src/mango/core/gui/window/CoreTierWindow.java branches/mango/MangoJPF/Mango/src/mango/module/ModuleWindow.java branches/mango/MangoJPF/Mango/src/mango/module/definition/DefinitionWindow.java branches/mango/MangoJPF/Mango/src/mango/module/instance/InstanceWindow.java branches/mango/MangoJPF/Mango/src/mango/module/instance/loop/LoopInstanceWindow.java branches/mango/MangoJPF/Mango/src/mango/module/instance/method/MethodInstanceWindow.java branches/mango/MangoJPF/Mango/src/mango/ruleAction/simpleSubstitution/SUBRautomatic.java branches/mango/MangoJPF/Mango/src/mango/script/MangoScriptResource.java branches/mango/MangoJPF/Mango/src/mango/script/gui/MangoScriptMessageCellRenderer.java branches/mango/MangoJPF/Mango/src/mango/script/model/MangoScriptModel.java branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java branches/mango/MangoJPF/Mango/src/mango/worker/WorkerControl.java branches/mango/MangoJPF/Mango/src/mango/worker/engine/sym/InterpretableSym.java branches/mango/MangoJPF/Mango/src/mango/worker/engine/unifier/UnifyEvent.java branches/mango/MangoJPF/Mango/src/mango/workstation/Workstation.java branches/mango/MangoJPF/Mango/src/mango/workstation/interaction/WorkstationMenuItem.java branches/mango/MangoJPF/src/mango/intro/Perspective.java branches/mango/MangoJPF/src/mango/views/GenSpecWindow.java branches/mango/MangoJPF/src/mango/views/LogWindow.java branches/mango/MangoJPF/src/mango/views/MainPanel.java Removed Paths: ------------- branches/mango/MangoJPF/Mango/src/mango/control/action/input/LibraryJarsAction.java branches/mango/MangoJPF/Mango/src/mango/control/action/input/SourceDirsAction.java branches/mango/MangoJPF/Mango/src/mango/control/action/input/TargetJarsAction.java branches/mango/MangoJPF/Mango/src/mango/control/action/window/GlobalViewAction.java branches/mango/MangoJPF/Mango/src/mango/control/action/window/WorkstationAction.java branches/mango/MangoJPF/Mango/src/mango/control/input/ branches/mango/MangoJPF/Mango/src/mango/script/model/MangoScriptClassModel.java branches/mango/MangoJPF/Mango/src/mango/script/model/MangoScriptLibraryModel.java branches/mango/MangoJPF/Mango/src/mango/script/model/MangoScriptMethodModel.java branches/mango/MangoJPF/Mango/src/mango/script/model/MangoScriptSourceModel.java branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/msg/UnblockStateRequestMsg.java branches/mango/MangoJPF/Mango/src/mango/workstation/window/ToggleUnblockingStateAction.java branches/mango/MangoJPF/src/mango/views/GlobalViewWindow.java branches/mango/MangoJPF/src/mango/views/WorkstationWindow.java This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <fra...@us...> - 2009-05-09 17:14:30
|
Revision: 1494 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1494&view=rev Author: frankrimlinger Date: 2009-05-09 17:14:29 +0000 (Sat, 09 May 2009) Log Message: ----------- added preferences for automation Modified Paths: -------------- branches/mango/MangoJPF/.classpath branches/mango/MangoJPF/Mango/src/mango/workstation/Workstation.java branches/mango/MangoJPF/src/mango/preferences/GeneralPreferencePage.java branches/mango/MangoJPF/src/mango/views/LogWindow.java This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <fra...@us...> - 2009-05-08 16:44:52
|
Revision: 1493 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1493&view=rev Author: frankrimlinger Date: 2009-05-08 16:44:45 +0000 (Fri, 08 May 2009) Log Message: ----------- Cleanup and addition of rulebase preference and Priority.E AUTO. The plan is to remove the "Input Manager" and "Java Code Entrypoints" windows, as this functionality has been subsumed. However, the "New Worker", "Reset", "MFL Editor", and "Rulebase" buttons now migrate to the "Specification" window. Here is the top-level logic for automation of mango. This will be great for getting demos off the ground without trouble. Nominally,at startup, "Rulebase" enabled, "New Worker" and "Reset" disabled. 1. If, at startup, there is a valid rulebase specified in the preferences, then it is read in, and the "New Worker" button will be enabled. "Rulebase" disabled. 2. If the "Fire new worker on startup" preference is checked, then, the New Worker action will fire automatically. "New Worker" disabled and "Reset" enabled 3. If the "Open Definition Window Automatically" preference is checked, then the default target selected by the targeting algorithm will be used to open the definition window. 4. If the "Generate Specification Automatically" preference is checked, then the SPECIFICATION extension of JPF will do its thing. Of course there will still be some user interaction, but only when the specification listeners deem it necessary to query the user. In this case, the user will be told what the issue is and suggested ways to proceed will be offered. This will allow the user to learn by doing. NOTE: SPECIFICATION will need to cache some backtracking information in the rulebase, in order to deduce which paths have already been specified. This finally stretches the original rulebase concept completely beyond the breaking point. A rational structure for persistent data will obviously have a hierarchical data base structure, but this must be addressed in a future lifetime. 5. Once the specification is done, "Rulebase" will be enabled. If "Save Rulebase and Session Automatically" is set, then this is done. Otherwise, the user will be prompted to do this. if the "Reset Automatically" preference is checked, then the reset will occur automatically and the process will repeat. The same preference rules will apply, except in step 1, the existing rulebase will be recycled, just flushing the worker image, as is already done now. These steps will be accomplished via Commands. Since this all of this is happening transparently to the notion of a session, a new lowest priority level "AUTO" has been added to Priority, and the "LOW" priority has been renamed "SESSION". Observe that these new Commands now defer to user preferences when deciding whether or not to post successors. Also, this level of automation will be the first real test of the new "nested ack" capability. Also, the AUTO worker thread persists for the lifetime of mango, only the higher priority threads are killed on reset. If worst comes to worst, you must add a "Cold Reset" to kill off the AUTO thread and really start from scratch. Modified Paths: -------------- branches/mango/MangoJPF/Mango/src/mango/control/msg/ReplayedMsg.java branches/mango/MangoJPF/Mango/src/mango/core/gui/action/ApplyCoreRuleAction.java branches/mango/MangoJPF/Mango/src/mango/core/gui/action/CloneCoreRuleAction.java branches/mango/MangoJPF/Mango/src/mango/core/gui/action/CoreCutAction.java branches/mango/MangoJPF/Mango/src/mango/core/gui/action/CorePasteAction.java branches/mango/MangoJPF/Mango/src/mango/core/gui/action/DownloadCoreRuleAction.java branches/mango/MangoJPF/Mango/src/mango/core/gui/action/ImportCoreRuleAction.java branches/mango/MangoJPF/Mango/src/mango/core/gui/action/ImportCoreTierAction.java branches/mango/MangoJPF/Mango/src/mango/core/gui/action/NewCoreRuleAction.java branches/mango/MangoJPF/Mango/src/mango/core/gui/action/NewCoreTierAction.java branches/mango/MangoJPF/Mango/src/mango/core/gui/tablemodel/CoreRuleBaseTableModel.java branches/mango/MangoJPF/Mango/src/mango/core/gui/tablemodel/CoreTierTableModel.java branches/mango/MangoJPF/Mango/src/mango/core/gui/tablemodel/CoreVariableTableModel.java branches/mango/MangoJPF/Mango/src/mango/debugger/msg/ClearBreakPointMsg.java branches/mango/MangoJPF/Mango/src/mango/module/definition/msg/AddConjectureRequestMsg.java branches/mango/MangoJPF/Mango/src/mango/module/definition/msg/AddConjectureTranslateMsg.java branches/mango/MangoJPF/Mango/src/mango/module/definition/msg/AddEquivalenceAutoRequestMsg.java branches/mango/MangoJPF/Mango/src/mango/module/definition/msg/AddHypothesisAutoRequestMsg.java branches/mango/MangoJPF/Mango/src/mango/module/definition/msg/AddHypothesisRequestMsg.java branches/mango/MangoJPF/Mango/src/mango/module/definition/msg/AddHypothesisTranslateMsg.java branches/mango/MangoJPF/Mango/src/mango/module/definition/msg/CloseDefinitionMsg.java branches/mango/MangoJPF/Mango/src/mango/module/definition/msg/DeleteUnusedParametersMsg.java branches/mango/MangoJPF/Mango/src/mango/module/definition/msg/EliminateHypothesisRequestMsg.java branches/mango/MangoJPF/Mango/src/mango/module/instance/msg/SubmitStandingHypothesisMsg.java branches/mango/MangoJPF/Mango/src/mango/module/msg/ApplyLinearRequestMsg.java branches/mango/MangoJPF/Mango/src/mango/module/msg/GarbageCollectRequestMsg.java branches/mango/MangoJPF/Mango/src/mango/module/msg/GeneralizeRequestMsg.java branches/mango/MangoJPF/Mango/src/mango/module/msg/MapToScopeRequestMsg.java branches/mango/MangoJPF/Mango/src/mango/module/msg/MatchMakerRequestMsg.java branches/mango/MangoJPF/Mango/src/mango/script/util/ScriptAndPostAction.java branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/coreTechniques/msg/RewriteRequestMsg.java branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/msg/AddCoreMangoObjectMsg.java branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/msg/DeleteCoreMangoObjectMsg.java branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/msg/ModifyCoreMangoObjectMsg.java branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/msg/ReplaceRequestMsg.java branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/msg/ScheduleRequestMsg.java branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/msg/SetActiveCoreMangoObjectMsg.java branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/msg/TrapCommand.java branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/msg/WorkerCommand.java branches/mango/MangoJPF/Mango/src/mango/workstation/Workstation.java branches/mango/MangoJPF/ThreadSupport/src/threadModel/Priority.java branches/mango/MangoJPF/ThreadSupport/src/threadModel/ScriptableCommand.java branches/mango/MangoJPF/ThreadSupport/src/threadTest/CommandUtilities.java branches/mango/MangoJPF/ThreadSupport/src/threadTest/ScriptTest.java branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/SCANNER.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/BranchChoiceGenerator.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/CodeSurvey.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/INVOKETARGET.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/InvocationUtil.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoTargetLauncher.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/src/mango/intro/ConfigurationDetails.java branches/mango/MangoJPF/src/mango/intro/LoginDialog.java Removed Paths: ------------- branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/InstructionTemplates.txt This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <fra...@us...> - 2009-05-07 20:05:58
|
Revision: 1492 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1492&view=rev Author: frankrimlinger Date: 2009-05-07 20:05:48 +0000 (Thu, 07 May 2009) Log Message: ----------- Tweaked bytecodes to eliminate some unneeded classes. SCANNER phases are now just JPF and SCANNING, and in fact the whole concept of phase is now trivial. Punched in exception handler scanning code. This completes the scanner. Ready to write mango scanner hookups as outlined in previous comment. Modified Paths: -------------- branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/SCANNER.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/CodeSurvey.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/InstructionTemplates.txt 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/bytecode/AALOAD.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/AASTORE.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/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/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/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/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/TABLESWITCH.java Removed Paths: ------------- branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/Dispatch.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/Transition.java This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <fra...@us...> - 2009-05-07 16:14:09
|
Revision: 1491 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1491&view=rev Author: frankrimlinger Date: 2009-05-07 16:14:04 +0000 (Thu, 07 May 2009) Log Message: ----------- Fixed a few more scanning bugs. Successful scan of all methods system code (i.e. in javapathfinder-trunk/env/jpf/java) and user code (in MangoJPF/mangoUserHome/rkrug/input). Identification of clinit, native, and abstract methods. Identification of all unmodelled invocation destinations. Verified tableswitch is working correctly, which is a good sign that BranchChoiceGenerator is ok. It remains only to punch in the exception handler entrypoints to the TargetChoiceGenerator, and the scanner is complete. NB: OK, you need to position the scan AFTER the rulebase is read in. The reason is that we must have the manifest of abstraction methods ready-to-go before the scan starts. Now for some fun stuff. Several things must happen on-the-fly as control flow edges are reported to mango: 1. build a map from unmodelled-and-abstracted to rulebase abstractions. Report link errors for unmodelled-and-not-abstracted 2. build a map from modelled-and-abstracted invocations to rulebase abstractions. 3. build a dependency graph of modelled-but-not-abstracted. The leaves of this graph will be the candidates for the next abstraction target. 4. and of course, build the total control diagram whose vertices are bound to jpf Instructions and mango formal logic. This is the critical binding that will allow context-free expressions to bind to context and tap into jpf world. NOTE: in 1-3, vertices are bound to jpf MethodInfos. So, by the end of the scan, the stage is set for mango component analysis. We just jump right in at BackupAlg.phaseII() and deal with the culture shock. Modified Paths: -------------- 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/TargetChoiceGenerator.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LOOKUPSWITCH.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/TABLESWITCH.java This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <fra...@us...> - 2009-05-07 02:26:48
|
Revision: 1490 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1490&view=rev Author: frankrimlinger Date: 2009-05-07 02:26:40 +0000 (Thu, 07 May 2009) Log Message: ----------- Fixed various invocation related bugs. There is a problem when a choice terminates at an instruction that has already been visited. For some reason, pc becomes null because no listener is listening? Must investigate. Modified Paths: -------------- branches/mango/MangoJPF/Mango/src/mango/worker/Mango.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/InvocationUtil.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-05-06 21:27:56
|
Revision: 1489 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1489&view=rev Author: frankrimlinger Date: 2009-05-06 21:27:41 +0000 (Wed, 06 May 2009) Log Message: ----------- Finished final bytecode rehab and started testing code scanner. Late binding of the choice generated PC via VMListeners turns out to be a huge win. This works exactly as expected, and jpf is spinning out beautiful graph data for Mango to absorb. All the data is offered on a silver platter, without having to painfully wrestle down the bits in the .class files. Have starting working on well understood control flow issues, rulebase look up for missing code, etc. Once this settles down I will bind the formal state transition logic to the instructions, and adapt the mango code subdivision algorithm to the new setting. All that is required is to maintain the binding to jpf instructions, so that eventually the rewriter can be driven by jpf simulation. This will be very cool. Modified Paths: -------------- branches/mango/MangoJPF/Mango/src/mango/worker/Mango.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/mango/scanner/CodeSurvey.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/INVOKETARGET.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/InvocationUtil.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKESTATIC.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/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/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/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/TABLESWITCH.java Added Paths: ----------- branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/TargetListener.java This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <ubn...@us...> - 2009-05-05 22:18:32
|
Revision: 1488 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1488&view=rev Author: ubnepvpb Date: 2009-05-05 22:18:24 +0000 (Tue, 05 May 2009) Log Message: ----------- Carl Albach's fixes for the statechart visualizer to make it compatible with changes done to the core JPF and core statecharts. Modified Paths: -------------- trunk/extensions/statechart/src/gov/nasa/jpf/tools/visualize/VisualDriver.java trunk/extensions/statechart/src/gov/nasa/jpf/tools/visualize/VisualModel.java trunk/extensions/statechart/src/gov/nasa/jpf/tools/visualize/VisualSimStateMachine.java This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <fra...@us...> - 2009-05-05 21:40:25
|
Revision: 1487 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1487&view=rev Author: frankrimlinger Date: 2009-05-05 21:40:16 +0000 (Tue, 05 May 2009) Log Message: ----------- Scanner bytecodes are squeaky clean now, and most branch and all invocation bytecodes have been written. The only tricky thing is jsr and ret. Actually, jsr is easy because you can get the destination from the bcel peer. But ret is harder because the ret destination is in a local variable, and the frame is of course not available to us. So we resort to the mango method, just walk through the method, looking for a jsr which branches to the ret. Once we find it, our dest is just the instruction after the jsr. EZ Modified Paths: -------------- branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/AASTORE.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ARETURN.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/BIPUSH.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/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 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/LRETURN.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/RET.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/RETURN.java This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <fra...@us...> - 2009-05-05 18:19:59
|
Revision: 1486 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1486&view=rev Author: frankrimlinger Date: 2009-05-05 18:19:45 +0000 (Tue, 05 May 2009) Log Message: ----------- Prep work for final scanner bytecode rehab in place. The code is a lot cleaner and meaner. Replacing the target launcher with a choice generator for the synthetic INVOKETARGET instruction turned out to really simplify matters. In particular, the "phase transition" is now trivial. Once the scanner turns on, it stays until vm^2 exits upon exhausting all choices. Hopefully it will all work as expected, but not possible to test until bytecodes are ready. Modified Paths: -------------- branches/mango/MangoJPF/Mango/src/mango/worker/Mango.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/TargetChoiceGenerator.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEVIRTUAL.java Added Paths: ----------- branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/InvocationUtil.java Removed Paths: ------------- branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/ScannerStackFrame.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/InvocationChoiceGenerator.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ScanChoiceGenerator.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/VirtualInvocationScan.java This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <pc...@us...> - 2009-05-05 02:11:15
|
Revision: 1485 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1485&view=rev Author: pcorina Date: 2009-05-05 02:11:07 +0000 (Tue, 05 May 2009) Log Message: ----------- Modified Paths: -------------- trunk/extensions/symbc/test/gov/nasa/jpf/symbc/symtest.sh This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |