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-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-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-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-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-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: <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-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: <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-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: <fra...@us...> - 2009-05-13 20:48:30
|
Revision: 1510 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1510&view=rev Author: frankrimlinger Date: 2009-05-13 20:48:14 +0000 (Wed, 13 May 2009) Log Message: ----------- Rulebase image hooked up to automated start up. SCANNER hooked up to automated start up. Promptly crashes because no Mango object setup. Fix this bug and start working on control flow activities that occur during scan. Modified Paths: -------------- branches/mango/MangoJPF/Mango/src/mango/core/gui/action/SaveCoreRuleBaseAction.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/javapathfinder-mango-bridge/gov/nasa/jpf/SCANNER.java This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <fra...@us...> - 2009-05-14 15:26:09
|
Revision: 1513 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1513&view=rev Author: frankrimlinger Date: 2009-05-14 15:24:37 +0000 (Thu, 14 May 2009) Log Message: ----------- Deleted obsolete hashtables from Mango class. Deleted the following subpackages of mango.worker.javaModel: classParser errorModel jmvSyntax.attributes jvmSytax.helper_classes linkingModel sym Needless to say, this severely traumatized the mango codebase. The equivalent jpf functionality must now be wired in. Since the only remaining subpackage is byteCodeModel, it is now moved to mango.worker.byteCodeModel. This package maps bytecodes to their formal counterparts. The first order of business is to parcel this code out into the mango.scanner.bytecode classes. To this end, these classes will implement the new MangoFormalLanguage interface. For the purpose of this port, the deleted classes mango.worker.javaModel.classParser.Field mango.worker.javaModel.classParser.Instruction mango.worker.javaModel.classParser.Method mango.worker.javaModel.classParser.ClassModel become gov.nasa.jpf.jvm.FieldInfo gov.nasa.jpf.jvm.bytecode.Instruction gov.nasa.jpf.jvm.MethodInfo gov.nasa.jpf.jvm.ClassInfo This transformation will effectively bind mango flow control to jpf simulation. Hopefully the symbol counterparts of the mango classes can be totally eliminated now, but if not, they will be rewritten from scratch. Modified Paths: -------------- branches/mango/MangoJPF/Mango/src/mango/ruleAction/coreRewriter/classModel/BuildAbstractUcon.java branches/mango/MangoJPF/Mango/src/mango/ruleAction/coreRewriter/classModel/Is_class_loadable.java branches/mango/MangoJPF/Mango/src/mango/ruleAction/coreRewriter/clinit/ComposePrependedClinits.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/byteCodeModel/ArithmeticOp.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Branching.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Getandput.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Invocation.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Invoking.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Linker.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Loading.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/LogicAndIntegerInc.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Newandmisc.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/PopDupSwap.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Pushing.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Return.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Storing.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/TypeCasting.java branches/mango/MangoJPF/Mango/src/mango/worker/engine/events/LocalMessage.java branches/mango/MangoJPF/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHash.java branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/form/model/FrameModel.java branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/form/sym/binder/executable/FrameSym.java Added Paths: ----------- branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/ branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoFormalLanguage.java Removed Paths: ------------- branches/mango/MangoJPF/Mango/src/mango/worker/javaModel/byteCodeModel/ branches/mango/MangoJPF/Mango/src/mango/worker/javaModel/classParser/ branches/mango/MangoJPF/Mango/src/mango/worker/javaModel/errorModel/ branches/mango/MangoJPF/Mango/src/mango/worker/javaModel/jvmSyntax/attributes/ branches/mango/MangoJPF/Mango/src/mango/worker/javaModel/jvmSyntax/helper_classes/ branches/mango/MangoJPF/Mango/src/mango/worker/javaModel/linkingModel/ branches/mango/MangoJPF/Mango/src/mango/worker/javaModel/sym/ This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <fra...@us...> - 2009-05-14 18:51:47
|
Revision: 1515 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1515&view=rev Author: frankrimlinger Date: 2009-05-14 18:51:32 +0000 (Thu, 14 May 2009) Log Message: ----------- Created a new set of regular expressions for the formal bytecode port. These have all been tested on the port to AALOAD. Created ExceptionHandlerUtil to take over generation of the creation of flow control for exceptions. This code scattered around but a lot of it is in the obsolete CodeAttribute class. The strategy is to create a mapping of MethodInfo --> HandlerInfo, where HandlerInfo is a private inner class of ExceptionHandlerUtil. This map will allow ExceptionHandlerUtil to service the various requests for ExceptionHandler support. Also need to create a few synthetic Instructions to support throwing exception. The goal is just to replicate the existing control flow for thrown exceptions, generated as the scanner spins out it data. Modified Paths: -------------- branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoFormalLanguage.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/AALOAD.java Added Paths: ----------- branches/mango/MangoJPF/bytecode cheat.txt branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ExceptionHandlerUtil.java This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <fra...@us...> - 2009-05-14 21:05:37
|
Revision: 1518 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1518&view=rev Author: frankrimlinger Date: 2009-05-14 21:05:17 +0000 (Thu, 14 May 2009) Log Message: ----------- port of exception handler code to javapathfinder-mango-bridge in progress Modified Paths: -------------- branches/mango/MangoJPF/Mango/src/mango/worker/Worker.java branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/JPF_mango_scanner_ScannerMJI.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ExceptionHandlerUtil.java Added Paths: ----------- branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecodeSynthetic/ branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecodeSynthetic/ACATCHHANDLER.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecodeSynthetic/ATHROWCREATOR.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecodeSynthetic/ATHROWHANDLER.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecodeSynthetic/INVOKETARGET.java Removed Paths: ------------- branches/mango/MangoJPF/Mango/src/mango/worker/javaModel/ branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/INVOKETARGET.java This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <fra...@us...> - 2009-05-15 06:15:59
|
Revision: 1523 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1523&view=rev Author: frankrimlinger Date: 2009-05-15 06:15:50 +0000 (Fri, 15 May 2009) Log Message: ----------- Completed migration of ArithmeticOp bytecodes to the bridge. Rough-out of branching for nominal and exceptional cases. Applied regular expressions to all worker bytecodes to prepare for migration. Modified Paths: -------------- branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Branching.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Getandput.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Invoking.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Loading.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/LogicAndIntegerInc.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Newandmisc.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/PopDupSwap.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Pushing.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Return.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Storing.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/TypeCasting.java branches/mango/MangoJPF/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashOpcodeSyms.java branches/mango/MangoJPF/bytecode cheat.txt branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ExceptionHandlerUtil.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInstructionFactory.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/AALOAD.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DADD.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DDIV.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/DSUB.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FADD.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FDIV.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/FSUB.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IADD.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IDIV.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/IREM.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ISUB.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LADD.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LDIV.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/LREM.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LSUB.java Added Paths: ----------- branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/BranchUtil.java Removed Paths: ------------- branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/ArithmeticOp.java This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <fra...@us...> - 2009-05-16 19:56:14
|
Revision: 1525 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1525&view=rev Author: frankrimlinger Date: 2009-05-16 19:56:04 +0000 (Sat, 16 May 2009) Log Message: ----------- details of BackupAlg.phase1 migration. Prior to calling the SCANNER, the BackupAlg instance is created. In particular, the Instructions BadPlace, AbstractUconPlace, and OSplace are set up. I have decided not to use all caps for synthetic instruction classes anymore. The solution for one-pass graph construction is to use MethodInfo and Instruction objects as proxies for src and destination vertices in the call and total graphs, respectively. This allows the old Branch class to be retired, as edges are created immediately. Since updateTotalGraph is really doing a lot more than just the total graph, it is now called updateMangoModel So updateMangoModel is now only passed the src vertex, and provides one-stop shopping for all instructions. in particular, the Mango routines processReturn, processThrow, and processNativeCall now just bounce to updateTotalGraph The SCANNER pass must accomplish the equivalent functionality of BackupAlg.phaseI.CreateVertices() and LinkVertices(). So Mango. updateMangoModel does the following, only for src vertex. 1. if necessary, call BackupAlg.Method_2_vertices for the corresponding MethodInfo 2. call BackupAlg.instruction_2_vertices() for the src vertex, which becomes the peerVertex member of the src instruction. 3. call buildFormalPeer, creating the state transition and exit edges. Because we create the edges immediately, there is no need for a link phase. Instead of instantiating branches, just fold in the equivalent functionality of BackupAlg.instruction_link and BackupAlg.branch_link. If all goes well, the graphs we create should be acceptable input for phase2. But you will have to hotwire the 2d graph command so they can at least be inspected. 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/mangoModel/backupAlg/BackupAlg.java branches/mango/MangoJPF/Mango/src/mango/worker/msg/NewWorkerMsg.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/BranchChoiceGenerator.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/InvocationUtil.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/JSR.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/JSR_W.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/RET.java This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <fra...@us...> - 2009-05-16 23:54:32
|
Revision: 1526 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1526&view=rev Author: frankrimlinger Date: 2009-05-16 23:54:14 +0000 (Sat, 16 May 2009) Log Message: ----------- port of phase1 in progress. The old java model symbols have been reinstated. It is too early to try and phase them out. Instead, they must be ported so that they host the underlying jpf classes. Modified Paths: -------------- branches/mango/MangoJPF/Mango/src/mango/core/CoreRule.java branches/mango/MangoJPF/Mango/src/mango/ruleAction/coreRewriter/classModel/BuildAbstractUcon.java branches/mango/MangoJPF/Mango/src/mango/worker/Worker.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Invocation.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/backupAlg/BackupAlg.java Added Paths: ----------- branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/sym/ branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/sym/ClassSym.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/sym/InstructionSym.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/sym/InvocationSym.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/sym/JclassSym.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/sym/JfieldSym.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/sym/JmethodSym.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/sym/JnonclassSym.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/sym/ReturnPointLinkSym.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/sym/notes on access.rtf branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/sym/trick heap stuff.rtf 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/FakeMethod.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/OSmethod.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecodeSynthetic/AbstractUconPlace.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecodeSynthetic/BadPlace.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecodeSynthetic/OSplace.java This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <fra...@us...> - 2009-05-17 05:17:55
|
Revision: 1527 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1527&view=rev Author: frankrimlinger Date: 2009-05-17 05:17:30 +0000 (Sun, 17 May 2009) Log Message: ----------- Ported the Invocation class. This class generates the formal branch conditions for invocations, now based on the CodeSurvey and the bridge classes BranchUtil and ExceptionHandlerUtil. Also introduced bridge class InstructionUtil to help out with generating various names using existing mango api. Modified Paths: -------------- branches/mango/MangoJPF/Mango/src/mango/module/definition/method/MethodDefinitionManager.java branches/mango/MangoJPF/Mango/src/mango/source/agent/msg/SourceViewCreateRequestMsg.java branches/mango/MangoJPF/Mango/src/mango/worker/Worker.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Invocation.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Invoking.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/sym/InstructionSym.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/sym/InvocationSym.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/sym/JclassSym.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/sym/JfieldSym.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/sym/JmethodSym.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/sym/JnonclassSym.java branches/mango/MangoJPF/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashCoreParser.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/graphic/CodeSym.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/ucon/MethodEntrySym.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/vertex/CpnVertex.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 Added Paths: ----------- branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/sym/ClassSym.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/InstructionUtil.java Removed Paths: ------------- branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/sym/ClassSym.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/sym/ReturnPointLinkSym.java This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <fra...@us...> - 2009-05-18 04:39:08
|
Revision: 1529 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1529&view=rev Author: frankrimlinger Date: 2009-05-18 04:38:59 +0000 (Mon, 18 May 2009) Log Message: ----------- Bridge port for lots of broken code Added MethodUtil, ClassUtil classes. A porting pattern is emerging. Except in simple cases where direct translation is possible, add an adapter method to the appropriate bridge utility, rather than attempt an in-situ fix. This will localize the porting issues in the util classes. Added a concept of "mangoNative_packages" to indicate the code that will not be modelled by the backup algorithm. This is the latest reincarnation of the "library" concept. It is interesting that the concept of "native" is now three levels deep. porting createBadBranch, the issue is that we need to determine if we already branched to the badBranch from this vertex. So we need to know how to query the src Instruction to get its vertex to examine its outgoing edges. Modified Paths: -------------- branches/mango/MangoJPF/Mango/src/mango/graph/data/graphic/CodeData.java branches/mango/MangoJPF/Mango/src/mango/graph/data/graphic/MethodData.java branches/mango/MangoJPF/Mango/src/mango/graph/data/supervertex/SuperVertexData.java branches/mango/MangoJPF/Mango/src/mango/graph/data/ucon/UconData.java branches/mango/MangoJPF/Mango/src/mango/module/definition/loop/LoopDefinitionManager.java branches/mango/MangoJPF/Mango/src/mango/module/definition/loop/msg/LoopDefinitionLocatorMsg.java branches/mango/MangoJPF/Mango/src/mango/module/definition/method/MethodDefinitionManager.java branches/mango/MangoJPF/Mango/src/mango/module/definition/method/msg/CreateMethodStubMsg.java branches/mango/MangoJPF/Mango/src/mango/module/definition/method/msg/MethodDefinitionLocatorMsg.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/loop/model/LoopInstanceManager.java branches/mango/MangoJPF/Mango/src/mango/ruleAction/coreRewriter/classModel/BuildAbstractUcon.java branches/mango/MangoJPF/Mango/src/mango/ruleAction/coreRewriter/classModel/Checkcast.java branches/mango/MangoJPF/Mango/src/mango/ruleAction/coreRewriter/classModel/GetInterfaceRunTimeException.java branches/mango/MangoJPF/Mango/src/mango/ruleAction/coreRewriter/classModel/GetInterfaceRunTimeMethod.java branches/mango/MangoJPF/Mango/src/mango/ruleAction/coreRewriter/classModel/GetVirtualRunTimeException.java branches/mango/MangoJPF/Mango/src/mango/ruleAction/coreRewriter/classModel/GetVirtualRunTimeMethod.java branches/mango/MangoJPF/Mango/src/mango/ruleAction/coreRewriter/classModel/IsAssignmentCompatible.java branches/mango/MangoJPF/Mango/src/mango/ruleAction/coreRewriter/classModel/IsInterface.java branches/mango/MangoJPF/Mango/src/mango/ruleAction/coreRewriter/classModel/IsSuperClass.java branches/mango/MangoJPF/Mango/src/mango/ruleAction/coreRewriter/classModel/Is_class_loadable.java branches/mango/MangoJPF/Mango/src/mango/ruleAction/coreRewriter/clinit/CallThisClinit.java branches/mango/MangoJPF/Mango/src/mango/ruleAction/coreRewriter/clinit/ComposePrependedClinits.java branches/mango/MangoJPF/Mango/src/mango/ruleAction/translate/engine/AmbientLocal.java branches/mango/MangoJPF/Mango/src/mango/ruleAction/translate/engine/TranslateValueH.java branches/mango/MangoJPF/Mango/src/mango/ruleRequirement/linearArithmetic/ArithmeticLocalVar.java branches/mango/MangoJPF/Mango/src/mango/ruleRequirement/symbols/InstructionSymReq.java branches/mango/MangoJPF/Mango/src/mango/ruleRequirement/symbols/InvocationSymReq.java branches/mango/MangoJPF/Mango/src/mango/ruleRequirement/typing/ArithmeticFieldType.java branches/mango/MangoJPF/Mango/src/mango/ruleRequirement/typing/ArithmeticValue.java branches/mango/MangoJPF/Mango/src/mango/ruleRequirement/typing/IntegralArrayFieldType.java branches/mango/MangoJPF/Mango/src/mango/ruleRequirement/typing/IntegralFieldType.java branches/mango/MangoJPF/Mango/src/mango/source/agent/msg/SourceViewCreateRequestMsg.java branches/mango/MangoJPF/Mango/src/mango/worker/Worker.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Invocation.java branches/mango/MangoJPF/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashCoreParser.java branches/mango/MangoJPF/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashEngine.java branches/mango/MangoJPF/Mango/src/mango/worker/engine/rule/AssumeEquivRule.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/agent/CheckCast_getValueAgent.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/agent/IsAssignmentCompatibleAgent.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/backupAlg/BackupAlg.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/graphic/MethodSym.java branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/form/model/HeapModel.java branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/model/HitemUtil.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/BranchUtil.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/InstructionUtil.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/src/mango/intro/ConfigurationDetails.java branches/mango/MangoJPF/src/mango/intro/LoginDialog.java Added Paths: ----------- branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ClassUtil.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-05-18 18:47:25
|
Revision: 1531 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1531&view=rev Author: frankrimlinger Date: 2009-05-18 18:47:16 +0000 (Mon, 18 May 2009) Log Message: ----------- bridge port of type casting and branching instructions. Modified Paths: -------------- branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Branching.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Getandput.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Loading.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Newandmisc.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Return.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Storing.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/TypeCasting.java branches/mango/MangoJPF/bytecode cheat.txt 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/DCMPG.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DCMPL.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/FCMPG.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FCMPL.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/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/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/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/LCMP.java This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <fra...@us...> - 2009-05-19 05:57:50
|
Revision: 1533 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1533&view=rev Author: frankrimlinger Date: 2009-05-19 05:57:37 +0000 (Tue, 19 May 2009) Log Message: ----------- Interpolated the MangoInstruction class, a virtual version of InstructionUtil, between the jpf Instruction class and its direct extensions. This will allow the mango adapter code to take advantage of the jpf Instruction functionality. Also interpolated MangoFormalLanguage as an abstract class between MangoInstruction and Instruction, as this gives some technical advantages. You must now finish eliminated all the stale code in the ported formal bytecodes, as well as references to obsolete BranchUtil and InstructionUtil, which are now folded into virtual methods of MangoInstruction. Background: The decision to extend my bytecodes from the jpf bytecodes causes some trouble. The static adapter methods of InstructionUtil are growing in number and complexity, and have become an unacceptable violation of object oriented programming practice. Evidently I must now adapt a copy of package gov.nasa.jpf.jvm.bytecode as special purpose code that does not belong in the jpf kernel. This ugly duplication of code is the price paid for the elegance and simplicity of the MangoTargetLauncher. I did make attempts to extend my bytecodes directly from Instruction, but this led to lots of little and not so little problems. Abandoning jpf Instruction altogether is not an option, because mango now depends on this functionality. So for now, I just duplicate and adapt the gov.nasa.jpf.jvm.bytecode. If there is a better solution, well, let it come as it may. Modified Paths: -------------- branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Getandput.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Invocation.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Invoking.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Loading.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/LogicAndIntegerInc.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Newandmisc.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/PopDupSwap.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Pushing.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Return.java branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Storing.java branches/mango/MangoJPF/Mango/src/mango/worker/engine/hash/Hitem.java branches/mango/MangoJPF/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashEngine.java branches/mango/MangoJPF/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashOpcodeNames.java branches/mango/MangoJPF/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashOpcodeSyms.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/agent/InstanceOfAgent.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/backupAlg/BackupAlg.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/graph/LoopGraph.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/graphic/CodeSym.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/graphic/SuperVertexClassSym.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/reflection/StateSym.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/return_terminator/ReturnTerminatorSym.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/sink_terminator/SinkTerminatorSym.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/sink_terminator/ThrowSym.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/superVertex/SuperCpnSym.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/superVertex/SuperVertexSym.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/ucon/MethodEntrySym.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/ucon/UconOSTerminatorSym.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/ucon/UconSym.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/vertex/CpnVertex.java 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/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 branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecodeSynthetic/ACATCHHANDLER.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecodeSynthetic/ATHROWCREATOR.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecodeSynthetic/ATHROWHANDLER.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecodeSynthetic/AbstractUconPlace.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecodeSynthetic/BadPlace.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecodeSynthetic/OSplace.java Added Paths: ----------- branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Package.java branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/ branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/AALOAD.java branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/AASTORE.java branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/ACONST_NULL.java branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/ALOAD.java branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/ANEWARRAY.java branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/ARETURN.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/ASTORE.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/ArrayLoadInstruction.java branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/ArrayStoreInstruction.java branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/BALOAD.java branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/BASTORE.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/CALOAD.java branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/CASTORE.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/DALOAD.java branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/DASTORE.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/DLOAD.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/DRETURN.java branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/DSTORE.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/FALOAD.java branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/FASTORE.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/FLOAD.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/FRETURN.java branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/FSTORE.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/GETFIELD.java branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/GETSTATIC.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/GOTO_W.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/IALOAD.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/IASTORE.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/IFEQ.java branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/IFGE.java branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/IFGT.java branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/IFLE.java branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/IFLT.java branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/IFNE.java branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/IFNONNULL.java branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/IFNULL.java branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/IF_ACMPEQ.java branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/IF_ACMPNE.java branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/IF_ICMPEQ.java branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/IF_ICMPGE.java branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/IF_ICMPGT.java branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/IF_ICMPLE.java branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/IF_ICMPLT.java branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/IF_ICMPNE.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/ILOAD.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/INVOKECG.java branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/INVOKECLINIT.java branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/INVOKEINTERFACE.java branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/INVOKESPECIAL.java branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/INVOKESTATIC.java branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/INVOKEVIRTUAL.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/IRETURN.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/ISTORE.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/InstanceFieldInstruction.java branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/InvokeInstruction.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/LALOAD.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/LASTORE.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/LDC_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/LLOAD.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/LOOKUPSWITCH.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/LRETURN.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/LSTORE.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/LocalVariableInstruction.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/LongArrayLoadInstruction.java branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/LongArrayStoreInstruction.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/MangoFormalLanguage.java branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/MangoInstruction.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/PUTFIELD.java branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/PUTSTATIC.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/RETURN.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/SALOAD.java branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/SASTORE.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/StaticFieldInstruction.java branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/StoreInstruction.java branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/SwitchInstruction.java branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/TABLESWITCH.java branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/VariableAccessor.java branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/VirtualInvocation.java Removed Paths: ------------- branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/BranchUtil.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/InstructionUtil.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoFormalLanguage.java This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <fra...@us...> - 2009-05-19 16:03:50
|
Revision: 1535 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1535&view=rev Author: frankrimlinger Date: 2009-05-19 16:03:40 +0000 (Tue, 19 May 2009) Log Message: ----------- Cleanup for interpolated MangoInstruction class essentially complete, but a new issue has been identified. Unlike Instruction, there is no interpolating MethodInfo. So you have to package a MethodInfo in a MethodProxy extension of HiddenObject for the worker id system. See WorkerCommand class. Modified Paths: -------------- branches/mango/MangoJPF/Mango/src/mango/graph/data/graphic/CodeData.java branches/mango/MangoJPF/Mango/src/mango/graph/data/ucon/UconData.java branches/mango/MangoJPF/Mango/src/mango/module/definition/loop/LoopDefinitionManager.java branches/mango/MangoJPF/Mango/src/mango/module/definition/loop/msg/LoopDefinitionLocatorMsg.java branches/mango/MangoJPF/Mango/src/mango/module/instance/loop/model/LoopInstanceManager.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/graphic/CodeSym.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/reflection/StateSym.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/return_terminator/ReturnTerminatorSym.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/sink_terminator/SinkTerminatorSym.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/ucon/UconOSTerminatorSym.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/vertex/CpnVertex.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/vertex/SuperCpnVertex.java branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/coreTechniques/model/HeapTracer.java branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/form/model/LocalItemModel.java branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/form/model/OpItemModel.java branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/form/model/StackModel.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/FrameSym.java branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/form/sym/binder/executable/LocalVarSym.java branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/invariant/agent/LocalVarConditionalEquivalenceAgent.java branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/invariant/model/InvariantModel.java branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/msg/WorkerCommand.java branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/MangoInstruction.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-05-20 21:23:29
|
Revision: 1538 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1538&view=rev Author: frankrimlinger Date: 2009-05-20 21:23:18 +0000 (Wed, 20 May 2009) Log Message: ----------- Refactored MangoInstruction and MangoFormalLanguage, as these really belong in the mango.scanner package. Some delicate surgery on the phase1 code to hook it up properly to updateMangoModel(). Some code has been peeled away in a routine called buildSpecialEdges(), which handles some invocation related issues. The MangoInstruction.createXXXBranch methods are now just adaptors for BackupAlg.buildEdge(). It remains just to clean up and accommodate the MangoInstruction proxy for the Vertex dest field of and Edge. You must hot wire the rest of the automation driver for a specific target (i.e. itsAWrap.clear()) and test before proceeding to adapt phaseII to the new design. There are sure to be phase1 buggies to deal with. You don't want to debug phase1 and phase2 simultaneously. Modified Paths: -------------- branches/mango/MangoJPF/Mango/src/mango/graph/data/graphic/CodeData.java branches/mango/MangoJPF/Mango/src/mango/graph/data/ucon/UconData.java branches/mango/MangoJPF/Mango/src/mango/module/definition/loop/LoopDefinitionManager.java branches/mango/MangoJPF/Mango/src/mango/module/definition/loop/msg/LoopDefinitionLocatorMsg.java branches/mango/MangoJPF/Mango/src/mango/module/instance/loop/model/LoopInstanceManager.java branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/backupAlg/BackupAlg.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/graphic/CodeSym.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/graphic/InvocationEdgeSym.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/reflection/StateSym.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/return_terminator/ReturnTerminatorSym.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/sink_terminator/SinkTerminatorSym.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/ucon/UconOSTerminatorSym.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/vertex/CpnVertex.java branches/mango/MangoJPF/Mango/src/mango/worker/msg/NewWorkerMsg.java branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/ACONST_NULL.java branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/ANEWARRAY.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/INVOKECG.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/InvokeInstruction.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/LocalVariableInstruction.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/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/InvocationUtil.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/AALOAD.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/DCMPG.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DCMPL.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DDIV.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/DSUB.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/FCMPG.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FCMPL.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FDIV.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/FSUB.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/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/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/IMUL.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INEG.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IREM.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ISUB.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/LCMP.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LDIV.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/LREM.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LSUB.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecodeSynthetic/ACATCHHANDLER.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecodeSynthetic/ATHROWCREATOR.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecodeSynthetic/ATHROWHANDLER.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecodeSynthetic/AbstractUconPlace.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecodeSynthetic/BadPlace.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecodeSynthetic/OSplace.java Added Paths: ----------- branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoFormalLanguage.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInstruction.java Removed Paths: ------------- branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/MangoFormalLanguage.java branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/MangoInstruction.java This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <fra...@us...> - 2009-05-21 04:29:56
|
Revision: 1540 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1540&view=rev Author: frankrimlinger Date: 2009-05-21 04:29:42 +0000 (Thu, 21 May 2009) Log Message: ----------- Lots of EZ bridge cleanup. Also finished bridge port of ExceptionHandlerUtil.createACatchHandlerBranching. This is one fiendish piece of work. Ran into a little snag in that MethodInfo drops the ball concerning CodeExceptions for finally clauses. So I had to dig into bcel world to get this info. Modified Paths: -------------- branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/graph/Graph.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/graph/LoopGraph.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/graph/StrataGraph.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/return_terminator/ReturnTerminatorSym.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/sink_terminator/SinkTerminatorSym.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/sink_terminator/ThrowSym.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/superVertex/SuperVertexSym.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/ucon/AbstractUconSym.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/ucon/MethodEntrySym.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/ucon/UconOSTerminatorSym.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/vertex/AcyclicVertex.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/vertex/BackupVertex.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/vertex/CallVertex.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/vertex/CpnVertex.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/vertex/LoopVertex.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/vertex/MethodVertex.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/vertex/SuperCpnVertex.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/vertex/SuperVertex.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/vertex/Vertex.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/BranchChoiceGenerator.java 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/MangoInstruction.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MethodUtil.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecodeSynthetic/ACATCHHANDLER.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecodeSynthetic/ATHROWCREATOR.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecodeSynthetic/ATHROWHANDLER.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecodeSynthetic/AbstractUconPlace.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecodeSynthetic/BadPlace.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecodeSynthetic/INVOKETARGET.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecodeSynthetic/OSplace.java Added Paths: ----------- branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecodeSynthetic/SyntheticInstruction.java This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |
From: <fra...@us...> - 2009-05-21 15:03:01
|
Revision: 1541 http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1541&view=rev Author: frankrimlinger Date: 2009-05-21 15:02:53 +0000 (Thu, 21 May 2009) Log Message: ----------- All edge building logic has been ported. This is by far the trickiest step, so apparently the one-pass strategy is going to pan out. It remains to 1. transfer the required functionality in the old ClassParser.Instruction to MangoInstruction to complete the port of the BackupAlg, 2. port the required functionlity from the old ClassParser Method and ClassModel classes to MethodUtil and ClassUtil, resp, 3. finish porting the rest of the mango formal logic to the bridge bytecodes. Modified Paths: -------------- branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/backupAlg/BackupAlg.java branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/edge/Edge.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ExceptionHandlerUtil.java branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInstruction.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. |