[Javapathfinder-svn] SF.net SVN: javapathfinder: [845] branches/v5

[<pcm...@us...>]

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.