Menu
▾
▴
javapathfinder-svn
|
From: <pcm...@us...> - 2008-05-12 23:55:37
|
Revision: 845
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=845&view=rev
Author: pcmehlitz
Date: 2008-05-12 16:55:33 -0700 (Mon, 12 May 2008)
Log Message:
-----------
* all changes of current working copy vs. trunk head. This is the real base of the v5 branch.
The DynamicArea references have been replaced wherever there is no direct dependency of its
implementation, i.e. the Serializers/Restorers still need to be changed. Since we most
probably will change the ElementInfo management anyways (so that we don't reuse the same
ElementInfo object for different objects in different paths), this probably means the
existing Serializer/Restorer will have to be replaced. There will be only the default
classes, and they won't have to do any caching anymore, but that's one of the next steps.
ElementInfo still also holds the Area field, which has to go away
NOTE - the Heap interface will most likely still change. For now, it is just meant to be
a firewall against DynamicArea
Modified Paths:
--------------
branches/v5/.classpath
branches/v5/doc/home.html
branches/v5/doc/navigation.html
branches/v5/doc/news.html
branches/v5/env/jpf/gov/nasa/jpf/AnnotationProxyBase.java
branches/v5/env/jpf/gov/nasa/jpf/ConsoleOutputStream.java
branches/v5/env/jpf/java/lang/Class.java
branches/v5/env/jpf/java/lang/System.java
branches/v5/env/jvm/gov/nasa/jpf/jvm/JPF_java_io_InputStreamReader.java
branches/v5/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Class.java
branches/v5/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Integer.java
branches/v5/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Object.java
branches/v5/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_String.java
branches/v5/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Thread.java
branches/v5/env/jvm/gov/nasa/jpf/jvm/JPF_java_text_SimpleDateFormat.java
branches/v5/env/jvm/gov/nasa/jpf/jvm/JPF_java_util_Random.java
branches/v5/examples/ase2006/Optimizer.java
branches/v5/examples/ase2006/clean.java
branches/v5/examples/issta2006/BinTree/JPF_issta2006_BinTree_BinTree.java
branches/v5/examples/issta2006/BinTree/JPF_issta2006_BinTree_SymBinTree.java
branches/v5/examples/issta2006/BinomialHeap/JPF_issta2006_BinomialHeap_BinomialHeap.java
branches/v5/examples/issta2006/BinomialHeap/JPF_issta2006_BinomialHeap_SymBinomialHeap.java
branches/v5/examples/issta2006/FibHeap/JPF_issta2006_FibHeap_FibHeap.java
branches/v5/examples/issta2006/FibHeap/JPF_issta2006_FibHeap_SymFibHeap.java
branches/v5/examples/issta2006/TreeMap/JPF_issta2006_TreeMap_SymTreeMap.java
branches/v5/examples/issta2006/TreeMap/JPF_issta2006_TreeMap_TreeMap.java
branches/v5/examples/jpfESAS/launch/CV-assumptions-1-2.launch
branches/v5/examples/jpfESAS/launch/CV-generate-assumption-2.launch
branches/v5/examples/jpfESAS/script/generatedAssumption2
branches/v5/examples/k9/AbstractExecutive.java
branches/v5/examples/k9/AbstractTimePoint.java
branches/v5/examples/k9/Condition.java
branches/v5/examples/k9/Database.java
branches/v5/examples/k9/ExecConditionChecker.java
branches/v5/examples/k9/ExecTimer.java
branches/v5/examples/k9/ExecTimerWaiter.java
branches/v5/examples/k9/ExecWakeupTime.java
branches/v5/examples/k9/Executive.java
branches/v5/examples/k9/ExpandableListOfExecWakeupTimes.java
branches/v5/examples/k9/ListOfVariableBindings.java
branches/v5/examples/k9/Node.java
branches/v5/examples/k9/PlanParser.java
branches/v5/examples/k9/RuntimeExecutive.java
branches/v5/examples/k9/TimePoint.java
branches/v5/examples/launch/basic-random.launch
branches/v5/extensions/cv/examples/TestSafetyAutomaton.java
branches/v5/extensions/cv/src/gov/nasa/jpf/cv/AssertionFilteringListener.java
branches/v5/extensions/cv/src/gov/nasa/jpf/cv/ModularTeacher.java
branches/v5/extensions/cv/src/gov/nasa/jpf/cv/SCConformanceListener.java
branches/v5/extensions/cv/src/gov/nasa/jpf/cv/SCModularTeacher.java
branches/v5/extensions/cv/src/gov/nasa/jpf/cv/SCSafetyAutomaton.java
branches/v5/extensions/cv/src/gov/nasa/jpf/cv/SETLearner.java
branches/v5/extensions/cv/src/gov/nasa/jpf/cv/SafetyAutomaton.java
branches/v5/extensions/cv/src/gov/nasa/jpf/cv/SafetyListener.java
branches/v5/extensions/cv/src/gov/nasa/jpf/cv/TransitionsParser.java
branches/v5/extensions/cv/src/gov/nasa/jpf/tools/cv/ScRunCV.java
branches/v5/extensions/numeric/test/gov/nasa/jpf/numeric/TestNumeric.java
branches/v5/extensions/statechart/env/jpf/gov/nasa/jpf/sc/PendingEventQueue.java
branches/v5/extensions/statechart/env/jpf/gov/nasa/jpf/sc/State.java
branches/v5/extensions/statechart/env/jpf/gov/nasa/jpf/sc/StateMachine.java
branches/v5/extensions/statechart/env/jvm/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_sc_State.java
branches/v5/extensions/statechart/env/jvm/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_sc_StateMachine.java
branches/v5/extensions/statechart/env/jvm/gov/nasa/jpf/jvm/NativeStateMachine.java
branches/v5/extensions/statechart/examples/Ortho1.java
branches/v5/extensions/statechart/examples/Repeater.java
branches/v5/extensions/statechart/examples/SendEvents1.java
branches/v5/extensions/statechart/src/gov/nasa/jpf/jvm/choice/sc/SCEvent.java
branches/v5/extensions/statechart/src/gov/nasa/jpf/tools/sc/Coverage.java
branches/v5/extensions/statechart/src/gov/nasa/jpf/tools/sc/PathConstraint.java
branches/v5/extensions/statechart/src/gov/nasa/jpf/tools/sc/SimStateMachine.java
branches/v5/extensions/symbc/src/gov/nasa/jpf/symbc/SymbolicInstructionFactory.java
branches/v5/extensions/symbc/src/gov/nasa/jpf/symbc/SymbolicListener.java
branches/v5/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/BytecodeUtils.java
branches/v5/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/D2F.java
branches/v5/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/F2D.java
branches/v5/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/I2B.java
branches/v5/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/I2C.java
branches/v5/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/I2L.java
branches/v5/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/I2S.java
branches/v5/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/L2I.java
branches/v5/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/RealProblem.java
branches/v5/extensions/symbc/test/gov/nasa/jpf/symbc/ExSymExeDDIV.java
branches/v5/extensions/symbc/test/gov/nasa/jpf/symbc/ExSymExeI2D.java
branches/v5/extensions/symbc/test/gov/nasa/jpf/symbc/ExSymExeI2F.java
branches/v5/extensions/symbc/test/gov/nasa/jpf/symbc/PathConditionListener.java
branches/v5/extensions/symbc/test/gov/nasa/jpf/symbc/TestIntSpecial1.java
branches/v5/extensions/symbolic/src/gov/nasa/jpf/symbolic/array/ArrayIntCheckStructure.java
branches/v5/extensions/symbolic/src/gov/nasa/jpf/symbolic/integer/ConstraintBuilder.java
branches/v5/extensions/symbolic/src/gov/nasa/jpf/symbolic/integer/Expression.java
branches/v5/extensions/symbolic/src/gov/nasa/jpf/symbolic/integer/JPF_gov_nasa_jpf_symbolic_integer_SymbolicConstraintsSolver.java
branches/v5/extensions/symbolic/src/gov/nasa/jpf/symbolic/integer/Reconstruction.java
branches/v5/extensions/symbolic/src/gov/nasa/jpf/symbolic/integer/SymbolicConstraints.java
branches/v5/extensions/symbolic/src/gov/nasa/jpf/symbolic/integer/SymbolicFloat.java
branches/v5/extensions/symts/src/gov/nasa/jpf/ts/RWSameFieldRace.java
branches/v5/extensions/symts/src/gov/nasa/jpf/ts/RaceCandidate.java
branches/v5/extensions/symts/src/gov/nasa/jpf/ts/TSVM.java
branches/v5/extensions/undo/src/gov/nasa/jpf/jvm/UndoDynamicFactory.java
branches/v5/extensions/undo/src/gov/nasa/jpf/jvm/UndoRestorer.java
branches/v5/extensions/undo/src/gov/nasa/jpf/jvm/UndoStaticFactory.java
branches/v5/src/gov/nasa/jpf/Config.java
branches/v5/src/gov/nasa/jpf/JPF.java
branches/v5/src/gov/nasa/jpf/JPFException.java
branches/v5/src/gov/nasa/jpf/jvm/Area.java
branches/v5/src/gov/nasa/jpf/jvm/ArrayFields.java
branches/v5/src/gov/nasa/jpf/jvm/CachingSerializerDeserializer.java
branches/v5/src/gov/nasa/jpf/jvm/ChoicePoint.java
branches/v5/src/gov/nasa/jpf/jvm/ClassInfo.java
branches/v5/src/gov/nasa/jpf/jvm/CollapsingRestorer.java
branches/v5/src/gov/nasa/jpf/jvm/CollapsingSerializer.java
branches/v5/src/gov/nasa/jpf/jvm/DynamicArea.java
branches/v5/src/gov/nasa/jpf/jvm/ElementInfo.java
branches/v5/src/gov/nasa/jpf/jvm/ExceptionInfo.java
branches/v5/src/gov/nasa/jpf/jvm/Fields.java
branches/v5/src/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_jvm_Verify.java
branches/v5/src/gov/nasa/jpf/jvm/JVM.java
branches/v5/src/gov/nasa/jpf/jvm/KernelState.java
branches/v5/src/gov/nasa/jpf/jvm/MJIEnv.java
branches/v5/src/gov/nasa/jpf/jvm/MethodInfo.java
branches/v5/src/gov/nasa/jpf/jvm/Ref.java
branches/v5/src/gov/nasa/jpf/jvm/ReferenceFieldInfo.java
branches/v5/src/gov/nasa/jpf/jvm/RobustCollapsingSerializer.java
branches/v5/src/gov/nasa/jpf/jvm/SingleFieldLockInfo.java
branches/v5/src/gov/nasa/jpf/jvm/StackFrame.java
branches/v5/src/gov/nasa/jpf/jvm/StaticArea.java
branches/v5/src/gov/nasa/jpf/jvm/StaticElementInfo.java
branches/v5/src/gov/nasa/jpf/jvm/StatisticFieldLockInfo.java
branches/v5/src/gov/nasa/jpf/jvm/SystemState.java
branches/v5/src/gov/nasa/jpf/jvm/ThreadData.java
branches/v5/src/gov/nasa/jpf/jvm/ThreadInfo.java
branches/v5/src/gov/nasa/jpf/jvm/UncaughtException.java
branches/v5/src/gov/nasa/jpf/jvm/abstraction/abstractor/AbstractorBasedBuilder.java
branches/v5/src/gov/nasa/jpf/jvm/abstraction/filter/FilteringSerializer.java
branches/v5/src/gov/nasa/jpf/jvm/bytecode/ANEWARRAY.java
branches/v5/src/gov/nasa/jpf/jvm/bytecode/ARETURN.java
branches/v5/src/gov/nasa/jpf/jvm/bytecode/ARRAYLENGTH.java
branches/v5/src/gov/nasa/jpf/jvm/bytecode/ArrayLoadInstruction.java
branches/v5/src/gov/nasa/jpf/jvm/bytecode/ArrayStoreInstruction.java
branches/v5/src/gov/nasa/jpf/jvm/bytecode/CHECKCAST.java
branches/v5/src/gov/nasa/jpf/jvm/bytecode/GETFIELD.java
branches/v5/src/gov/nasa/jpf/jvm/bytecode/I2D.java
branches/v5/src/gov/nasa/jpf/jvm/bytecode/INSTANCEOF.java
branches/v5/src/gov/nasa/jpf/jvm/bytecode/INVOKECLINIT.java
branches/v5/src/gov/nasa/jpf/jvm/bytecode/INVOKEINTERFACE.java
branches/v5/src/gov/nasa/jpf/jvm/bytecode/INVOKESPECIAL.java
branches/v5/src/gov/nasa/jpf/jvm/bytecode/INVOKESTATIC.java
branches/v5/src/gov/nasa/jpf/jvm/bytecode/INVOKEVIRTUAL.java
branches/v5/src/gov/nasa/jpf/jvm/bytecode/InstanceFieldInstruction.java
branches/v5/src/gov/nasa/jpf/jvm/bytecode/InvokeInstruction.java
branches/v5/src/gov/nasa/jpf/jvm/bytecode/L2D.java
branches/v5/src/gov/nasa/jpf/jvm/bytecode/LDC.java
branches/v5/src/gov/nasa/jpf/jvm/bytecode/LDC_W.java
branches/v5/src/gov/nasa/jpf/jvm/bytecode/LockInstruction.java
branches/v5/src/gov/nasa/jpf/jvm/bytecode/MONITORENTER.java
branches/v5/src/gov/nasa/jpf/jvm/bytecode/MONITOREXIT.java
branches/v5/src/gov/nasa/jpf/jvm/bytecode/MULTIANEWARRAY.java
branches/v5/src/gov/nasa/jpf/jvm/bytecode/NEW.java
branches/v5/src/gov/nasa/jpf/jvm/bytecode/NEWARRAY.java
branches/v5/src/gov/nasa/jpf/jvm/bytecode/PUTFIELD.java
branches/v5/src/gov/nasa/jpf/jvm/bytecode/RUNSTART.java
branches/v5/src/gov/nasa/jpf/jvm/bytecode/ReturnInstruction.java
branches/v5/src/gov/nasa/jpf/jvm/bytecode/VirtualInvocation.java
branches/v5/src/gov/nasa/jpf/jvm/choice/DoubleSpec.java
branches/v5/src/gov/nasa/jpf/jvm/choice/IntSpec.java
branches/v5/src/gov/nasa/jpf/jvm/choice/TypedObjectChoice.java
branches/v5/src/gov/nasa/jpf/jvm/untracked/UntrackedManager.java
branches/v5/src/gov/nasa/jpf/report/ConsolePublisher.java
branches/v5/src/gov/nasa/jpf/report/Reporter.java
branches/v5/src/gov/nasa/jpf/search/DFSearch.java
branches/v5/src/gov/nasa/jpf/search/RandomSearch.java
branches/v5/src/gov/nasa/jpf/search/Search.java
branches/v5/src/gov/nasa/jpf/search/SearchListenerMulticaster.java
branches/v5/src/gov/nasa/jpf/search/Simulation.java
branches/v5/src/gov/nasa/jpf/test/Contract.java
branches/v5/src/gov/nasa/jpf/test/ContractContext.java
branches/v5/src/gov/nasa/jpf/test/ContractSpecLexer.java
branches/v5/src/gov/nasa/jpf/test/ContractSpecParser.java
branches/v5/src/gov/nasa/jpf/test/Operand.java
branches/v5/src/gov/nasa/jpf/test/Satisfies.java
branches/v5/src/gov/nasa/jpf/test/TestContext.java
branches/v5/src/gov/nasa/jpf/test/TestSpec.g
branches/v5/src/gov/nasa/jpf/test/TestSpecLexer.java
branches/v5/src/gov/nasa/jpf/test/TestSpecParser.java
branches/v5/src/gov/nasa/jpf/tools/AssertionProperty.java
branches/v5/src/gov/nasa/jpf/tools/ConstChecker.java
branches/v5/src/gov/nasa/jpf/tools/ContractVerifier.java
branches/v5/src/gov/nasa/jpf/tools/HeapTracker.java
branches/v5/src/gov/nasa/jpf/tools/MethodTester.java
branches/v5/src/gov/nasa/jpf/tools/ObjectTracker.java
branches/v5/src/gov/nasa/jpf/tools/PreciseRaceDetector.java
branches/v5/src/gov/nasa/jpf/tools/SearchMonitor.java
branches/v5/src/gov/nasa/jpf/tools/SearchStats.java
branches/v5/src/gov/nasa/jpf/tools/StateSpaceAnalyzer.java
branches/v5/src/gov/nasa/jpf/tools/StateSpaceDot.java
branches/v5/src/gov/nasa/jpf/tools/VarTracker.java
branches/v5/src/gov/nasa/jpf/util/IntTable.java
branches/v5/src/gov/nasa/jpf/util/Invocation.java
branches/v5/src/gov/nasa/jpf/util/JPFRunner.java
branches/v5/src/gov/nasa/jpf/util/LogManager.java
branches/v5/src/gov/nasa/jpf/util/Misc.java
branches/v5/src/gov/nasa/jpf/util/SparseClusterArray.java
branches/v5/src/gov/nasa/jpf/util/Trace.java
branches/v5/test/gov/nasa/jpf/embedded/TestSearchListener.java
branches/v5/test/gov/nasa/jpf/jvm/TestInvokeListenerJPF.java
branches/v5/test/gov/nasa/jpf/mc/TestVMDeadlock.java
branches/v5/test/gov/nasa/jpf/test/TestMethodTest.java
branches/v5/test/gov/nasa/jpf/test/TestSequence.java
Added Paths:
-----------
branches/v5/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Math.java
branches/v5/examples/issta2006/Linearizer.java
branches/v5/examples/issta2006/PredicateMap.java
branches/v5/extensions/statechart/env/jpf/gov/nasa/jpf/sc/EventSpec.java
branches/v5/extensions/statechart/examples/SyncEvents.java
branches/v5/extensions/symbc/lib/choco-1_2_04.jar
branches/v5/src/gov/nasa/jpf/jvm/Heap.java
branches/v5/src/gov/nasa/jpf/test/Fun.java
branches/v5/test/gov/nasa/jpf/test/MethodTest.launch
branches/v5/test/gov/nasa/jpf/test/ann-contracts.launch
branches/v5/test/gov/nasa/jpf/test/ann-requirements.launch
branches/v5/test/gov/nasa/jpf/test/ann-sequence.launch
branches/v5/test/gov/nasa/jpf/test/ann-test.launch
branches/v5/test/gov/nasa/jpf/test/anno-test-standalone.launch
Removed Paths:
-------------
branches/v5/choco-1_2_04.jar
branches/v5/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_MathOld.java
branches/v5/extensions/statechart/env/jpf/gov/nasa/jpf/sc/PendingEvent.java
branches/v5/src/gov/nasa/jpf/jvm/PredicateMap.java
branches/v5/src/gov/nasa/jpf/search/heuristic/UserHeuristic.java
branches/v5/src/gov/nasa/jpf/util/Debug.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-05-15 05:14:44
|
Revision: 847
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=847&view=rev
Author: pcmehlitz
Date: 2008-05-14 22:14:41 -0700 (Wed, 14 May 2008)
Log Message:
-----------
* revamped interrupt handling - interrupt status is actually more of a flag on the model side than it is
a ThreadInfo state. We still keep the INTERRUPTED state, but mostly for symmetry reasons (in analogy to
NOTIFIED or TIMEDOUT, i.e. representing a WAIT end condition), maybe it will go away (but make sure of
proper interrupt notification in this case!). The UNBLOCKED_INTERRUPT state is gone - waiters that got
interrupted now either go to to BLOCKED (if they can't re-acquire the lock), or to UNBLOCKED (if they can),
and we use the model field to determine if we have to throw an InterruptedException coming out of the wait.
Going into the wait, we skip the CG if there is a pending interrupt and directly throw. Since interrupt()
changes thread status, we turn it into a SchedulingPoint - this might cause some more states, but they are
required (other theads might become runnable at this point). The model flag carries some speed penalties, maybe
we have to move/shadow it to native, but w/o loosing backtrackability (what a word!)
This seems this solves Oksana's ThreadPoolTest example (java.util.concurrent.ExecutorService)
Still need to add the test cases tomorrow
* also finally added Elena's ThreadInfo.createThreadInfo() fix to prevent multiple occurrences of the same
ThreadInfo in the ThreadList (which is another relict) - thanks Elena
Modified Paths:
--------------
branches/v5/env/jpf/java/lang/Thread.java
branches/v5/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Object.java
branches/v5/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Thread.java
branches/v5/env/jvm/gov/nasa/jpf/jvm/JPF_sun_misc_Unsafe.java
branches/v5/src/gov/nasa/jpf/jvm/DefaultSchedulerFactory.java
branches/v5/src/gov/nasa/jpf/jvm/ElementInfo.java
branches/v5/src/gov/nasa/jpf/jvm/JVM.java
branches/v5/src/gov/nasa/jpf/jvm/Monitor.java
branches/v5/src/gov/nasa/jpf/jvm/SchedulerFactory.java
branches/v5/src/gov/nasa/jpf/jvm/ThreadInfo.java
branches/v5/src/gov/nasa/jpf/jvm/choice/ThreadChoiceFromSet.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-05-21 19:53:52
|
Revision: 852
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=852&view=rev
Author: pcmehlitz
Date: 2008-05-21 12:53:50 -0700 (Wed, 21 May 2008)
Log Message:
-----------
* replaced the UIActionGeneratorFactory with UIScriptEnvironment, ditched the XXGeneratorFactory classes. The loop
unrolling of the GeneratorFactory was actually broken in the UI model checking (JavaSeq)
(that was motivated by getting real world state changes for more profiling)
Modified Paths:
--------------
branches/v5/extensions/ui/env/jvm/gov/nasa/jpf/jvm/JPF_java_awt_EventDispatchThread.java
branches/v5/extensions/ui/src/gov/nasa/jpf/jvm/choice/ui/UIActionFromSet.java
branches/v5/extensions/ui/src/gov/nasa/jpf/jvm/choice/ui/UIActionSingleChoice.java
branches/v5/extensions/ui/src/gov/nasa/jpf/tools/UIInspector.java
branches/v5/src/gov/nasa/jpf/util/script/ScriptEnvironment.java
Added Paths:
-----------
branches/v5/extensions/ui/src/gov/nasa/jpf/jvm/choice/ui/UIScriptEnvironment.java
Removed Paths:
-------------
branches/v5/extensions/statechart/src/gov/nasa/jpf/jvm/choice/sc/SCEventGeneratorFactory.java
branches/v5/extensions/ui/src/gov/nasa/jpf/jvm/choice/ui/UIActionGeneratorFactory.java
branches/v5/src/gov/nasa/jpf/util/script/EventGeneratorFactory.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-05-28 16:55:18
|
Revision: 855
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=855&view=rev
Author: pcmehlitz
Date: 2008-05-28 09:55:16 -0700 (Wed, 28 May 2008)
Log Message:
-----------
* StateExtensionListener did throw an exception w/o state matching (state id = -1, we need
to turn off state matching in a more direct way, but that's part of the state mgnt rewrite anyways)
Modified Paths:
--------------
branches/v5/default.properties
branches/v5/extensions/statechart/examples/Repeat.es
branches/v5/extensions/statechart/examples/Repeater.java
branches/v5/src/gov/nasa/jpf/jvm/CollapsePools.java
branches/v5/src/gov/nasa/jpf/jvm/DynamicArea.java
branches/v5/src/gov/nasa/jpf/jvm/DynamicMapIndex.java
branches/v5/src/gov/nasa/jpf/jvm/ElementInfo.java
branches/v5/src/gov/nasa/jpf/jvm/abstraction/filter/FilteringSerializer.java
branches/v5/src/gov/nasa/jpf/jvm/bytecode/FieldInstruction.java
branches/v5/src/gov/nasa/jpf/jvm/bytecode/InvokeInstruction.java
branches/v5/src/gov/nasa/jpf/util/HashPool.java
branches/v5/src/gov/nasa/jpf/util/IntTable.java
branches/v5/src/gov/nasa/jpf/util/ObjVector.java
branches/v5/src/gov/nasa/jpf/util/StateExtensionListener.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-06-09 17:24:18
|
Revision: 860
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=860&view=rev
Author: pcmehlitz
Date: 2008-06-09 10:24:09 -0700 (Mon, 09 Jun 2008)
Log Message:
-----------
* added a static LogManager.setExternalOutput(OutputStream), which can be used if JPF runs embedded and we want to display log
output differently than System.out/err. Note that the provided OutputStream has to be closed explicitly by the calling
context
Modified Paths:
--------------
branches/v5/doc/about_us.html
branches/v5/env/jpf/java/lang/System.java
branches/v5/src/gov/nasa/jpf/util/LogHandler.java
branches/v5/src/gov/nasa/jpf/util/LogManager.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-06-12 17:42:17
|
Revision: 861
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=861&view=rev
Author: pcmehlitz
Date: 2008-06-12 10:42:13 -0700 (Thu, 12 Jun 2008)
Log Message:
-----------
* removed the state abstraction, the undo and the untracked field support for now. Some of this
might come back later, but it slows down the ElementInfo/Fields/Area refactoring, so it's better
to keep it off until this is done, and redesign with true delta state storage in mind. Next thing
to vanish is the Static/DynamicFields branch
Modified Paths:
--------------
branches/v5/.classpath
branches/v5/src/gov/nasa/jpf/jvm/Area.java
branches/v5/src/gov/nasa/jpf/jvm/DynamicElementInfo.java
branches/v5/src/gov/nasa/jpf/jvm/DynamicFields.java
branches/v5/src/gov/nasa/jpf/jvm/ElementInfo.java
branches/v5/src/gov/nasa/jpf/jvm/Fields.java
branches/v5/src/gov/nasa/jpf/jvm/StaticElementInfo.java
branches/v5/src/gov/nasa/jpf/jvm/StaticFields.java
Added Paths:
-----------
branches/v5/src/gov/nasa/jpf/jvm/ElementInfoContainer.java
Removed Paths:
-------------
branches/v5/extensions/undo/
branches/v5/src/gov/nasa/jpf/jvm/abstraction/AbstractingSerializer.java
branches/v5/src/gov/nasa/jpf/jvm/abstraction/DefaultStateGraphSerializer.java
branches/v5/src/gov/nasa/jpf/jvm/abstraction/StateGraph.java
branches/v5/src/gov/nasa/jpf/jvm/abstraction/StateGraphBuilder.java
branches/v5/src/gov/nasa/jpf/jvm/abstraction/StateGraphLinearizer.java
branches/v5/src/gov/nasa/jpf/jvm/abstraction/StateGraphSerializer.java
branches/v5/src/gov/nasa/jpf/jvm/abstraction/StateGraphTransform.java
branches/v5/src/gov/nasa/jpf/jvm/abstraction/abstractor/
branches/v5/src/gov/nasa/jpf/jvm/abstraction/linearization/
branches/v5/src/gov/nasa/jpf/jvm/abstraction/state/
branches/v5/src/gov/nasa/jpf/jvm/abstraction/symmetry/
branches/v5/src/gov/nasa/jpf/jvm/untracked/
branches/v5/test/gov/nasa/jpf/mc/TestUntrackedField.java
branches/v5/test/gov/nasa/jpf/mc/TestUntrackedFieldJPF.java
branches/v5/test/gov/nasa/jpf/peterd_tests/
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-06-13 05:31:11
|
Revision: 862
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=862&view=rev
Author: pcmehlitz
Date: 2008-06-12 22:31:09 -0700 (Thu, 12 Jun 2008)
Log Message:
-----------
* removed the Dynamic/StaticFields hierarchy, Fields now get directly instantiated. This seemed to be
appropriate to enable data type specific Fields, even though they are probably more suitable for
arrays, and we already have ArrayFields. But having type and role specific Fields hierarchies at the same
time is bad. The only place where the Dynamic/Static roles were required, was the setAttrs() - in
case the fields didn't have attrs yet it could create them on-the-fly. Now the ElementInfo.setXAttrs()
have to do this, which isn't ideal, but therefore we might save a superfluous clone (in case somebody
sets a null attribute value in an object that didn't have attrs yet)
* added Verify.get/setStaticFieldAttr() methods, just for completeness sake
Modified Paths:
--------------
branches/v5/src/gov/nasa/jpf/jvm/DefaultFieldsFactory.java
branches/v5/src/gov/nasa/jpf/jvm/DynamicArea.java
branches/v5/src/gov/nasa/jpf/jvm/ElementInfo.java
branches/v5/src/gov/nasa/jpf/jvm/Fields.java
branches/v5/src/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_jvm_Verify.java
branches/v5/src/gov/nasa/jpf/jvm/Verify.java
branches/v5/test/gov/nasa/jpf/jvm/TestAttrs.java
Removed Paths:
-------------
branches/v5/src/gov/nasa/jpf/jvm/DynamicFields.java
branches/v5/src/gov/nasa/jpf/jvm/StaticFields.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-06-14 01:31:17
|
Revision: 863
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=863&view=rev
Author: pcmehlitz
Date: 2008-06-13 18:31:09 -0700 (Fri, 13 Jun 2008)
Log Message:
-----------
* finally deArea'ed the ElementInfo, even though it required a new ElementInfoContainer interface that is factored
out / generalized from Heap. This was required so that we can re-use ElementInfo with non-Area heap implementations,
while still using StaticArea for the static fields
* changed the delta iteration of Area/ElementInfoContainer to have separate changedIterator(), removedIterator()
Iterators that return ElementInfos instead of reference values. Required if we want to do some inspection
on removed ElementInfos, like for instance delta storage (where we have to store the whole thing that got deleted)
* placeholders for "T Verify.getObject(Class<T> type,String cgId)", "T getReachableObject(Class<T> type,Object root)"
and Verify.getObject(). Esp. the last one is a real state space buster which I only regard as useful in very,
very special (read 'tiny') test apps. Still lacks the native peer implementation
Modified Paths:
--------------
branches/v5/src/gov/nasa/jpf/jvm/Area.java
branches/v5/src/gov/nasa/jpf/jvm/CollapsingRestorer.java
branches/v5/src/gov/nasa/jpf/jvm/CollapsingSerializer.java
branches/v5/src/gov/nasa/jpf/jvm/DynamicArea.java
branches/v5/src/gov/nasa/jpf/jvm/ElementInfo.java
branches/v5/src/gov/nasa/jpf/jvm/ElementInfoContainer.java
branches/v5/src/gov/nasa/jpf/jvm/Heap.java
branches/v5/src/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_jvm_Verify.java
branches/v5/src/gov/nasa/jpf/jvm/StaticElementInfo.java
branches/v5/src/gov/nasa/jpf/jvm/Verify.java
branches/v5/test/gov/nasa/jpf/mc/TestDataChoice.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-06-17 17:09:16
|
Revision: 871
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=871&view=rev
Author: pcmehlitz
Date: 2008-06-17 10:09:06 -0700 (Tue, 17 Jun 2008)
Log Message:
-----------
* changes in Fields/ElementInfo interface, to facilitate type specific ArrayFields, and centralize change
management in ElementInfo. Still needs more changes to accommodate per-field change flags. Fields/FieldInfo is
now more tightly coupled, but ElementInfo doesn't have to know about it
Modified Paths:
--------------
branches/v5/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_String.java
branches/v5/examples/issta2006/Linearizer.java
branches/v5/src/gov/nasa/jpf/jvm/Area.java
branches/v5/src/gov/nasa/jpf/jvm/ArrayFields.java
branches/v5/src/gov/nasa/jpf/jvm/ClassInfo.java
branches/v5/src/gov/nasa/jpf/jvm/DoubleFieldInfo.java
branches/v5/src/gov/nasa/jpf/jvm/DynamicArea.java
branches/v5/src/gov/nasa/jpf/jvm/ElementInfo.java
branches/v5/src/gov/nasa/jpf/jvm/ElementInfoContainer.java
branches/v5/src/gov/nasa/jpf/jvm/Fields.java
branches/v5/src/gov/nasa/jpf/jvm/FloatFieldInfo.java
branches/v5/src/gov/nasa/jpf/jvm/Heap.java
branches/v5/src/gov/nasa/jpf/jvm/IntegerFieldInfo.java
branches/v5/src/gov/nasa/jpf/jvm/LongFieldInfo.java
branches/v5/src/gov/nasa/jpf/jvm/MJIEnv.java
branches/v5/src/gov/nasa/jpf/jvm/ReferenceFieldInfo.java
branches/v5/src/gov/nasa/jpf/jvm/StaticElementInfo.java
branches/v5/src/gov/nasa/jpf/jvm/ThreadInfo.java
branches/v5/src/gov/nasa/jpf/jvm/abstraction/filter/FilteringSerializer.java
branches/v5/src/gov/nasa/jpf/jvm/abstraction/filter/SimpleFilteringSerializer.java
branches/v5/src/gov/nasa/jpf/jvm/bytecode/ArrayLoadInstruction.java
branches/v5/src/gov/nasa/jpf/jvm/bytecode/LongArrayStoreInstruction.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
×
Want the latest updates on software, tech news, and AI?
Get latest updates about software, tech news, and AI from SourceForge directly in your inbox once a month.
Thanks for helping keep SourceForge clean.
X