Menu
▾
▴
javapathfinder-devel
|
From: <pcm...@us...> - 2007-06-05 16:10:52
|
Revision: 351
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=351&view=rev
Author: pcmehlitz
Date: 2007-06-05 09:10:51 -0700 (Tue, 05 Jun 2007)
Log Message:
-----------
* don't change curEvent in StateMachine if it's only a completion (which does not require an event). The
implementation needs to be reworked though, since it's not backtracking/restore safe
* it's not UML, but with a slight modification, entryActions can now also do transitions. That's
to accomodate some of the "executable UML" dialects
* DFSHeuristic ctor was wrong
* CoverageAnalyzer should do some sanity checks on *.class files/jar entries before adding to
the set of analyzed classes
Modified Paths:
--------------
trunk/doc/links.html
trunk/extensions/statechart/env/jpf/gov/nasa/jpf/sc/StateMachine.java
trunk/extensions/statechart/env/jvm/gov/nasa/jpf/jvm/NativeStateMachine.java
trunk/extensions/statechart/src/gov/nasa/jpf/jvm/choice/sc/SCEvent.java
trunk/src/gov/nasa/jpf/search/heuristic/DFSHeuristic.java
trunk/src/gov/nasa/jpf/tools/CoverageAnalyzer.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-06-05 16:47:23
|
Revision: 352
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=352&view=rev
Author: pcmehlitz
Date: 2007-06-05 09:47:20 -0700 (Tue, 05 Jun 2007)
Log Message:
-----------
* active state carry over was wrong in last commit (only in case there was no
transition to a next state or end state, the current state has to be re-added
to the active set)
Modified Paths:
--------------
trunk/bin/jpf.bat
trunk/extensions/statechart/env/jpf/gov/nasa/jpf/sc/StateMachine.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-06-07 06:46:46
|
Revision: 354
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=354&view=rev
Author: pcmehlitz
Date: 2007-06-06 23:46:45 -0700 (Wed, 06 Jun 2007)
Log Message:
-----------
* big overhaul of java.lang.Throwable - this was motivated by the runtime costs of
unconditionally creating StackTraceElement[] arrays to keep (more or less) the
execution snapshot at the time of the Throwable creation. Only that in 99% the
StackTraceElements are not explicitly used (only implicitly with x.printStackTrace())
Now we store this much more efficiently and less lossy as an int[] array containing
the global method ids and pc offsets
this should esp. make a difference in applications that do a lot of explorative
reflection lookup (which produces tons of NoSuchMethodExceptions etc.)
* since we now model Throwable, also streamlined the InvocationTargetException
(the cause/target mess)
* for that purpose, added an unconditional MethodInfo.globalId, which is just a running
index into a static ArrayList (as opposed to the previous IntTable)
* to offset the additional memory, finally removed the isStatic, isPublic, isSynchronized, isNative
attribute fields (which are all in modifiers anyways). Should actually save memory
Modified Paths:
--------------
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Throwable.java
trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
trunk/src/gov/nasa/jpf/jvm/MethodInfo.java
trunk/src/gov/nasa/jpf/jvm/ThreadInfo.java
trunk/src/gov/nasa/jpf/report/ConsolePublisher.java
Added Paths:
-----------
trunk/env/jpf/java/lang/Throwable.java
trunk/env/jpf/java/lang/reflect/InvocationTargetException.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-06-07 23:16:06
|
Revision: 355
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=355&view=rev
Author: pcmehlitz
Date: 2007-06-07 16:16:04 -0700 (Thu, 07 Jun 2007)
Log Message:
-----------
* extended and updated the HeapTracker, which is now a PublisherExtension
and can report type allocation statistics. type filtering is now also
done with the StringSetMatcher (includes/excludes pattern)
the reason is that JavaSeq is broken with OutOfMemory, which must be some
standrad library modeling that's used from within Swing, and we have to
find out what it is. Unfortunately, Publisher isn't yet aware of OutOfMemory
(we need a property for that)
* PropertyListenerAdapter wasn't a PublisherExtension
* added the demo case to TestRandom
* updated the "Running JPF.." page, since -show is gone
Modified Paths:
--------------
trunk/doc/Running_JPF.html
trunk/src/gov/nasa/jpf/PropertyListenerAdapter.java
trunk/src/gov/nasa/jpf/tools/HeapTracker.java
trunk/test/gov/nasa/jpf/mc/TestRandom.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-06-09 02:12:26
|
Revision: 356
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=356&view=rev
Author: pcmehlitz
Date: 2007-06-08 19:12:25 -0700 (Fri, 08 Jun 2007)
Log Message:
-----------
* OUTCH - apparently, at least the Eclipse compiler does change slot types, and we didn't
reset the reference flag when setting long values. This caused JavaSeq to run into an
OutOfMemoryError that was cause by the mark phase (trying to set the mark bit for a
ridiculously large reference value). That was a tough one to debug
* publishFinished even if we run out of memory - there might be listeners configured
that give us a better idea how far we got
Modified Paths:
--------------
trunk/extensions/ui/src/gov/nasa/jpf/tools/UIInspector.java
trunk/src/gov/nasa/jpf/JPF.java
trunk/src/gov/nasa/jpf/jvm/DynamicArea.java
trunk/src/gov/nasa/jpf/jvm/StackFrame.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-06-12 23:19:03
|
Revision: 357
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=357&view=rev
Author: pcmehlitz
Date: 2007-06-12 16:19:00 -0700 (Tue, 12 Jun 2007)
Log Message:
-----------
* the big change is that statechart guidance scripts are now instance (field) based, i.e.
we don't use the class names anymore to look up events. This was required because
the executable UML dialects require multiple instances of the same state (which are
'state machines' in their notation), and we would not have been able to write
guidance scripts for that. Recursive lookup through the hierarchy chain of states
still applies.
* to extend this, we now can also have arrays of states, which are named by
appending the subscript (in square brackets) to the array name. Also added a
little Array1 example for this
* a guidance script SECTION can now how have a comma separated list of IDs, to
specify event sequences for unrelated states
* added a preliminary (and very raw) guidance script documentation file
* the extension/statechart/build.xml was broken because we have an inverted
dependency chain. That's bad, and the fix in build.xml is bad too, but it
will take some time to reshuffle things, and the problem does not occur inside
Eclipse anyways
There soon will be a more elaborate 'jpfESAS' example for the statechart extension
Modified Paths:
--------------
trunk/default.properties
trunk/extensions/statechart/build.xml
trunk/extensions/statechart/doc/translation-rules.txt
trunk/extensions/statechart/env/jpf/gov/nasa/jpf/sc/State.java
trunk/extensions/statechart/env/jpf/gov/nasa/jpf/sc/StateMachine.java
trunk/extensions/statechart/env/jvm/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_sc_State.java
trunk/extensions/statechart/env/jvm/gov/nasa/jpf/jvm/NativeStateMachine.java
trunk/extensions/statechart/examples/FixedPhone.es
trunk/extensions/statechart/src/gov/nasa/jpf/jvm/choice/sc/SCEventGeneratorFactory.java
trunk/extensions/statechart/src/gov/nasa/jpf/tools/sc/Coverage.java
trunk/extensions/statechart/src/gov/nasa/jpf/tools/sc/PathConstraint.java
trunk/extensions/statechart/src/gov/nasa/jpf/tools/sc/SimStateMachine.java
trunk/src/gov/nasa/jpf/jvm/DynamicArea.java
trunk/src/gov/nasa/jpf/jvm/FieldInfo.java
trunk/src/gov/nasa/jpf/jvm/bytecode/Instruction.java
trunk/src/gov/nasa/jpf/util/script/ESParser.java
trunk/src/gov/nasa/jpf/util/script/Section.java
trunk/src/gov/nasa/jpf/util/script/StringSetGenerator.java
Added Paths:
-----------
trunk/extensions/statechart/doc/guidance-scripts.txt
trunk/extensions/statechart/examples/Array1.es
trunk/extensions/statechart/examples/Array1.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-06-20 22:45:41
|
Revision: 365
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=365&view=rev
Author: pcmehlitz
Date: 2007-06-20 15:45:38 -0700 (Wed, 20 Jun 2007)
Log Message:
-----------
* the big change is an overhaul and completion of the Stackframe attribute system.
attribute references for locals and operands are only added on demand, i.e. are
not allocated by default. Once they are there, xLOAD/xSTORE and all the operand stack
ops update attributes automatically (i.e. copy between stack and operands etc.). Using
the attributes needs more testing though
* this required some changes in the StackFrame interface (as exposed by ThreadInfo), to
better accomodate the xLOAD/xSTORE insns
* added some public StackFrame accessors for attributes and operand/local values
* various little bugs reg. Throwable (e.g. a missing native toString())
* changed the RawTest interface = we only support calling one test method at a time,
but with optional String/int/double/boolean parameters. This also wraps InvocationTargetExceptions
into RuntimeExceptions, so that RawTest main() methods don't have to declare exception anymore.
Updated a bunh of tests accordingly
* some obsolete Debug cleanup
Modified Paths:
--------------
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Throwable.java
trunk/extensions/numeric/test/gov/nasa/jpf/numeric/TestNumeric.java
trunk/src/gov/nasa/jpf/jvm/DirectCallStackFrame.java
trunk/src/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_jvm_Verify.java
trunk/src/gov/nasa/jpf/jvm/JVM.java
trunk/src/gov/nasa/jpf/jvm/KernelState.java
trunk/src/gov/nasa/jpf/jvm/MethodInfo.java
trunk/src/gov/nasa/jpf/jvm/StackFrame.java
trunk/src/gov/nasa/jpf/jvm/ThreadInfo.java
trunk/src/gov/nasa/jpf/jvm/Verify.java
trunk/src/gov/nasa/jpf/jvm/bytecode/ALOAD.java
trunk/src/gov/nasa/jpf/jvm/bytecode/ASTORE.java
trunk/src/gov/nasa/jpf/jvm/bytecode/DLOAD.java
trunk/src/gov/nasa/jpf/jvm/bytecode/DSTORE.java
trunk/src/gov/nasa/jpf/jvm/bytecode/FLOAD.java
trunk/src/gov/nasa/jpf/jvm/bytecode/FSTORE.java
trunk/src/gov/nasa/jpf/jvm/bytecode/ILOAD.java
trunk/src/gov/nasa/jpf/jvm/bytecode/INVOKESTATIC.java
trunk/src/gov/nasa/jpf/jvm/bytecode/ISTORE.java
trunk/src/gov/nasa/jpf/jvm/bytecode/LLOAD.java
trunk/src/gov/nasa/jpf/jvm/bytecode/LSTORE.java
trunk/src/gov/nasa/jpf/jvm/bytecode/LocalVariableInstruction.java
trunk/src/gov/nasa/jpf/jvm/bytecode/NEW.java
trunk/test/gov/nasa/jpf/jvm/RawTest.java
trunk/test/gov/nasa/jpf/jvm/TestFileIO.java
trunk/test/gov/nasa/jpf/jvm/TestJavaLangString.java
trunk/test/gov/nasa/jpf/jvm/TestNativePeer.java
trunk/test/gov/nasa/jpf/jvm/TestNativePeerJPF.java
trunk/test/gov/nasa/jpf/mc/TestRace.java
trunk/test/gov/nasa/jpf/mc/TestRandom.java
trunk/test/gov/nasa/jpf/mc/TestRandomJPF.java
trunk/test/gov/nasa/jpf/mc/TestVMDeadlock.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-06-22 06:09:12
|
Revision: 381
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=381&view=rev
Author: pcmehlitz
Date: 2007-06-21 23:09:09 -0700 (Thu, 21 Jun 2007)
Log Message:
-----------
* fix for the famous "Oksana bug" - due to the (bad) nature of the heap symmetry (DynamicMapIndex),
there actually were situations where the InvokeVirtual method caching did not work. It required the
same INVOKEVIRTUAL insn to get the same reference value for different objects, which in turn
requires the same allocation insn for different objects. Alternatively, any combination of
DynamicMapIndex inputs causing the same reference value (but that's probably even harder).
now we cache the callee ClassInfo. Slightly slower, but safe, and still saves us the (recursive) method
lookup if it's a match
* created a TestMethod test case, which in turn required to implement Runtime.gc() to force a GC
* extended the ObjectTracker so that invokes and gets are only printed as an option
Modified Paths:
--------------
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Runtime.java
trunk/src/gov/nasa/jpf/jvm/MJIEnv.java
trunk/src/gov/nasa/jpf/jvm/bytecode/VirtualInvocation.java
trunk/src/gov/nasa/jpf/tools/ObjectTracker.java
trunk/test/gov/nasa/jpf/jvm/TestMethod.java
trunk/test/gov/nasa/jpf/jvm/TestMethodJPF.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-06-27 00:16:02
|
Revision: 395
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=395&view=rev
Author: pcmehlitz
Date: 2007-06-26 17:15:59 -0700 (Tue, 26 Jun 2007)
Log Message:
-----------
* first installment of the Annotation replacement. We now don't use the real annotations anymore,
but model them as AnnotationInfo (created from bcel AnnotationEntries). The main reason for this is
to avoid having to put model types (like the statechart @Params) in the CLASSPATH.
AnnotationLoader/LoadedAnnotations are gone.
reflection support for Annotations (i.e. use in the application) still needs to be done. For now
we are mostly concerned about using annotations to specify JPF properties.
* updated bcel to the latest and greatest for the annotation support
* extended the ObjectTracker to check for @NonShared annotations - if a monitored object that has such
a class annotation is called or modified in another thread than its creator, we report a property
violation
* added a simple TestAnnotationProperties to the regression tests
* factored AnnotationSupport into a InfoObject class, which is the root for ClassInfo, MethodInfo, FieldInfo
* added a generic TestJPF.runJPFError() method
* added some post exec info to MONITOR instructions
Modified Paths:
--------------
trunk/env/jpf/java/lang/Class.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Class.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_reflect_Method.java
trunk/extensions/statechart/env/jvm/gov/nasa/jpf/jvm/NativeStateMachine.java
trunk/lib/bcel.jar
trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
trunk/src/gov/nasa/jpf/jvm/ElementInfo.java
trunk/src/gov/nasa/jpf/jvm/FieldInfo.java
trunk/src/gov/nasa/jpf/jvm/JVM.java
trunk/src/gov/nasa/jpf/jvm/MethodInfo.java
trunk/src/gov/nasa/jpf/jvm/abstraction/filter/IgnoresFromAnnotations.java
trunk/src/gov/nasa/jpf/jvm/abstraction/filter/IncludesFromAnnotations.java
trunk/src/gov/nasa/jpf/jvm/bytecode/MONITORENTER.java
trunk/src/gov/nasa/jpf/jvm/bytecode/MONITOREXIT.java
trunk/src/gov/nasa/jpf/tools/ExecTracker.java
trunk/src/gov/nasa/jpf/tools/ObjectTracker.java
trunk/test/gov/nasa/jpf/jvm/TestJPF.java
Added Paths:
-----------
trunk/env/jpf/gov/nasa/jpf/NonShared.java
trunk/src/gov/nasa/jpf/jvm/AnnotationInfo.java
trunk/src/gov/nasa/jpf/jvm/InfoObject.java
trunk/src/gov/nasa/jpf/jvm/bytecode/LockInstruction.java
trunk/test/gov/nasa/jpf/mc/TestAnnotationProperties.java
trunk/test/gov/nasa/jpf/mc/TestAnnotationPropertiesJPF.java
Removed Paths:
-------------
trunk/src/gov/nasa/jpf/jvm/AnnotationLoader.java
trunk/src/gov/nasa/jpf/jvm/LoadedAnnotations.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-06-27 19:50:35
|
Revision: 403
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=403&view=rev
Author: pcmehlitz
Date: 2007-06-27 12:50:33 -0700 (Wed, 27 Jun 2007)
Log Message:
-----------
* added a @Const annotation, together with a +ot.check_const option for the
ObjectTracker. It checks for PUTFIELDS from @Const marked methods
we could also do this deep, which would be cool
* restructured the ObjectTracker to make it a bit more generic
* extended the TestAnnotation regression tests for it
* yet again - some output formatting to enable source links from an Eclipse console
* some update in the TestNumeric reg tests (no throws in main())
Modified Paths:
--------------
trunk/extensions/numeric/test/gov/nasa/jpf/numeric/TestNumeric.java
trunk/extensions/numeric/test/gov/nasa/jpf/numeric/TestNumericJPF.java
trunk/src/gov/nasa/jpf/jvm/StackFrame.java
trunk/src/gov/nasa/jpf/tools/ObjectTracker.java
trunk/test/gov/nasa/jpf/mc/TestAnnotationProperties.java
trunk/test/gov/nasa/jpf/mc/TestAnnotationPropertiesJPF.java
Added Paths:
-----------
trunk/env/jpf/gov/nasa/jpf/Const.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-06-27 21:00:37
|
Revision: 405
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=405&view=rev
Author: pcmehlitz
Date: 2007-06-27 14:00:36 -0700 (Wed, 27 Jun 2007)
Log Message:
-----------
* added .../test and .../examples subdirs for extension/symbc
Modified Paths:
--------------
trunk/.classpath
Added Paths:
-----------
trunk/extensions/symbc/examples/
trunk/extensions/symbc/test/
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-06-28 23:31:12
|
Revision: 419
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=419&view=rev
Author: pcmehlitz
Date: 2007-06-28 16:31:08 -0700 (Thu, 28 Jun 2007)
Log Message:
-----------
* basic field attributes. arrays still need to be done
* forgot to propagate attributes in RETURN insns. not yet tested for long slots
* added a reg test for attribute propagation. does not cover statics or longs yet
* some more attribute accessors in ThreadInfo, icluding versions that do not
clone the top frame, which isn't necessary of we also changed a local/operand value
* added link to the practicioners guidebook
Modified Paths:
--------------
trunk/doc/JPF_Related_Papers.html
trunk/src/gov/nasa/jpf/jvm/ElementInfo.java
trunk/src/gov/nasa/jpf/jvm/Fields.java
trunk/src/gov/nasa/jpf/jvm/ThreadInfo.java
trunk/src/gov/nasa/jpf/jvm/bytecode/GETFIELD.java
trunk/src/gov/nasa/jpf/jvm/bytecode/GETSTATIC.java
trunk/src/gov/nasa/jpf/jvm/bytecode/IRETURN.java
trunk/src/gov/nasa/jpf/jvm/bytecode/PUTFIELD.java
trunk/src/gov/nasa/jpf/jvm/bytecode/PUTSTATIC.java
trunk/src/gov/nasa/jpf/jvm/bytecode/RETURN.java
trunk/src/gov/nasa/jpf/jvm/bytecode/ReturnInstruction.java
Added Paths:
-----------
trunk/test/gov/nasa/jpf/jvm/TestAttrs.java
trunk/test/gov/nasa/jpf/jvm/TestAttrsJPF.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-06-29 22:19:40
|
Revision: 422
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=422&view=rev
Author: pcmehlitz
Date: 2007-06-29 15:19:25 -0700 (Fri, 29 Jun 2007)
Log Message:
-----------
* tested and fixed long/double attributes. There is a snag - we have to decide whether to store
the attribute on the first or the second word (attributes for frames are kept per-slot, since
we don't have type info at all the bytecode ops). Since the StackFrame.getLocalVariableIndex()
returns the lower index, we choose this one. But that means we have to explicitly use
setLongOperandAttr()/getLongOperandAttr() to access double word attributes
* added the corresponding accessors to ThreadInfo
* extended TestAttrs with statics and doubles
* added two more SystemState attributes: 'isForced' means we always treat this as a new state,
'retainAttributes' means we don't reset the attributes at each nextSucessor() call (i.e. Listeners
can switch matching on/off). Also made the existing attributes mutually exclusive (isForced/isIgnored,
isInteresting/isBoring). Added accessors in both SystemState and JVM
Modified Paths:
--------------
trunk/src/gov/nasa/jpf/jvm/JVM.java
trunk/src/gov/nasa/jpf/jvm/StackFrame.java
trunk/src/gov/nasa/jpf/jvm/SystemState.java
trunk/src/gov/nasa/jpf/jvm/ThreadInfo.java
trunk/src/gov/nasa/jpf/jvm/bytecode/D2I.java
trunk/src/gov/nasa/jpf/jvm/bytecode/D2L.java
trunk/src/gov/nasa/jpf/jvm/bytecode/DRETURN.java
trunk/src/gov/nasa/jpf/jvm/bytecode/I2D.java
trunk/src/gov/nasa/jpf/jvm/bytecode/I2L.java
trunk/src/gov/nasa/jpf/jvm/bytecode/L2D.java
trunk/src/gov/nasa/jpf/jvm/bytecode/LRETURN.java
trunk/src/gov/nasa/jpf/jvm/bytecode/ReturnInstruction.java
trunk/test/gov/nasa/jpf/jvm/TestAttrs.java
trunk/test/gov/nasa/jpf/jvm/TestAttrsJPF.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-07-02 20:39:28
|
Revision: 424
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=424&view=rev
Author: pcmehlitz
Date: 2007-07-02 13:39:27 -0700 (Mon, 02 Jul 2007)
Log Message:
-----------
* added a GenericInstructionFactory, and refactored NumericInstructionFactory accordingly. Rationale is
to simplify creation of extensions that have their own execution modes (like various flavors of
symbolic execution)
Modified Paths:
--------------
trunk/extensions/numeric/src/gov/nasa/jpf/numeric/NumericInstructionFactory.java
Added Paths:
-----------
trunk/src/gov/nasa/jpf/util/GenericInstructionFactory.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-07-11 02:07:48
|
Revision: 434
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=434&view=rev
Author: pcmehlitz
Date: 2007-07-10 19:07:47 -0700 (Tue, 10 Jul 2007)
Log Message:
-----------
* refactored the InvokeInstruction observability, esp. the getArgumentValues(), which was broken for
MJI methods. The problem is that NativePeer.executeMethod() returns with the callers stack modified
(args popped, return pushed), so an instructionExecuted had no way to determine what the call args
were. The current way of using the static NativePeer cache is the lesser of n evils, since it shouldn't
impose too much performance penalty to normal insns. Still this behavioral combinatorial snake pit of
instance/static JPF/MJI pre-/post- exec notification is not nice. There are probably some other
insns out there (fields) that still have to be made consistent too
* added some tests for this
* to aggravate this, added an INVOKECG pseudo-insn that can be used to obtain a method to call
from a InvocationCG, with an Invocation being the abstraction of a call. This will be used esp.
in drivers that require other entries than main() (like the upcoming thread-safe symbolic execution)
Modified Paths:
--------------
trunk/extensions/numeric/src/gov/nasa/jpf/numeric/NumericInstructionFactory.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/SymbolicListener.java
trunk/src/gov/nasa/jpf/jvm/JVM.java
trunk/src/gov/nasa/jpf/jvm/MethodInfo.java
trunk/src/gov/nasa/jpf/jvm/NativePeer.java
trunk/src/gov/nasa/jpf/jvm/StackFrame.java
trunk/src/gov/nasa/jpf/jvm/SystemState.java
trunk/src/gov/nasa/jpf/jvm/ThreadInfo.java
trunk/src/gov/nasa/jpf/jvm/bytecode/INVOKECLINIT.java
trunk/src/gov/nasa/jpf/jvm/bytecode/INVOKESTATIC.java
trunk/src/gov/nasa/jpf/jvm/bytecode/Instruction.java
trunk/src/gov/nasa/jpf/jvm/bytecode/InvokeInstruction.java
trunk/src/gov/nasa/jpf/jvm/bytecode/VirtualInvocation.java
trunk/src/gov/nasa/jpf/tools/CallMonitor.java
trunk/src/gov/nasa/jpf/tools/ChoiceSelector.java
trunk/src/gov/nasa/jpf/tools/MethodTracker.java
trunk/src/gov/nasa/jpf/tools/ObjectTracker.java
trunk/src/gov/nasa/jpf/util/GenericInstructionFactory.java
Added Paths:
-----------
trunk/src/gov/nasa/jpf/jvm/bytecode/INVOKECG.java
trunk/src/gov/nasa/jpf/jvm/choice/InvocationCG.java
trunk/src/gov/nasa/jpf/util/Invocation.java
trunk/test/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_jvm_TestInvokeListener.java
trunk/test/gov/nasa/jpf/jvm/TestInvokeListener.java
trunk/test/gov/nasa/jpf/jvm/TestInvokeListenerJPF.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-07-11 23:34:04
|
Revision: 435
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=435&view=rev
Author: pcmehlitz
Date: 2007-07-11 16:34:02 -0700 (Wed, 11 Jul 2007)
Log Message:
-----------
* wow, bug in Class.asSubclass(), which caused JUnit 4.3 to fail. Amazing how long this can
go undetected. Added related regression tests
Modified Paths:
--------------
trunk/env/jpf/java/lang/Class.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Class.java
trunk/test/gov/nasa/jpf/jvm/TestJavaLangClass.java
trunk/test/gov/nasa/jpf/jvm/TestJavaLangClassJPF.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-07-17 00:35:35
|
Revision: 439
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=439&view=rev
Author: pcmehlitz
Date: 2007-07-16 17:35:33 -0700 (Mon, 16 Jul 2007)
Log Message:
-----------
* the MethodInfo caching in VirtualInvocation was still broken (in case the callee ClassInfo was
not different, the lastObj reference was not updated). How hard can it be..
* all the explicit MethodInfo creators have to use the InstructionFactory, which for this purpose
had to be extended with a generic create(clsName). Be aware of that users have to initailze these
Instruction objects explicitly!
There are probably still some explicitly created Instruction objects that don't use the factory,
but at least the reflection call stub should do
Modified Paths:
--------------
trunk/extensions/cv/src/gov/nasa/jpf/cv/AssertionFilteringListener.java
trunk/src/gov/nasa/jpf/jvm/DefaultInstructionFactory.java
trunk/src/gov/nasa/jpf/jvm/ElementInfo.java
trunk/src/gov/nasa/jpf/jvm/InstructionFactory.java
trunk/src/gov/nasa/jpf/jvm/MJIEnv.java
trunk/src/gov/nasa/jpf/jvm/MethodInfo.java
trunk/src/gov/nasa/jpf/jvm/bytecode/IFEQ.java
trunk/src/gov/nasa/jpf/jvm/bytecode/IFGE.java
trunk/src/gov/nasa/jpf/jvm/bytecode/IFGT.java
trunk/src/gov/nasa/jpf/jvm/bytecode/IFLE.java
trunk/src/gov/nasa/jpf/jvm/bytecode/IFLT.java
trunk/src/gov/nasa/jpf/jvm/bytecode/IFNE.java
trunk/src/gov/nasa/jpf/jvm/bytecode/IFNONNULL.java
trunk/src/gov/nasa/jpf/jvm/bytecode/IFNULL.java
trunk/src/gov/nasa/jpf/jvm/bytecode/IF_ACMPEQ.java
trunk/src/gov/nasa/jpf/jvm/bytecode/IF_ACMPNE.java
trunk/src/gov/nasa/jpf/jvm/bytecode/IF_ICMPEQ.java
trunk/src/gov/nasa/jpf/jvm/bytecode/IF_ICMPGE.java
trunk/src/gov/nasa/jpf/jvm/bytecode/IF_ICMPGT.java
trunk/src/gov/nasa/jpf/jvm/bytecode/IF_ICMPLE.java
trunk/src/gov/nasa/jpf/jvm/bytecode/IF_ICMPLT.java
trunk/src/gov/nasa/jpf/jvm/bytecode/IF_ICMPNE.java
trunk/src/gov/nasa/jpf/jvm/bytecode/INVOKECG.java
trunk/src/gov/nasa/jpf/jvm/bytecode/INVOKECLINIT.java
trunk/src/gov/nasa/jpf/jvm/bytecode/INVOKEINTERFACE.java
trunk/src/gov/nasa/jpf/jvm/bytecode/INVOKESPECIAL.java
trunk/src/gov/nasa/jpf/jvm/bytecode/INVOKESTATIC.java
trunk/src/gov/nasa/jpf/jvm/bytecode/INVOKEVIRTUAL.java
trunk/src/gov/nasa/jpf/jvm/bytecode/IfInstruction.java
trunk/src/gov/nasa/jpf/jvm/bytecode/Instruction.java
trunk/src/gov/nasa/jpf/jvm/bytecode/InvokeInstruction.java
trunk/src/gov/nasa/jpf/jvm/bytecode/NEW.java
trunk/src/gov/nasa/jpf/jvm/bytecode/NOP.java
trunk/src/gov/nasa/jpf/jvm/bytecode/VirtualInvocation.java
trunk/src/gov/nasa/jpf/util/GenericInstructionFactory.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-07-19 17:17:17
|
Revision: 447
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=447&view=rev
Author: pcmehlitz
Date: 2007-07-19 10:17:13 -0700 (Thu, 19 Jul 2007)
Log Message:
-----------
Modified Paths:
--------------
trunk/.classpath
trunk/examples/Racer.java
trunk/src/gov/nasa/jpf/jvm/MethodInfo.java
trunk/src/gov/nasa/jpf/jvm/bytecode/ALOAD.java
trunk/src/gov/nasa/jpf/jvm/bytecode/ANEWARRAY.java
trunk/src/gov/nasa/jpf/jvm/bytecode/ASTORE.java
trunk/src/gov/nasa/jpf/jvm/bytecode/BIPUSH.java
trunk/src/gov/nasa/jpf/jvm/bytecode/CHECKCAST.java
trunk/src/gov/nasa/jpf/jvm/bytecode/DLOAD.java
trunk/src/gov/nasa/jpf/jvm/bytecode/DSTORE.java
trunk/src/gov/nasa/jpf/jvm/bytecode/FLOAD.java
trunk/src/gov/nasa/jpf/jvm/bytecode/FSTORE.java
trunk/src/gov/nasa/jpf/jvm/bytecode/GETFIELD.java
trunk/src/gov/nasa/jpf/jvm/bytecode/GETSTATIC.java
trunk/src/gov/nasa/jpf/jvm/bytecode/GOTO.java
trunk/src/gov/nasa/jpf/jvm/bytecode/GOTO_W.java
trunk/src/gov/nasa/jpf/jvm/bytecode/IINC.java
trunk/src/gov/nasa/jpf/jvm/bytecode/ILOAD.java
trunk/src/gov/nasa/jpf/jvm/bytecode/INSTANCEOF.java
trunk/src/gov/nasa/jpf/jvm/bytecode/INVOKECG.java
trunk/src/gov/nasa/jpf/jvm/bytecode/INVOKEINTERFACE.java
trunk/src/gov/nasa/jpf/jvm/bytecode/ISTORE.java
trunk/src/gov/nasa/jpf/jvm/bytecode/IfInstruction.java
trunk/src/gov/nasa/jpf/jvm/bytecode/Instruction.java
trunk/src/gov/nasa/jpf/jvm/bytecode/InvokeInstruction.java
trunk/src/gov/nasa/jpf/jvm/bytecode/JSR.java
trunk/src/gov/nasa/jpf/jvm/bytecode/JSR_W.java
trunk/src/gov/nasa/jpf/jvm/bytecode/LDC.java
trunk/src/gov/nasa/jpf/jvm/bytecode/LDC2_W.java
trunk/src/gov/nasa/jpf/jvm/bytecode/LDC_W.java
trunk/src/gov/nasa/jpf/jvm/bytecode/LLOAD.java
trunk/src/gov/nasa/jpf/jvm/bytecode/LOOKUPSWITCH.java
trunk/src/gov/nasa/jpf/jvm/bytecode/LSTORE.java
trunk/src/gov/nasa/jpf/jvm/bytecode/MULTIANEWARRAY.java
trunk/src/gov/nasa/jpf/jvm/bytecode/NEW.java
trunk/src/gov/nasa/jpf/jvm/bytecode/NEWARRAY.java
trunk/src/gov/nasa/jpf/jvm/bytecode/PUTFIELD.java
trunk/src/gov/nasa/jpf/jvm/bytecode/PUTSTATIC.java
trunk/src/gov/nasa/jpf/jvm/bytecode/RET.java
trunk/src/gov/nasa/jpf/jvm/bytecode/SIPUSH.java
trunk/src/gov/nasa/jpf/jvm/bytecode/TABLESWITCH.java
trunk/src/gov/nasa/jpf/util/Invocation.java
Added Paths:
-----------
trunk/examples/launch/
trunk/examples/launch/basic-racer-test.launch
trunk/examples/launch/basic-racer.launch
trunk/examples/launch/basic-random-test.launch
trunk/examples/launch/basic-random.launch
trunk/examples/launch/conc-0-RA-test.launch
trunk/examples/launch/conc-1-RA.launch
trunk/examples/launch/conc-2-RA_da.launch
trunk/examples/launch/conc-3-lockorder.launch
trunk/examples/launch/conc-4-ms.launch
trunk/examples/launch/conc-5-nml.launch
trunk/examples/launch/conc-6-race.launch
trunk/examples/launch/conc-7-race-eraser.launch
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-07-19 18:00:18
|
Revision: 448
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=448&view=rev
Author: pcmehlitz
Date: 2007-07-19 11:00:17 -0700 (Thu, 19 Jul 2007)
Log Message:
-----------
* first beginnings of the "symbolic threadsafety" execution mode
* added a CodeBuilder to solve the offset/position initialization problem
when creating synthetic methods
Added Paths:
-----------
trunk/extensions/symts/
trunk/extensions/symts/src/
trunk/extensions/symts/src/gov/
trunk/extensions/symts/src/gov/nasa/
trunk/extensions/symts/src/gov/nasa/jpf/
trunk/extensions/symts/src/gov/nasa/jpf/ts/
trunk/extensions/symts/src/gov/nasa/jpf/ts/GETFIELD.java
trunk/extensions/symts/src/gov/nasa/jpf/ts/IFEQ.java
trunk/extensions/symts/src/gov/nasa/jpf/ts/IFGE.java
trunk/extensions/symts/src/gov/nasa/jpf/ts/IFGT.java
trunk/extensions/symts/src/gov/nasa/jpf/ts/IFLE.java
trunk/extensions/symts/src/gov/nasa/jpf/ts/IFLT.java
trunk/extensions/symts/src/gov/nasa/jpf/ts/IFNE.java
trunk/extensions/symts/src/gov/nasa/jpf/ts/IFNONNULL.java
trunk/extensions/symts/src/gov/nasa/jpf/ts/IFNULL.java
trunk/extensions/symts/src/gov/nasa/jpf/ts/INVOKESPECIAL.java
trunk/extensions/symts/src/gov/nasa/jpf/ts/INVOKEVIRTUAL.java
trunk/extensions/symts/src/gov/nasa/jpf/ts/PUTFIELD.java
trunk/extensions/symts/src/gov/nasa/jpf/ts/TSInstructionFactory.java
trunk/extensions/symts/src/gov/nasa/jpf/ts/TSVM.java
trunk/extensions/symts/test/
trunk/extensions/symts/test/gov/
trunk/extensions/symts/test/gov/nasa/
trunk/extensions/symts/test/gov/nasa/jpf/
trunk/extensions/symts/test/gov/nasa/jpf/ts/
trunk/extensions/symts/test/gov/nasa/jpf/ts/TestUnprotectedRW.java
trunk/src/gov/nasa/jpf/jvm/CodeBuilder.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-07-23 05:58:56
|
Revision: 449
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=449&view=rev
Author: pcmehlitz
Date: 2007-07-22 22:58:52 -0700 (Sun, 22 Jul 2007)
Log Message:
-----------
* basic framework for symbolic threadsafe test generation
* had to turn some JVM methods into protected, probably more to follow
Modified Paths:
--------------
trunk/extensions/symts/src/gov/nasa/jpf/ts/GETFIELD.java
trunk/extensions/symts/src/gov/nasa/jpf/ts/PUTFIELD.java
trunk/extensions/symts/src/gov/nasa/jpf/ts/TSVM.java
trunk/src/gov/nasa/jpf/jvm/JVM.java
trunk/src/gov/nasa/jpf/util/Invocation.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pc...@us...> - 2007-07-25 02:36:57
|
Revision: 456
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=456&view=rev
Author: pcorina
Date: 2007-07-24 19:36:56 -0700 (Tue, 24 Jul 2007)
Log Message:
-----------
added choco decision procedure:
http://choco.sourceforge.net/
Modified Paths:
--------------
trunk/.classpath
Added Paths:
-----------
trunk/choco-1_2_04.jar
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-07-26 19:35:41
|
Revision: 458
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=458&view=rev
Author: pcmehlitz
Date: 2007-07-26 12:00:46 -0700 (Thu, 26 Jul 2007)
Log Message:
-----------
* some core changes to make VM and bytecode subclassing easier
* got the TSVM/TestCandidate/TestType/Listener structure for the symbolic threadsafety exec
in place. NOT FUNCTIONAL YET - now I have to put the branch CGs back in place, and
settle on an exit strategy for test case detection
Modified Paths:
--------------
trunk/examples/ase2006/Optimizer.java
trunk/examples/issta2006/TestListener.java
trunk/examples/issta2006/TestSearchMonitor.java
trunk/extensions/symts/src/gov/nasa/jpf/ts/TSInstructionFactory.java
trunk/extensions/symts/src/gov/nasa/jpf/ts/TSVM.java
trunk/src/gov/nasa/jpf/jvm/ThreadInfo.java
trunk/src/gov/nasa/jpf/jvm/bytecode/InvokeInstruction.java
trunk/src/gov/nasa/jpf/util/GenericInstructionFactory.java
Removed Paths:
-------------
trunk/extensions/symts/src/gov/nasa/jpf/ts/GETFIELD.java
trunk/extensions/symts/src/gov/nasa/jpf/ts/INVOKESPECIAL.java
trunk/extensions/symts/src/gov/nasa/jpf/ts/INVOKEVIRTUAL.java
trunk/extensions/symts/src/gov/nasa/jpf/ts/PUTFIELD.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-07-30 23:57:11
|
Revision: 460
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=460&view=rev
Author: pcmehlitz
Date: 2007-07-30 16:57:02 -0700 (Mon, 30 Jul 2007)
Log Message:
-----------
* added the missing IfInstructions for the TS extension, delegating the insn execution
(to the TSVM. in absence of a better place). Caused some suboptimal refactoring of
base class method attributes, but that still looks better than to retrict the type
of listener that can be used in conjunction with the derived bytecodes.
* the Instruction.getNext(ThreadInfo) was outdated, we don't purge stackframes anymore
on System.exit
* added a very incomplete TestJavaLangSystem reg test
Modified Paths:
--------------
trunk/extensions/symts/src/gov/nasa/jpf/ts/IFEQ.java
trunk/extensions/symts/src/gov/nasa/jpf/ts/IFGE.java
trunk/extensions/symts/src/gov/nasa/jpf/ts/IFGT.java
trunk/extensions/symts/src/gov/nasa/jpf/ts/IFLE.java
trunk/extensions/symts/src/gov/nasa/jpf/ts/IFLT.java
trunk/extensions/symts/src/gov/nasa/jpf/ts/IFNE.java
trunk/extensions/symts/src/gov/nasa/jpf/ts/IFNONNULL.java
trunk/extensions/symts/src/gov/nasa/jpf/ts/IFNULL.java
trunk/extensions/symts/src/gov/nasa/jpf/ts/TSInstructionFactory.java
trunk/extensions/symts/src/gov/nasa/jpf/ts/TSVM.java
trunk/extensions/symts/test/gov/nasa/jpf/ts/TestUnprotectedRW.java
trunk/src/gov/nasa/jpf/jvm/bytecode/IFEQ.java
trunk/src/gov/nasa/jpf/jvm/bytecode/IFGE.java
trunk/src/gov/nasa/jpf/jvm/bytecode/IFGT.java
trunk/src/gov/nasa/jpf/jvm/bytecode/IFLE.java
trunk/src/gov/nasa/jpf/jvm/bytecode/IFLT.java
trunk/src/gov/nasa/jpf/jvm/bytecode/IFNE.java
trunk/src/gov/nasa/jpf/jvm/bytecode/IFNONNULL.java
trunk/src/gov/nasa/jpf/jvm/bytecode/IFNULL.java
trunk/src/gov/nasa/jpf/jvm/bytecode/IF_ACMPEQ.java
trunk/src/gov/nasa/jpf/jvm/bytecode/IF_ACMPNE.java
trunk/src/gov/nasa/jpf/jvm/bytecode/IF_ICMPEQ.java
trunk/src/gov/nasa/jpf/jvm/bytecode/IF_ICMPGE.java
trunk/src/gov/nasa/jpf/jvm/bytecode/IF_ICMPGT.java
trunk/src/gov/nasa/jpf/jvm/bytecode/IF_ICMPLE.java
trunk/src/gov/nasa/jpf/jvm/bytecode/IF_ICMPLT.java
trunk/src/gov/nasa/jpf/jvm/bytecode/IF_ICMPNE.java
trunk/src/gov/nasa/jpf/jvm/bytecode/IfInstruction.java
trunk/src/gov/nasa/jpf/jvm/bytecode/InstanceFieldInstruction.java
trunk/src/gov/nasa/jpf/jvm/bytecode/Instruction.java
Added Paths:
-----------
trunk/extensions/symts/src/gov/nasa/jpf/ts/IF_ACMPEQ.java
trunk/extensions/symts/src/gov/nasa/jpf/ts/IF_ACMPNE.java
trunk/extensions/symts/src/gov/nasa/jpf/ts/IF_ICMPEQ.java
trunk/extensions/symts/src/gov/nasa/jpf/ts/IF_ICMPGE.java
trunk/extensions/symts/src/gov/nasa/jpf/ts/IF_ICMPGT.java
trunk/extensions/symts/src/gov/nasa/jpf/ts/IF_ICMPLE.java
trunk/extensions/symts/src/gov/nasa/jpf/ts/IF_ICMPLT.java
trunk/extensions/symts/src/gov/nasa/jpf/ts/IF_ICMPNE.java
trunk/test/gov/nasa/jpf/jvm/TestJavaLangSystem.java
trunk/test/gov/nasa/jpf/jvm/TestJavaLangSystemJPF.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-07-31 00:15:58
|
Revision: 461
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=461&view=rev
Author: pcmehlitz
Date: 2007-07-30 17:15:49 -0700 (Mon, 30 Jul 2007)
Log Message:
-----------
* always good to look twice - since the 'executeBothBranches' is so generic, why not
put it as a protected method in IfInstruction itself, so that we can delegate in
the overloaded execute() methods without a need for a caset, and within the same
package, i.e. without exposing critical instruction state like 'conditionValue'
Modified Paths:
--------------
trunk/extensions/symts/src/gov/nasa/jpf/ts/IFEQ.java
trunk/extensions/symts/src/gov/nasa/jpf/ts/IFGE.java
trunk/extensions/symts/src/gov/nasa/jpf/ts/IFGT.java
trunk/extensions/symts/src/gov/nasa/jpf/ts/IFLE.java
trunk/extensions/symts/src/gov/nasa/jpf/ts/IFLT.java
trunk/extensions/symts/src/gov/nasa/jpf/ts/IFNE.java
trunk/extensions/symts/src/gov/nasa/jpf/ts/IFNONNULL.java
trunk/extensions/symts/src/gov/nasa/jpf/ts/IFNULL.java
trunk/extensions/symts/src/gov/nasa/jpf/ts/IF_ACMPEQ.java
trunk/extensions/symts/src/gov/nasa/jpf/ts/IF_ACMPNE.java
trunk/extensions/symts/src/gov/nasa/jpf/ts/IF_ICMPEQ.java
trunk/extensions/symts/src/gov/nasa/jpf/ts/IF_ICMPGE.java
trunk/extensions/symts/src/gov/nasa/jpf/ts/IF_ICMPGT.java
trunk/extensions/symts/src/gov/nasa/jpf/ts/IF_ICMPLE.java
trunk/extensions/symts/src/gov/nasa/jpf/ts/IF_ICMPLT.java
trunk/extensions/symts/src/gov/nasa/jpf/ts/IF_ICMPNE.java
trunk/extensions/symts/src/gov/nasa/jpf/ts/TSInstructionFactory.java
trunk/extensions/symts/src/gov/nasa/jpf/ts/TSVM.java
trunk/src/gov/nasa/jpf/jvm/bytecode/IfInstruction.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-08-01 23:35:23
|
Revision: 465
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=465&view=rev
Author: pcmehlitz
Date: 2007-08-01 16:35:22 -0700 (Wed, 01 Aug 2007)
Log Message:
-----------
* added a generic Trace / TraceElement pair to ease creation of property/application
specific traces from listeners. This is mainly factorizes the backtracking, including
state matching (i.e. reverting matched transitions)
* used this to do the TSVM trace over field access & lock ops (classical example of
property specific trace). Not completely integrated yet.
* added simple synchronization filter, but still needs to be extended towards
synchronized methods, which might require some refactoring
Modified Paths:
--------------
trunk/extensions/symts/src/gov/nasa/jpf/ts/TSVM.java
Added Paths:
-----------
trunk/src/gov/nasa/jpf/util/Trace.java
trunk/src/gov/nasa/jpf/util/TraceElement.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