Menu
▾
▴
javapathfinder-devel
|
From: <pcm...@us...> - 2007-04-10 22:40:17
|
Revision: 308
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=308&view=rev
Author: pcmehlitz
Date: 2007-04-10 15:40:15 -0700 (Tue, 10 Apr 2007)
Log Message:
-----------
* rewoked the CoverageAnalyzer so that partially covered method bodies are
printed as fileLocation ranges, assuming that it is better to use Eclipse
for browsing than to print source snippets w/o comments
* Instruction.getSourceLocation() now just uses .getFileLocation(). Just a matter
of cleanup
Modified Paths:
--------------
trunk/.classpath
trunk/src/gov/nasa/jpf/jvm/bytecode/Instruction.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-04-12 21:27:09
|
Revision: 309
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=309&view=rev
Author: pcmehlitz
Date: 2007-04-12 14:27:00 -0700 (Thu, 12 Apr 2007)
Log Message:
-----------
* implemented explicit event sends via State.sendEvent(String,Object...) for both
StateMachine/NativeSateMachine and SimStateMachine
* implemented State.getEventId(), State.getEventArguments() to query event+args
of the event that got us into the current state (e.g. to be queried from
an entryAction, and used to send the next event)
these two should actually take care of (most of) the KC interfacing. Since KC praises
Moore state machines as the best thing since sliced bread, we should be able to map
this into our hierarchical scheme (there is always just one actve state), which left
us with explicit event sends
* StateMachine wasn't prepared to enter end states, i.e. still was looking for
a next event even if the entryAction sets the state to end state (why somebody would do
such a thing escapes me, but we want to be able to drive the whole machine from
within actions)
* added a little SendEvents1 test
* added sone newXX() methods for box types in MJIEnv
* ESParser didn't parse string literals correctly (StreamTokenizer returns it
as a '"' char, but with the sval set to the literal w/o quotes)
Modified Paths:
--------------
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_StateMachine.java
trunk/extensions/statechart/env/jvm/gov/nasa/jpf/jvm/NativeStateMachine.java
trunk/extensions/statechart/src/gov/nasa/jpf/tools/sc/SimStateMachine.java
trunk/src/gov/nasa/jpf/jvm/MJIEnv.java
trunk/src/gov/nasa/jpf/tools/CoverageAnalyzer.java
trunk/src/gov/nasa/jpf/util/script/ESParser.java
Added Paths:
-----------
trunk/extensions/statechart/examples/SendEvents1.es
trunk/extensions/statechart/examples/SendEvents1.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-04-13 21:29:44
|
Revision: 310
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=310&view=rev
Author: pcmehlitz
Date: 2007-04-13 14:29:42 -0700 (Fri, 13 Apr 2007)
Log Message:
-----------
* added a bunch of reflection APIs to support running Junit through JPF
* added 'modifiers' to both ClassInfo and MethodInfo - but they are currently just
used for the reflection API, whereas they should replace the various 'isStatic', 'isPublic'
or whatever boolean fields
* fixed a bug in Class.getDeclaredMethod() - internally, we keep MethodInfos, i.e. don't
differentiate between methods and ctors. Externally (via the reflection API), we have to
do that
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_Constructor.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_reflect_Method.java
trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
trunk/src/gov/nasa/jpf/jvm/JVM.java
trunk/src/gov/nasa/jpf/jvm/MethodInfo.java
trunk/src/gov/nasa/jpf/jvm/Types.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-04-13 21:57:44
|
Revision: 311
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=311&view=rev
Author: pcmehlitz
Date: 2007-04-13 14:57:39 -0700 (Fri, 13 Apr 2007)
Log Message:
-----------
* NumberFormat.getInstance() was missing (defaults to NUMBER type)
* native Class.getMethod() failed on empty args list ??
Modified Paths:
--------------
trunk/env/jpf/java/text/NumberFormat.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Class.java
trunk/src/gov/nasa/jpf/jvm/bytecode/INVOKESTATIC.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-04-15 02:19:38
|
Revision: 313
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=313&view=rev
Author: pcmehlitz
Date: 2007-04-14 19:19:37 -0700 (Sat, 14 Apr 2007)
Log Message:
-----------
* a hard days fight to make junit runnable under JPF, let's see..
* a bunch of missing reflection stuff
* didn't really handle Throwable.cause - it's sort of in now, but still
not fully compliant
* need to show native methods and Method.invoke as StackTraceElements, but both
are not on the stack (i.e. need to create them)
* InvocationTargetException is a pretty bad thing - we didn't handle it correctly (handle up to
the invoke() as the original exception, then wrap it into an InvocationTargetException), only
that ITXes store their cause differently (and override getCause). Nasty
* our StackTraceElement model class needs a toString()
* changed vm.halt_on_throw from a boolean into a string list with exception class name patterns
* File.getName() should only return base name
Modified Paths:
--------------
trunk/default.properties
trunk/env/jpf/java/io/File.java
trunk/env/jpf/java/lang/StackTraceElement.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Throwable.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_reflect_Method.java
trunk/src/gov/nasa/jpf/jvm/JVM.java
trunk/src/gov/nasa/jpf/jvm/MethodInfo.java
trunk/src/gov/nasa/jpf/jvm/ThreadInfo.java
trunk/src/gov/nasa/jpf/search/Search.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-04-16 07:37:25
|
Revision: 314
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=314&view=rev
Author: pcmehlitz
Date: 2007-04-16 00:37:24 -0700 (Mon, 16 Apr 2007)
Log Message:
-----------
* reworked trace replay - the SystemState internal replay was too redundant with
the ChoiceSelector, and the double use of "vm.use_trace" (both create and replay)
was too confusing.
* removed all this stuff from SystemState
* storage is now done with the TraceStorer, and it can handle a number of store
conditions outside property_violations. This also solves the problem of storing
init traces (if no error was found). Use "trace.file=.." to specify trace file
names (there are also a bunch of other options like "trace.multiple"). Default
trace file name is "trace"
* replay is done via the ChoiceSelector, which now has the "choice.use_trace"
property
* added a simple SingSetMatcher, to get rid once and for all with the
"prefix vs. regexpr" lookup in class lists, field lists, method lists etc.
This one also handled wildcards in a more Java identifier friendly way
(wildcard is '*', the '.' is an ordinary char and can appear in the pattern)
Still need to convert potential users
Modified Paths:
--------------
trunk/examples/ase2006/TestPartialTrace.java
trunk/src/gov/nasa/jpf/JPF.java
trunk/src/gov/nasa/jpf/jvm/ChoicePoint.java
trunk/src/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_jvm_Verify.java
trunk/src/gov/nasa/jpf/jvm/JVM.java
trunk/src/gov/nasa/jpf/jvm/SystemState.java
trunk/src/gov/nasa/jpf/jvm/Verify.java
trunk/src/gov/nasa/jpf/search/Search.java
trunk/src/gov/nasa/jpf/tools/ChoiceSelector.java
trunk/test/gov/nasa/jpf/mc/TestPartialTrace.java
trunk/test/gov/nasa/jpf/mc/TestPartialTraceJPF.java
Added Paths:
-----------
trunk/src/gov/nasa/jpf/tools/TraceStorer.java
trunk/src/gov/nasa/jpf/util/StringSetMatcher.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-04-17 20:09:45
|
Revision: 316
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=316&view=rev
Author: pcmehlitz
Date: 2007-04-17 13:09:43 -0700 (Tue, 17 Apr 2007)
Log Message:
-----------
* fixed bug with the java.text.Format initialization, causing only the last
created Format instance to be used. Forgot to call the super (Format) ctor
explicitly from the native peer, hence the 'id' handle never got updated.
Refactored native method into 'init0' calls, and added comments to all
relevant classes so that I don't forget it again
Modified Paths:
--------------
trunk/env/jpf/java/text/DecimalFormat.java
trunk/env/jpf/java/text/Format.java
trunk/env/jpf/java/text/SimpleDateFormat.java
trunk/env/jpf/java/util/concurrent/atomic/AtomicReferenceFieldUpdater.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_text_DecimalFormat.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_text_SimpleDateFormat.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_util_concurrent_atomic_AtomicReferenceFieldUpdater.java
trunk/src/gov/nasa/jpf/tools/CoverageAnalyzer.java
trunk/test/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_jvm_TestNativePeer.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-04-21 05:17:32
|
Revision: 322
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=322&view=rev
Author: pcmehlitz
Date: 2007-04-20 22:17:31 -0700 (Fri, 20 Apr 2007)
Log Message:
-----------
* introduced java.lang.System model class, to better support system properties, which
can be initialized via JPF properties or just copied from the host VM. Downside is a
slightly increased startup time
* created first versions of InputStreamReader / OutputStreamWriter for the
byte / char conversion that makes Java IO so international and slow. It's
terribly inefficient in JPF since we can't do much buffering, so it's a per-byte/char
native call, but at least it should be sun.* free now.
* created gov.nasa.jpf.ConsoleOutputStream for System.out/err, which bypasses PrintStream
for better efficiency (vast majority of IO is still System.out.println())
* finally added basic support for String.format(..)
Modified Paths:
--------------
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_String.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_System.java
trunk/src/gov/nasa/jpf/jvm/JVM.java
trunk/src/gov/nasa/jpf/jvm/MJIEnv.java
Added Paths:
-----------
trunk/env/jpf/gov/
trunk/env/jpf/gov/nasa/
trunk/env/jpf/gov/nasa/jpf/
trunk/env/jpf/gov/nasa/jpf/ConsoleOutputStream.java
trunk/env/jpf/java/io/InputStreamReader.java
trunk/env/jpf/java/io/OutputStreamWriter.java
trunk/env/jpf/java/lang/System.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_ConsoleOutputStream.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_io_InputStreamReader.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_io_OutputStreamWriter.java
Removed Paths:
-------------
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_io_PrintStream.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-04-23 07:48:41
|
Revision: 325
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=325&view=rev
Author: pcmehlitz
Date: 2007-04-23 00:48:38 -0700 (Mon, 23 Apr 2007)
Log Message:
-----------
* fixed both InputStreamReader & OutputStreamWriter to use block decode/encode. It's
still slow, but not braindead single char/byte conversion anymore. Still needs a lock
though
* little extension in DirectCallStackFrame.reset() - now we can reuse the frame
in loops from native methods
* finally created an example/testcase for an interative + recursive roundtrip
in TestNativePeer.testRoundtripLoop().
(JPF calls native, native repeatedly calls JPF, calls native). I hope that
doesn't cause all hell to break loose
* some more native String methods + tests
Modified Paths:
--------------
trunk/env/jpf/java/io/InputStreamReader.java
trunk/env/jpf/java/io/OutputStreamWriter.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_io_InputStreamReader.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_io_OutputStreamWriter.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_String.java
trunk/src/gov/nasa/jpf/jvm/DirectCallStackFrame.java
trunk/src/gov/nasa/jpf/jvm/MJIEnv.java
trunk/src/gov/nasa/jpf/jvm/StackFrame.java
trunk/test/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_jvm_TestNativePeer.java
trunk/test/gov/nasa/jpf/jvm/TestJavaLangString.java
trunk/test/gov/nasa/jpf/jvm/TestJavaLangStringJPF.java
trunk/test/gov/nasa/jpf/jvm/TestNativePeer.java
trunk/test/gov/nasa/jpf/jvm/TestNativePeerJPF.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-04-24 05:40:10
|
Revision: 326
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=326&view=rev
Author: pcmehlitz
Date: 2007-04-23 22:40:07 -0700 (Mon, 23 Apr 2007)
Log Message:
-----------
* FileInputStream & FileOutputStream support - finally!
file data is stored in the real file system, which makes the mechanism
suitable for large files. The JPF side so far mainly stores the
file position and the status. Operations are implemented in a
slightly bent FileDescriptor.
NOTE: write still lacks some notion of file data hashing, so it *is* still
possible to have a false state match (but it's quite unlikely the
difference would be only in the file data)
* added a roundtrip test case for file IO and Writers/Readers
* slightly improved OutputStreamWriter for String output (no more
per operation alloc)
Modified Paths:
--------------
trunk/env/jpf/java/io/FileDescriptor.java
trunk/env/jpf/java/io/FileInputStream.java
trunk/env/jpf/java/io/OutputStreamWriter.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_io_FileDescriptor.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_io_OutputStreamWriter.java
Added Paths:
-----------
trunk/env/jpf/java/io/FileOutputStream.java
trunk/test/gov/nasa/jpf/jvm/TestFileIO.java
trunk/test/gov/nasa/jpf/jvm/TestFileIOJPF.java
Removed Paths:
-------------
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_io_FileInputStream.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-04-27 07:12:25
|
Revision: 327
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=327&view=rev
Author: pcmehlitz
Date: 2007-04-27 00:12:23 -0700 (Fri, 27 Apr 2007)
Log Message:
-----------
first stab at serialization - ObjectInput/Outputstream works, even between a JVM and JPF.
I wouldn't consider it very stable yet, since our ObjectStreamClass compatibility is
awfully fragile (esp. with respect to sun.misc.Unsafe and java.util.concurrency, which
are both used). At some point we should model ObjectStreamClass
* the SerializationConstructor is a hack around a hack - to be compatible, we need a
synthetic ctor that initializes only upwards from the first non-serializable superclass
and leaves everything below for explicit init via reflection. It's a bit lazy to do this
on the model side (the real Constructor is a final class) though
* lots of reflection related fixes (e.g. the static Field.getX/setX with null params)
* fix in the canonical class name (arrays use the L-dot notation)
* minimalistic support for Date (still requires a lot more to be performant)
* MessageDigest forwarding (finalize doesn't work yet?)
* AccessController didn't properly wrap exceptions
lots more
Modified Paths:
--------------
trunk/env/jpf/java/lang/Class.java
trunk/env/jpf/java/lang/reflect/Constructor.java
trunk/env/jpf/java/lang/reflect/Field.java
trunk/env/jpf/java/lang/reflect/Method.java
trunk/env/jpf/java/security/AccessController.java
trunk/env/jpf/sun/misc/Unsafe.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_io_ObjectStreamClass.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Class.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_System.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_reflect_Constructor.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_reflect_Field.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_reflect_Method.java
trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
trunk/src/gov/nasa/jpf/jvm/DoubleFieldInfo.java
trunk/src/gov/nasa/jpf/jvm/FieldInfo.java
trunk/src/gov/nasa/jpf/jvm/FloatFieldInfo.java
trunk/src/gov/nasa/jpf/jvm/IntegerFieldInfo.java
trunk/src/gov/nasa/jpf/jvm/LongFieldInfo.java
trunk/src/gov/nasa/jpf/jvm/MJIEnv.java
trunk/src/gov/nasa/jpf/jvm/ReferenceFieldInfo.java
trunk/src/gov/nasa/jpf/jvm/Types.java
trunk/src/gov/nasa/jpf/jvm/bytecode/IfInstruction.java
Added Paths:
-----------
trunk/env/jpf/gov/nasa/jpf/SerializationConstructor.java
trunk/env/jpf/java/security/MessageDigest.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_SerializationConstructor.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_io_ObjectInputStream.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_security_MessageDigest.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_text_DateFormatSymbols.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_sun_reflect_ReflectionFactory.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-04-27 22:45:00
|
Revision: 329
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=329&view=rev
Author: pcmehlitz
Date: 2007-04-27 15:44:58 -0700 (Fri, 27 Apr 2007)
Log Message:
-----------
* cleaned up the invoke instructions with respect to getting the callee
* shifted the MethodTracker to executeInstruction() notification
* put it to use with some Locale and TimeZone methods
but that still doesn't do it - we need to model Date to cut off the
sun.util.Calendar usage
Modified Paths:
--------------
trunk/src/gov/nasa/jpf/jvm/JVM.java
trunk/src/gov/nasa/jpf/jvm/ThreadInfo.java
trunk/src/gov/nasa/jpf/jvm/bytecode/INVOKESPECIAL.java
trunk/src/gov/nasa/jpf/jvm/bytecode/VirtualInvocation.java
trunk/src/gov/nasa/jpf/tools/MethodTracker.java
Added Paths:
-----------
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_util_Locale.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_util_TimeZone.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-04-30 18:17:34
|
Revision: 330
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=330&view=rev
Author: pcmehlitz
Date: 2007-04-30 11:17:32 -0700 (Mon, 30 Apr 2007)
Log Message:
-----------
* the Eclipse search missed a JPF_java_lang_Class reference within MJIEnv,
which I most superfluously reintroduced (getReferredClassInfo() *is* in
MJIEnv nowadays)
* FileDescriptor didn't throw FileNotFoundException
* FileDescriptor access methods should check for fd != -1 and throw an
IOException if the file is closed
Modified Paths:
--------------
trunk/env/jpf/java/io/FileDescriptor.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_io_FileDescriptor.java
trunk/src/gov/nasa/jpf/jvm/MJIEnv.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-05-01 05:28:02
|
Revision: 331
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=331&view=rev
Author: pcmehlitz
Date: 2007-04-30 22:27:56 -0700 (Mon, 30 Apr 2007)
Log Message:
-----------
* serialization support for doubles (using Double.doubleToLongBits)
* more TimeZone, Calendar and Date forwarding (not yet safe due to Date's dual nature), esp.
Calendar needs a lot more to avoid sun.* stuff. TimeZone is a hack since it's an abstract class,
which we de-abstractify by means of it's peer
* String.equals wasn't null-safe
* temp file name support
Modified Paths:
--------------
trunk/env/jpf/java/io/File.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_io_ObjectInputStream.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_String.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_util_TimeZone.java
trunk/src/gov/nasa/jpf/jvm/abstraction/filter/FilteringSerializer.java
Added Paths:
-----------
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_io_ObjectOutputStream.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_util_Calendar.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_util_Date.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-05-02 08:05:06
|
Revision: 332
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=332&view=rev
Author: pcmehlitz
Date: 2007-05-02 01:05:01 -0700 (Wed, 02 May 2007)
Log Message:
-----------
* very very early ClassLoader support. Actually, we only support part of
the getResource(), and no user defined ClassLoaders yet (no link from
Class to ClassLoader yet), but that's good enough for simple file
resource lookup
* for that purpose, added a ClassInfo.getResource(), which has to
traverse the ClassPath itself because BCEL doesn't handle jar resources
(finds them, but there is no telling it is in a jar)
* ConsoleOutputStream wasn't null resilient
* added an AtomicLong compareAndSet, which is the basis for Random
* actually, there is an interesting question of how to handle
Random - it looks like we only optionally want this to turn into
CGs, because some apps would otherwise blow up
Modified Paths:
--------------
trunk/env/jpf/gov/nasa/jpf/ConsoleOutputStream.java
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_util_Random.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_util_concurrent_atomic_AtomicLong.java
trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
trunk/src/gov/nasa/jpf/jvm/JVM.java
trunk/src/gov/nasa/jpf/jvm/MJIEnv.java
Added Paths:
-----------
trunk/env/jpf/java/lang/ClassLoader.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_ClassLoader.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-05-03 07:41:07
|
Revision: 333
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=333&view=rev
Author: pcmehlitz
Date: 2007-05-03 00:41:04 -0700 (Thu, 03 May 2007)
Log Message:
-----------
* InputStreamReader has to provide a ready()
* casting multi-dim array objects failed because of the / . type name confusion
* Random now uses the standard lib randomizing. Still need to do the optional
CG enumeration - THIS MIGHT BREAK SOME JPF EXAMPLE/TEST APPS!!
* StringBuffer wasn't null safe
* UNBELIEVABLE - apparently we never had growing DynamicXArrays, since there was
a freakish relict bug in the growth handling
Modified Paths:
--------------
trunk/env/jpf/java/io/InputStreamReader.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_StringBuffer.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_reflect_Array.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_util_Random.java
trunk/src/gov/nasa/jpf/jvm/Types.java
trunk/src/gov/nasa/jpf/jvm/bytecode/CHECKCAST.java
trunk/src/gov/nasa/jpf/util/DynamicIntArray.java
trunk/src/gov/nasa/jpf/util/DynamicObjectArray.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-05-05 00:39:58
|
Revision: 335
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=335&view=rev
Author: pcmehlitz
Date: 2007-05-04 16:57:23 -0700 (Fri, 04 May 2007)
Log Message:
-----------
* decode in InputStreamReader native peer has to be reset before using it in a new run
* DecimalFormatSymbols were missing some inits
* StackFrame.printStackframe() didn't work for synthetic methods (w/o classes)
CoverageAnalyzer has to be smarter about class dirs, so that it doesn't list classes twice (e.g. by
recursively descending into '.')
Modified Paths:
--------------
trunk/env/jpf/java/io/InputStreamReader.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_io_InputStreamReader.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_text_DecimalFormatSymbols.java
trunk/src/gov/nasa/jpf/jvm/StackFrame.java
trunk/src/gov/nasa/jpf/jvm/bytecode/InvokeInstruction.java
trunk/src/gov/nasa/jpf/tools/CallMonitor.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-05-15 23:45:21
|
Revision: 340
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=340&view=rev
Author: pcmehlitz
Date: 2007-05-15 16:45:19 -0700 (Tue, 15 May 2007)
Log Message:
-----------
* leftover statemachine extensions from the demo
* NumericInstructionFactory that checks for classes to instrument
* StringSetMatcher convenience method for filters that use both
include and exclude sets
!! there seems to be a memory leak across repeated JPF invocations that shows up with the numeric test cases
Modified Paths:
--------------
trunk/build.xml
trunk/extensions/numeric/src/gov/nasa/jpf/numeric/NumericInstructionFactory.java
trunk/extensions/numeric/test/gov/nasa/jpf/numeric/TestNumeric.java
trunk/extensions/numeric/test/gov/nasa/jpf/numeric/TestNumericJPF.java
trunk/extensions/statechart/env/jpf/gov/nasa/jpf/sc/StateMachine.java
trunk/src/gov/nasa/jpf/Config.java
trunk/src/gov/nasa/jpf/jvm/DefaultInstructionFactory.java
trunk/src/gov/nasa/jpf/jvm/InstructionFactory.java
trunk/src/gov/nasa/jpf/jvm/JVM.java
trunk/src/gov/nasa/jpf/jvm/StackFrame.java
trunk/src/gov/nasa/jpf/jvm/bytecode/INVOKESPECIAL.java
trunk/src/gov/nasa/jpf/report/ConsolePublisher.java
trunk/src/gov/nasa/jpf/tools/AssertionProperty.java
trunk/src/gov/nasa/jpf/tools/CoverageAnalyzer.java
trunk/src/gov/nasa/jpf/util/StringSetMatcher.java
trunk/test/gov/nasa/jpf/jvm/TestInsnInterceptionListener.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-05-16 06:05:31
|
Revision: 341
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=341&view=rev
Author: pcmehlitz
Date: 2007-05-15 23:05:30 -0700 (Tue, 15 May 2007)
Log Message:
-----------
* added an init(Config) call from the NativePeer ctor, to initialize
native peer classes. the method is optional, but should be implemented
if the native peer class (which is all static) has static fields that
might cause memory leaks during consecutive JPF runs (e.g. from junit
test cases)
* updated native peers accordingly, which fixed a rather serious leak
in JPF_java_lang_reflect_Method
* commented out the PeerDispatcher support, it seems superfluous since
reflection invocation got fast enough
Modified Paths:
--------------
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_io_FileDescriptor.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_reflect_Field.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_reflect_Method.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_text_Format.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_security_MessageDigest.java
trunk/src/gov/nasa/jpf/jvm/JVM.java
trunk/src/gov/nasa/jpf/jvm/NativePeer.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-05-17 06:01:50
|
Revision: 342
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=342&view=rev
Author: pcmehlitz
Date: 2007-05-16 23:01:48 -0700 (Wed, 16 May 2007)
Log Message:
-----------
* native String.hashCode(), which makes a surprisingly huge difference in programs
that has a lot of Strings. I assume it's the step recording that came with 'statistics',
but that's not w/o relevance either. Side effect is that the original hashCode() of course
would have given the numeric bytecodes trouble, since it deliberatly overflows
Modified Paths:
--------------
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_String.java
trunk/src/gov/nasa/jpf/jvm/Fields.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-05-21 23:58:36
|
Revision: 343
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=343&view=rev
Author: pcmehlitz
Date: 2007-05-21 16:58:35 -0700 (Mon, 21 May 2007)
Log Message:
-----------
* a kind of hack'ish workaround to avoid PrintStream initialization if all we need
is System.out / System.err (which are our very own ConsolePrintStreams). To preserve the
inheritance structure, ConsoleOutputStream is a PrintStream subclass, but unfortunately
the PrintStream(OutputStream) ctor checks for a 'null' argument, so we have to
intercept the ConsoleOutputStream ctor in the peer. That means the PrintStream part of
it isn't initialized! Doesn't bother us as long as intercept all operations, which is
what we have this thing for anyways. Still, not very safe
* added getters for the StateMachine activeStates / nextActives sets, so that actions
that need to explicitly send events can check what to send (the "executable UML" dialect story)
* also added the interface to provide target states for explicit event sends, but that isn't
implemented yet on the native side
Modified Paths:
--------------
trunk/env/jpf/gov/nasa/jpf/ConsoleOutputStream.java
trunk/env/jpf/java/lang/System.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_ConsoleOutputStream.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_System.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_StateMachine.java
trunk/extensions/statechart/env/jvm/gov/nasa/jpf/jvm/NativeStateMachine.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-05-22 21:58:57
|
Revision: 344
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=344&view=rev
Author: pcmehlitz
Date: 2007-05-22 14:58:56 -0700 (Tue, 22 May 2007)
Log Message:
-----------
repository trouble again - seems at least two of my previous commits didn't make it
despite not showing an error. It's once more file renaming, not sure if Subversion or
Subclipse is the culprit. This is part 1 of the commit
* added branch coverage to the CoverageManager. It's not very polished yet, but at least we can
see which condition values are not executed
----------------------------------- previous commit message
* more work on static (re-)initialization of peer classes
* added a MethodInfoRegistry utility class. Since Method and Constructor are not inheritance related,
the best we can do to avoid code duplication is to factor this out
* added a RunRegistry/RunListener mechanism to help with dependencies between not inheritance related
peer classes. The problem is that the Class peer creates Constructor/
Method objects, so we either have to add Method and Class to the list of pre-initialized classes (bad, since
it means we have to make the dependencies explicit in JVM code that is otherwise not concerned about this), or
we have to come up with a general mechanism to detect re-initialization.
The general problem is that - wherever we use static fields (like in peers) - we have to be aware of
consecutive JPF runs (e.g. within a JUnit context), so we have to avoid memory leaks
* LogHandler didn't handle argument formatting
Modified Paths:
--------------
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Class.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_reflect_Constructor.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_reflect_Method.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_text_DecimalFormat.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_text_SimpleDateFormat.java
trunk/src/gov/nasa/jpf/JPF.java
trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
trunk/src/gov/nasa/jpf/jvm/JVM.java
trunk/src/gov/nasa/jpf/jvm/MJIEnv.java
trunk/src/gov/nasa/jpf/tools/CoverageAnalyzer.java
trunk/src/gov/nasa/jpf/util/LogHandler.java
Added Paths:
-----------
trunk/src/gov/nasa/jpf/util/MethodInfoRegistry.java
trunk/src/gov/nasa/jpf/util/RunListener.java
trunk/src/gov/nasa/jpf/util/RunRegistry.java
Removed Paths:
-------------
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_text_Format.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-05-23 17:08:15
|
Revision: 346
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=346&view=rev
Author: pcmehlitz
Date: 2007-05-23 10:08:14 -0700 (Wed, 23 May 2007)
Log Message:
-----------
* extended the StateMachine implementations so that events can be sent to specific
states. If no target state is provided, the event is sent to all active states. Semantics
are that in every step, the machine first looks for pending (sent) events for all
active states and creates a single CG from them. If there is no event pending (neither
sent to a state or to all), then the factory is used to obtain the next CG (from the
guidance script).
In scriptless mode, explicitly sent events are ignored, since the machine explores
all triggers for all active states anyways
With this mechanism, "executable UML" notations like KC (that use a number of concurrent
state machines communicating via explicit event sends) can be modeled as orthogonal
regions within the same master state. However, this still follows the run-to-completion
schema, i.e. these states advance synchronously (no concurrent execution)
still needs to be tested beyond SendEvent1 example
Modified Paths:
--------------
trunk/extensions/statechart/env/jvm/gov/nasa/jpf/jvm/NativeStateMachine.java
trunk/extensions/statechart/src/gov/nasa/jpf/tools/sc/SimStateMachine.java
trunk/src/gov/nasa/jpf/jvm/MJIEnv.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-05-24 08:06:04
|
Revision: 347
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=347&view=rev
Author: pcmehlitz
Date: 2007-05-24 01:06:02 -0700 (Thu, 24 May 2007)
Log Message:
-----------
* added a State.getMachine() accessor, which should be used with care since models should
be absolutely free of execution policy. This was necessary to obtain the set of active
states in our Unimod example
* finally started to implement the "vm.enumerate_random" option. Just nextInt() so far
* added a docu page with simple model checking examples. This needs to be more elaborated
to show how JPF differs from normal execution mode
Modified Paths:
--------------
trunk/doc/Model_Checking_vs_Testing.html
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_util_Random.java
trunk/extensions/statechart/env/jpf/gov/nasa/jpf/sc/State.java
Added Paths:
-----------
trunk/doc/sw_model_checking.html
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-05-25 22:33:17
|
Revision: 348
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=348&view=rev
Author: pcmehlitz
Date: 2007-05-25 15:33:15 -0700 (Fri, 25 May 2007)
Log Message:
-----------
* polished the "software model checking by example" page a bit, adding some graphs
* updated SVN access method in "Obtaining and Installing.."
* implemented Random.getBoolean for enumerate_random
this included a bug (missed re-init) in the Verify peer
* documented and updated the FixedPhone Java sources
* added a png for the FixedPhone
* updated default.properties with some new props
Modified Paths:
--------------
trunk/default.properties
trunk/doc/Obtaining_and_Installing_JPF.html
trunk/doc/sw_model_checking.html
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_util_Random.java
trunk/extensions/statechart/examples/FixedPhone.java
trunk/src/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_jvm_Verify.java
Added Paths:
-----------
trunk/doc/JPF_files/graffle/sw-model-checking.graffle
trunk/doc/JPF_files/state-graph-checking.png
trunk/doc/JPF_files/state-graph-testing.png
trunk/extensions/statechart/examples/FixedPhone.png
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