Menu
▾
▴
javapathfinder-devel
|
From: <pcm...@us...> - 2007-11-06 03:09:57
|
Revision: 648
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=648&view=rev
Author: pcmehlitz
Date: 2007-11-05 19:09:49 -0800 (Mon, 05 Nov 2007)
Log Message:
-----------
* AASTORE should check array element type compatibility for non-null element values
Thanks Tihomir Gvero and Milos Gligoric
* added TestArray test case for ArrayStoreExceptions (and finally converted it into
a RawTest class)
Modified Paths:
--------------
trunk/.classpath
trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
trunk/src/gov/nasa/jpf/jvm/bytecode/ArrayStoreInstruction.java
trunk/test/gov/nasa/jpf/jvm/TestArray.java
trunk/test/gov/nasa/jpf/jvm/TestArrayJPF.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-11-06 23:13:08
|
Revision: 649
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=649&view=rev
Author: pcmehlitz
Date: 2007-11-06 15:13:06 -0800 (Tue, 06 Nov 2007)
Log Message:
-----------
* 'permit' field was not initialized for main thread. still needs some refactoring though
* added a little test for Martijn Hendriks example, but it's not in the regression suite yet
since I still have to verify the deadlock
Modified Paths:
--------------
trunk/env/jpf/java/lang/Thread.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_sun_misc_Unsafe.java
trunk/src/gov/nasa/jpf/jvm/JVM.java
Added Paths:
-----------
trunk/test/gov/nasa/jpf/jvm/TestCountDownLatch.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-11-07 20:30:15
|
Revision: 650
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=650&view=rev
Author: pcmehlitz
Date: 2007-11-07 12:30:12 -0800 (Wed, 07 Nov 2007)
Log Message:
-----------
* added Runtime.availableProcessors(), together with a little test case. All the data acquisition
APIs in Runtime should be optionally turned into CGs (which is the case if "+cg.max_processors" is > 1)
* refactored the other API CG relevant settings to be under the "cg.*" section (enumerate_boolean, randomize_choices etc.)
Modified Paths:
--------------
trunk/default.properties
trunk/env/jpf/java/lang/Thread.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Runtime.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Thread.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_util_Random.java
trunk/test/gov/nasa/jpf/jvm/TestThread.java
trunk/test/gov/nasa/jpf/jvm/TestThreadJPF.java
trunk/test/gov/nasa/jpf/mc/TestRandomJPF.java
Added Paths:
-----------
trunk/test/gov/nasa/jpf/jvm/TestRuntime.java
trunk/test/gov/nasa/jpf/jvm/TestRuntimeJPF.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-11-15 22:52:59
|
Revision: 651
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=651&view=rev
Author: pcmehlitz
Date: 2007-11-15 14:52:57 -0800 (Thu, 15 Nov 2007)
Log Message:
-----------
* streamlined the ClassInfo.isInstanceOf implementation - the "instanceOf(String)" and "isInstanceOf(ClassInfo)" actually
behaved differently (the latter one not checking for interface types). renamed it so that it consistently uses
isInstanceOf, the string version being the real implementation (so that we can test w/o forcing to load classfiles)
* changes CHECKCAST accordingly (the old normalized type name blues)
* added a few more tests to TestJavaLangClass and changed TestCast accordingly
now it passes the UI examples again (which were producing ArrayStoreExceptions because of interface type arrays, using isInstaceOf(ci) for element type compatibility checks)
Modified Paths:
--------------
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Class.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Object.java
trunk/extensions/ui/env/jvm/gov/nasa/jpf/jvm/JPF_java_awt_EventDispatchThread.java
trunk/extensions/ui/env/jvm/gov/nasa/jpf/jvm/JPF_java_awt_Window.java
trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
trunk/src/gov/nasa/jpf/jvm/ElementInfo.java
trunk/src/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_jvm_Verify.java
trunk/src/gov/nasa/jpf/jvm/MJIEnv.java
trunk/src/gov/nasa/jpf/jvm/ThreadInfo.java
trunk/src/gov/nasa/jpf/jvm/Types.java
trunk/src/gov/nasa/jpf/jvm/abstraction/abstractor/FilterBasedAbstractorConfiguration.java
trunk/src/gov/nasa/jpf/jvm/bytecode/CHECKCAST.java
trunk/src/gov/nasa/jpf/jvm/choice/TypedObjectChoice.java
trunk/test/gov/nasa/jpf/jvm/TestCast.java
trunk/test/gov/nasa/jpf/jvm/TestCastJPF.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-11-20 06:14:20
|
Revision: 652
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=652&view=rev
Author: pcmehlitz
Date: 2007-11-19 22:14:18 -0800 (Mon, 19 Nov 2007)
Log Message:
-----------
* some more System.arraycopy element type checks (reference element types - thanks to Milos Gligoric and Tihomir Gvero,
ref/builtin, builtin/builtin, both single- and double word)
Modified Paths:
--------------
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_System.java
trunk/test/gov/nasa/jpf/jvm/TestArray.java
trunk/test/gov/nasa/jpf/jvm/TestArrayJPF.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-11-28 04:23:13
|
Revision: 666
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=666&view=rev
Author: pcmehlitz
Date: 2007-11-27 20:23:02 -0800 (Tue, 27 Nov 2007)
Log Message:
-----------
* Java SE 6 unveiled a forgotten check in the CHECKCAST insn - thanks to Franck van Breugel
Modified Paths:
--------------
trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
trunk/src/gov/nasa/jpf/jvm/bytecode/CHECKCAST.java
trunk/test/gov/nasa/jpf/jvm/TestCast.java
trunk/test/gov/nasa/jpf/jvm/TestCastJPF.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-11-29 19:32:56
|
Revision: 671
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=671&view=rev
Author: pcmehlitz
Date: 2007-11-29 11:32:54 -0800 (Thu, 29 Nov 2007)
Log Message:
-----------
* revamped contract grammar and interpreter - still a long way to go (array subscripts, functions, exception contracts,
open/closed intervals, sets, ...), but at least that's a better basis now. The big thing is that we have expressions
over operand values, including a generic "old(<expr>)" (so that we can store arbitrary exprs pre-exec)
Modified Paths:
--------------
trunk/src/gov/nasa/jpf/test/Contract.java
trunk/src/gov/nasa/jpf/test/ContractAnd.java
trunk/src/gov/nasa/jpf/test/ContractOr.java
trunk/src/gov/nasa/jpf/test/ContractSpec.g
trunk/src/gov/nasa/jpf/test/ContractSpecLexer.java
trunk/src/gov/nasa/jpf/test/ContractSpecParser.java
trunk/src/gov/nasa/jpf/test/EmptyContract.java
trunk/src/gov/nasa/jpf/test/Operand.java
trunk/src/gov/nasa/jpf/test/VarLookup.java
trunk/src/gov/nasa/jpf/tools/ChoiceSelector.java
trunk/src/gov/nasa/jpf/tools/ContractVerifier.java
trunk/test/gov/nasa/jpf/test/TestContracts.java
Added Paths:
-----------
trunk/src/gov/nasa/jpf/test/Expr.java
Removed Paths:
-------------
trunk/src/gov/nasa/jpf/test/SimpleContract.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-11-29 20:12:09
|
Revision: 672
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=672&view=rev
Author: pcmehlitz
Date: 2007-11-29 12:12:05 -0800 (Thu, 29 Nov 2007)
Log Message:
-----------
* @UntrackedField extension from Tihomir Gvero and Milos Gligoric.
This is a general solution for the problem of
accumulating values over all paths (i.e. vars that don't get restored upon backtrack), and e.g. comes in handy for
test applications (= JPF specific models) that do some kind of coverage analysis. Be aware of the 'Heisenberg' in
there, but it's much better than the crude MJI based counters we used for testing so far, or any ad-hoc application
solutions. If you want the details, there is a Untracked.html in the docs
Modified Paths:
--------------
trunk/default.properties
trunk/src/gov/nasa/jpf/jvm/Area.java
trunk/src/gov/nasa/jpf/jvm/CollapsingRestorer.java
trunk/src/gov/nasa/jpf/jvm/DynamicFields.java
trunk/src/gov/nasa/jpf/jvm/FieldInfo.java
trunk/src/gov/nasa/jpf/jvm/Fields.java
trunk/src/gov/nasa/jpf/jvm/StaticFields.java
Added Paths:
-----------
trunk/doc/Untracked.html
trunk/src/gov/nasa/jpf/jvm/untracked/
trunk/src/gov/nasa/jpf/jvm/untracked/UntrackedField.java
trunk/src/gov/nasa/jpf/jvm/untracked/UntrackedManager.java
trunk/test/gov/nasa/jpf/mc/TestUntrackedField.java
trunk/test/gov/nasa/jpf/mc/TestUntrackedFieldJPF.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-12-06 06:37:25
|
Revision: 689
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=689&view=rev
Author: pcmehlitz
Date: 2007-12-05 22:37:20 -0800 (Wed, 05 Dec 2007)
Log Message:
-----------
* support for user defined state class hierarchies, including masked state fields. Not sure
if that ever would make sense from a modeling standpoint (to the contrary - I am sure it doesn't),
but with some extra effort (explicitly walking the class hierarchy) we can also initialize the
masked fields. Seems worth it to prevent some very strange runtime behaviors that ultimately run into
uninitialized state objects with names of initialized ones. very confusing!
Modified Paths:
--------------
trunk/extensions/statechart/env/jpf/gov/nasa/jpf/sc/State.java
trunk/extensions/statechart/env/jvm/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_sc_State.java
trunk/extensions/statechart/src/gov/nasa/jpf/tools/sc/Coverage.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-12-11 19:37:16
|
Revision: 697
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=697&view=rev
Author: pcmehlitz
Date: 2007-12-11 11:37:07 -0800 (Tue, 11 Dec 2007)
Log Message:
-----------
* Tihomir's patch for long/double/short/byte/char annotation element types
* first stab at the SequenceAnalyzer, which is supposed to become an XMI exporter for UML sequence diagrams, produced from
running annotated Java programs. Still needs a long way to go though. It finally is (user) Trace<E> client. Actually, it even maintains two traces, but only one of them is a conceptual one (sequenceOps), the other one just abuses Trace to implement backtracking of the sequence context
Modified Paths:
--------------
trunk/env/jpf/java/lang/System.java
trunk/env/jpf/java/lang/Thread.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_System.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_sun_misc_Unsafe.java
trunk/src/gov/nasa/jpf/jvm/AnnotationInfo.java
trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
trunk/src/gov/nasa/jpf/jvm/MJIEnv.java
trunk/src/gov/nasa/jpf/jvm/MethodInfo.java
trunk/src/gov/nasa/jpf/jvm/bytecode/CHECKCAST.java
trunk/src/gov/nasa/jpf/util/Trace.java
Added Paths:
-----------
trunk/app/gov/nasa/jpf/NonNull.java
trunk/app/gov/nasa/jpf/Sequence.java
trunk/app/gov/nasa/jpf/SequenceEvent.java
trunk/app/gov/nasa/jpf/SequenceObject.java
trunk/src/gov/nasa/jpf/tools/SequenceAnalyzer.java
trunk/test/gov/nasa/jpf/mc/TestAnnotation.java
trunk/test/gov/nasa/jpf/mc/TestAnnotationJPF.java
trunk/test/gov/nasa/jpf/test/TestSequence.java
Removed Paths:
-------------
trunk/src/gov/nasa/jpf/test/Operator.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-12-12 19:14:57
|
Revision: 698
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=698&view=rev
Author: pcmehlitz
Date: 2007-12-12 11:14:55 -0800 (Wed, 12 Dec 2007)
Log Message:
-----------
* rather embarrassing bug in ClassInfo.getAllInterfaces(), which was not working recursively up the inheritance chain. The recursion at some point was in loadInterfacesRecursively, but vanished. Bug report thanks to Louise Dennis
Modified Paths:
--------------
trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
trunk/test/gov/nasa/jpf/jvm/TestCast.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-12-14 00:29:31
|
Revision: 703
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=703&view=rev
Author: pcmehlitz
Date: 2007-12-13 16:29:24 -0800 (Thu, 13 Dec 2007)
Log Message:
-----------
* next round for the SequenceAnalyzer. Added a SequenceProcessor abstraction to facilitate checks/reports on traces.
Added a default processor which writes out sequences in a format that's compatible to Alex Moffat's SEQUENCE
generator. Still needs a lot of cleanup and completion, and esp. a workaround for a BCEL bug that silently drops
annotation elements if there are default values
Modified Paths:
--------------
trunk/src/gov/nasa/jpf/tools/SequenceAnalyzer.java
trunk/src/gov/nasa/jpf/util/Trace.java
trunk/test/gov/nasa/jpf/test/TestSequence.java
Added Paths:
-----------
trunk/app/gov/nasa/jpf/SequenceMethod.java
trunk/src/gov/nasa/jpf/test/SequenceOp.java
trunk/src/gov/nasa/jpf/test/SequenceProcessor.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-12-14 05:17:11
|
Revision: 704
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=704&view=rev
Author: pcmehlitz
Date: 2007-12-13 21:17:08 -0800 (Thu, 13 Dec 2007)
Log Message:
-----------
* added PUTFIELD init of object references and symbolic result names
Modified Paths:
--------------
trunk/app/gov/nasa/jpf/SequenceMethod.java
trunk/app/gov/nasa/jpf/SequenceObject.java
trunk/src/gov/nasa/jpf/test/SequenceOp.java
trunk/src/gov/nasa/jpf/tools/SequenceAnalyzer.java
trunk/test/gov/nasa/jpf/test/TestSequence.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-12-15 04:49:14
|
Revision: 708
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=708&view=rev
Author: pcmehlitz
Date: 2007-12-14 20:49:11 -0800 (Fri, 14 Dec 2007)
Log Message:
-----------
* beginnings of @Requirement annotation extension for CoverageAnalyzer. It only stores the related MethodCoevarge
objects so far, statistics still need to be done
Modified Paths:
--------------
trunk/src/gov/nasa/jpf/tools/CoverageAnalyzer.java
trunk/src/gov/nasa/jpf/util/Misc.java
Added Paths:
-----------
trunk/app/gov/nasa/jpf/Requirement.java
trunk/test/gov/nasa/jpf/test/TestRequirementsCoverage.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-12-17 06:27:51
|
Revision: 710
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=710&view=rev
Author: pcmehlitz
Date: 2007-12-16 22:27:48 -0800 (Sun, 16 Dec 2007)
Log Message:
-----------
* changed requirements coverage report so that it shows the complete set of requirements (from the class set), and
hence reports the requirements/method coverage correctly (i.e. including the non-loaded requirements methods). The insn,
BB and branch coverage is only reported for the loaded ones, which might be a bit misleading.
That of course makes it even more important to NOT use ClassInfos for getting all defined requirements methods from the
class set
* minor bug in Instruction.isCompleted(ti) - has to include terminated threads (we mainly get this from the thread stack)
* first round against the ConstChecker, a little listener that monitors @Const attributes. The static method @Const is still a joke (inefficient), and we really need to use memory pools for this. The "return clone on mod" pattern for the pseudo-traces
(which are really just backtrackable/restorable stacks) is Ok, but error prone. There needs to be better infrastructure for
listener specific state extensions
Modified Paths:
--------------
trunk/src/gov/nasa/jpf/jvm/bytecode/Instruction.java
trunk/src/gov/nasa/jpf/tools/CoverageAnalyzer.java
trunk/src/gov/nasa/jpf/tools/SequenceAnalyzer.java
trunk/test/gov/nasa/jpf/test/TestRequirementsCoverage.java
Added Paths:
-----------
trunk/src/gov/nasa/jpf/tools/ConstChecker.java
trunk/test/gov/nasa/jpf/test/TestConst.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-12-17 06:43:40
|
Revision: 711
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=711&view=rev
Author: pcmehlitz
Date: 2007-12-16 22:43:39 -0800 (Sun, 16 Dec 2007)
Log Message:
-----------
* bug fix for casting builtin type arrays, thanks to Tihomir Gvero
Modified Paths:
--------------
trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
trunk/test/gov/nasa/jpf/jvm/TestCast.java
trunk/test/gov/nasa/jpf/jvm/TestCastJPF.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-12-18 03:06:31
|
Revision: 714
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=714&view=rev
Author: pcmehlitz
Date: 2007-12-17 19:05:53 -0800 (Mon, 17 Dec 2007)
Log Message:
-----------
* apparently, the non-ASCII +- char for center-interval tests screwed up either BCEL or ANTLR or both. Modified the
grammar, the test, and the contract class to replace it with "+-"
Modified Paths:
--------------
trunk/src/gov/nasa/jpf/test/Contract.java
trunk/src/gov/nasa/jpf/test/ContractSpec.g
trunk/src/gov/nasa/jpf/test/ContractSpecLexer.java
trunk/src/gov/nasa/jpf/test/ContractSpecParser.java
trunk/test/gov/nasa/jpf/test/TestContracts.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-12-21 00:37:11
|
Revision: 719
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=719&view=rev
Author: pcmehlitz
Date: 2007-12-20 16:37:04 -0800 (Thu, 20 Dec 2007)
Log Message:
-----------
* changed @Requirement annotation to have a String array attribute, so that a method can be associated with several
requirements. Still needs some more polishing for the report (we probably should report the uncovered/not-loaded methods for each requirement). It's also worth it to extend the MethodTester to execute test exprs for certain requirements (not the whole class)
* added the Eclipse launch configs to the test dir
Modified Paths:
--------------
trunk/app/gov/nasa/jpf/Requirement.java
trunk/doc/JPF_files/JPF-mod.css
trunk/src/gov/nasa/jpf/tools/CoverageAnalyzer.java
trunk/test/gov/nasa/jpf/test/TestMethodTest.java
trunk/test/gov/nasa/jpf/test/TestRequirementsCoverage.java
Added Paths:
-----------
trunk/test/gov/nasa/jpf/test/TestConst.launch
trunk/test/gov/nasa/jpf/test/TestContracts.launch
trunk/test/gov/nasa/jpf/test/TestMethods-standalone.launch
trunk/test/gov/nasa/jpf/test/TestMethods.launch
trunk/test/gov/nasa/jpf/test/TestRequirements.launch
trunk/test/gov/nasa/jpf/test/TestSequence.launch
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-12-27 07:15:44
|
Revision: 720
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=720&view=rev
Author: pcmehlitz
Date: 2007-12-26 23:15:39 -0800 (Wed, 26 Dec 2007)
Log Message:
-----------
* bag of bug fixes from Tihomir & Darko
- ConsoleOutputStream printf/format (w/o test, since only side effect)
- Enum<T>.valueOf() fix (requires - package private - Class.enumConstantDirectory(), which uses a private Class field)
- Class.getInterfaces() (according to doc, it was returning all interfaces, but it turns out that in reality it
only should return the declared (direct) interfaces)
- cloning of primitive type arrays
The last one was the biggest change with quite some fan out - the real problem is yet again in the various different
naming schemes (type code, dot/builtin, L-dot, L-slash). DynamicArea.newArray() tried to be too smart, which ended up in an
ambiguity between builtin typecodes and user defined classes in the default package (e.g. "B"). Of course, we can
only test this if we also allow rawtest/JPF driver combos in a test/ default package (Java >1.4 doesn't allow
importing def package classes into named packages), which also required build.xml to be modified.
NOTE - DynmaicArea.newArray() now expects L-slash notation! If you use the MJIEnv.newObjectArray() facade, you can still use
normal dot names, but otherwise the burden is on the caller. THIS MIGHT BREAK SOME CODE OUT THERE
A pity we hav to go through all this for the stupid case somebody wants to name default package classes "B", "C" etc.
(which is unfortunately what everybody does with quick tests)
* Fields.equals() had a bug with attribute comparison (missing branches) - thanks Hank
Modified Paths:
--------------
trunk/build.xml
trunk/env/jpf/java/lang/Class.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_ConsoleOutputStream.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Class.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Object.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_System.java
trunk/extensions/statechart/env/jvm/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_sc_State.java
trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
trunk/src/gov/nasa/jpf/jvm/DynamicArea.java
trunk/src/gov/nasa/jpf/jvm/Fields.java
trunk/src/gov/nasa/jpf/jvm/MJIEnv.java
trunk/test/gov/nasa/jpf/jvm/TestJavaLangClass.java
trunk/test/gov/nasa/jpf/jvm/TestJavaLangClassJPF.java
Added Paths:
-----------
trunk/test/TestJavaLangObject.java
trunk/test/TestJavaLangObjectJPF.java
trunk/test/gov/nasa/jpf/jvm/TestEnum.java
trunk/test/gov/nasa/jpf/jvm/TestEnumJPF.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-12-27 19:16:32
|
Revision: 721
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=721&view=rev
Author: pcmehlitz
Date: 2007-12-27 11:16:30 -0800 (Thu, 27 Dec 2007)
Log Message:
-----------
* bag of patches from Jerry James - thanks!
- compiler warnings about deprecated method calls
- C compiler warnings for the native constraint solver interface code in extensions/symbolic/csrc
- javadoc hickup fixes (not that we really have javadoc docu - mea culpa)
- a LOT of StringBuffer/Builder cleanups (use StringBuilder, use explicit init, avoid
single-char strings etc.). Mostly minor performance optimizations, but there's no excuse of being sloppy. Now if only
somebody would step in and provide similar patches for replacing Debug (with our logging) and other ever-pending
cleanups
There seems to be a problem with older Solaris javac's when compiling Thread.exit(), but the
suggested fix would break Java SE6. However, that just brings up the issue of reinstating
Thread.exit(), which is next
Modified Paths:
--------------
trunk/env/jpf/java/lang/Thread.java
trunk/examples/ase2006/Crossing.java
trunk/examples/ase2006/CrossingListener.java
trunk/examples/ase2006/CrossingNative.java
trunk/examples/jpfESAS/launch/CV-generate-assumption-1.launch
trunk/extensions/LTL2Buchi/src/gov/nasa/ltl/graph/Attributes.java
trunk/extensions/LTL2Buchi/src/gov/nasa/ltl/graph/Edge.java
trunk/extensions/LTL2Buchi/src/gov/nasa/ltl/graph/Generate.java
trunk/extensions/LTL2Buchi/src/gov/nasa/ltl/graph/SM2Dot.java
trunk/extensions/LTL2Buchi/src/gov/nasa/ltl/trans/Formula.java
trunk/extensions/LTL2Buchi/src/gov/nasa/ltl/trans/Transition.java
trunk/extensions/cv/src/gov/nasa/jpf/cv/SETLearner.java
trunk/extensions/statechart/env/jvm/gov/nasa/jpf/jvm/NativeStateMachine.java
trunk/extensions/symbolic/csrc/cvcl-inc.c
trunk/extensions/symbolic/csrc/cvcl-incsolve.c
trunk/extensions/symbolic/csrc/cvcl.c
trunk/extensions/symbolic/csrc/yices-inc.c
trunk/extensions/symbolic/csrc/yices-incsolve.c
trunk/extensions/symbolic/csrc/yices.c
trunk/extensions/symbolic/src/gov/nasa/jpf/symbolic/dp/CVCLInterface.java
trunk/extensions/symbolic/src/gov/nasa/jpf/symbolic/dp/OmegaInterface.java
trunk/extensions/symbolic/src/gov/nasa/jpf/symbolic/integer/ConstraintBuilder.java
trunk/extensions/symbolic/src/gov/nasa/jpf/symbolic/integer/JPF_gov_nasa_jpf_symbolic_integer_SymbolicConstraints.java
trunk/extensions/symbolic/src/gov/nasa/jpf/symbolic/integer/Reconstruction.java
trunk/extensions/ui/src/gov/nasa/jpf/jvm/choice/ui/UIAction.java
trunk/extensions/ui/src/gov/nasa/jpf/tools/UIInspector.java
trunk/src/gov/nasa/jpf/Config.java
trunk/src/gov/nasa/jpf/jvm/AnnotationInfo.java
trunk/src/gov/nasa/jpf/jvm/ArrayFields.java
trunk/src/gov/nasa/jpf/jvm/BooleanChoiceGenerator.java
trunk/src/gov/nasa/jpf/jvm/ChoiceGenerator.java
trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
trunk/src/gov/nasa/jpf/jvm/DynamicArea.java
trunk/src/gov/nasa/jpf/jvm/ElementInfo.java
trunk/src/gov/nasa/jpf/jvm/FieldInfo.java
trunk/src/gov/nasa/jpf/jvm/Fields.java
trunk/src/gov/nasa/jpf/jvm/JVM.java
trunk/src/gov/nasa/jpf/jvm/MethodInfo.java
trunk/src/gov/nasa/jpf/jvm/SingleFieldLockInfo.java
trunk/src/gov/nasa/jpf/jvm/StackFrame.java
trunk/src/gov/nasa/jpf/jvm/StatisticFieldLockInfo.java
trunk/src/gov/nasa/jpf/jvm/ThreadData.java
trunk/src/gov/nasa/jpf/jvm/ThreadInfo.java
trunk/src/gov/nasa/jpf/jvm/Types.java
trunk/src/gov/nasa/jpf/jvm/Verify.java
trunk/src/gov/nasa/jpf/jvm/choice/CustomBooleanChoiceGenerator.java
trunk/src/gov/nasa/jpf/jvm/choice/DoubleThresholdGenerator.java
trunk/src/gov/nasa/jpf/jvm/choice/IntChoiceFromSet.java
trunk/src/gov/nasa/jpf/jvm/choice/IntIntervalGenerator.java
trunk/src/gov/nasa/jpf/jvm/choice/IntSpec.java
trunk/src/gov/nasa/jpf/jvm/choice/InvocationCG.java
trunk/src/gov/nasa/jpf/tools/GenPeer.java
trunk/src/gov/nasa/jpf/tools/GenPeerDispatcher.java
trunk/src/gov/nasa/jpf/tools/ObjectTracker.java
trunk/src/gov/nasa/jpf/tools/StateSpaceDot.java
trunk/src/gov/nasa/jpf/util/Debug.java
trunk/src/gov/nasa/jpf/util/DynamicIntArray.java
trunk/src/gov/nasa/jpf/util/DynamicObjectArray.java
trunk/src/gov/nasa/jpf/util/Inspector.java
trunk/src/gov/nasa/jpf/util/JPFRunner.java
trunk/src/gov/nasa/jpf/util/Printable.java
trunk/src/gov/nasa/jpf/util/script/Event.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-01-02 20:12:45
|
Revision: 722
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=722&view=rev
Author: pcmehlitz
Date: 2008-01-02 12:12:41 -0800 (Wed, 02 Jan 2008)
Log Message:
-----------
* finally took the time and fixed the annoying triple reporting of JPF internal exceptions
* also finally did proper adding/removal of threads to ThreadGroups, including the main thread. This came together
with some reworking of thread termination processing. In the standard libs, this is done by magically calling
a Thread.exit(), which then calls ThreadGroup.remove(t), but this involves locking and notification from the
global (shared) ThreadGroup object, and the last thing we want is additional states when we are done with the app.
So we forego a bit of fidelity in favor of readability/efficiency. Also updated the TestThread accordingly
* the cyclic reference between Thread<->ThreadGroup unveiled a bug in UntrackedManager, which was fixed temporarily
but needs to be revisited for performance reasons
with this out of the way, next in the list of open threading issues is to reinstate Verify.begin/endAtomic() the right way (if you really need it)
Modified Paths:
--------------
trunk/env/jpf/java/lang/Thread.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Thread.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_sun_misc_Unsafe.java
trunk/src/gov/nasa/jpf/JPFException.java
trunk/src/gov/nasa/jpf/jvm/DefaultSchedulerFactory.java
trunk/src/gov/nasa/jpf/jvm/JVM.java
trunk/src/gov/nasa/jpf/jvm/PrioritySchedulerFactory.java
trunk/src/gov/nasa/jpf/jvm/SchedulerFactory.java
trunk/src/gov/nasa/jpf/jvm/ThreadInfo.java
trunk/src/gov/nasa/jpf/jvm/ThreadList.java
trunk/src/gov/nasa/jpf/jvm/abstraction/abstractor/AbstractorBasedBuilder.java
trunk/src/gov/nasa/jpf/jvm/abstraction/filter/FilteringSerializer.java
trunk/src/gov/nasa/jpf/jvm/abstraction/filter/SimpleFilteringSerializer.java
trunk/src/gov/nasa/jpf/jvm/bytecode/ReturnInstruction.java
trunk/src/gov/nasa/jpf/jvm/untracked/UntrackedManager.java
trunk/test/gov/nasa/jpf/jvm/TestThread.java
trunk/test/gov/nasa/jpf/jvm/TestThreadJPF.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-01-03 23:57:26
|
Revision: 723
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=723&view=rev
Author: pcmehlitz
Date: 2008-01-03 15:57:24 -0800 (Thu, 03 Jan 2008)
Log Message:
-----------
* the die-hard Verify.begin/endAtomic() is back! It's a different animal though - it works by short-cutting
the CG creation in the SchedulerFactory instances, and tolerates data CGs inside of atomic sections. It still
does not allow blocking inside an atomic section, but other than the old version reports this as a
deadlock, i.e. property violation, and not a silly JPF internal error (which it isn't - it's an
application problem).
* this required some reshuffle of the deadlock detection, which now mostly resides in ThreadList
Modified Paths:
--------------
trunk/src/gov/nasa/jpf/jvm/DefaultSchedulerFactory.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/PrioritySchedulerFactory.java
trunk/src/gov/nasa/jpf/jvm/SystemState.java
trunk/src/gov/nasa/jpf/jvm/ThreadInfo.java
trunk/src/gov/nasa/jpf/jvm/ThreadList.java
trunk/src/gov/nasa/jpf/jvm/bytecode/ReturnInstruction.java
trunk/test/gov/nasa/jpf/mc/TestAtomic.java
Added Paths:
-----------
trunk/test/gov/nasa/jpf/mc/TestAtomicJPF.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-01-09 01:31:09
|
Revision: 726
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=726&view=rev
Author: pcmehlitz
Date: 2008-01-08 17:31:08 -0800 (Tue, 08 Jan 2008)
Log Message:
-----------
* refactoring of DCMPx, FCMPx, LCMP to better suit subclassing for the symbc extension - thanks to Adam Kiezun
* replaced the somewhat braindead clone() of the StackFrame hierarchy with a covariant version that's based on
the generic one. Removes a couple of superfluous casts, but more importantly removes the need for clone()
overriding in DirectCallStackFrame.
>> I'm sure there are a gazillion of other screwed clones that wait to be
cleaned up, so somebody could earn immortal fame doing this
* extended the InfoObject interface with a getClassInfo(), so that the aggregate type can be queried (returns
itself for ClassInfos)
* some work on the generic Contract.Satisfies, but it's NOT yet really working - the Predicate interface
needs to be based on Operand. Introduced a ContractContext (analogous to the slightly outdated TestContext)
for the purpose of explicit conversion (it's the dreaded ElementInfo -> Java object), but it's not complete yet.
At least that also solve the class resolution problem for Predicate classes (default - package of contract specifier)
Modified Paths:
--------------
trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
trunk/src/gov/nasa/jpf/jvm/DirectCallStackFrame.java
trunk/src/gov/nasa/jpf/jvm/InfoObject.java
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/DCMPG.java
trunk/src/gov/nasa/jpf/jvm/bytecode/DCMPL.java
trunk/src/gov/nasa/jpf/jvm/bytecode/FCMPG.java
trunk/src/gov/nasa/jpf/jvm/bytecode/FCMPL.java
trunk/src/gov/nasa/jpf/jvm/bytecode/LCMP.java
trunk/src/gov/nasa/jpf/report/Reporter.java
trunk/src/gov/nasa/jpf/test/Contract.java
trunk/src/gov/nasa/jpf/test/ContractSpec.g
trunk/src/gov/nasa/jpf/test/ContractSpecLexer.java
trunk/src/gov/nasa/jpf/test/ContractSpecParser.java
trunk/src/gov/nasa/jpf/tools/ContractVerifier.java
trunk/test/gov/nasa/jpf/test/TestContracts.java
Added Paths:
-----------
trunk/src/gov/nasa/jpf/test/ContractContext.java
trunk/src/gov/nasa/jpf/test/Predicate.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-01-22 22:58:48
|
Revision: 734
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=734&view=rev
Author: pcmehlitz
Date: 2008-01-22 14:58:47 -0800 (Tue, 22 Jan 2008)
Log Message:
-----------
* somehow, the attribute hashing for StackFrames got lost, and out of sync with Fields hashing. Now
it's in for both, but maybe we should turn it into an option
* SimpleDateFormat was missing a non-public method that is used from its DateFormat factory. The workaround
is kind of suboptimal, since we use the factory on the native side to indirectly create an equivalent
native DateFormat (since we can't call the package default method), but of course that is making
assumptions about library code we don't see
Modified Paths:
--------------
trunk/env/jpf/java/text/SimpleDateFormat.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_text_SimpleDateFormat.java
trunk/src/gov/nasa/jpf/jvm/Fields.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...> - 2008-01-25 18:47:31
|
Revision: 735
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=735&view=rev
Author: pcmehlitz
Date: 2008-01-25 10:47:30 -0800 (Fri, 25 Jan 2008)
Log Message:
-----------
* forgotten metrics builder reference in Eclipse .project file
* somehow the jpfESAS/doc dir got lost. Reinstated, but needs to be cleaned up
* bug in thread termination - we have to check if we can acquire the thread object lock for
post mortem notification, otherwise we can run into a locking assertion. For
consistency reasons moved the notification from ThreadInfo.finish() over to ReturnInstruction.execute
(better keep everything together). Used a MonitorEnterCG for blocking, which is slightly
suspicious since there is no corresponding MonitorExitCG, but should only matter if we
have SchedulerFactories that rely on symmetry (the monitor_exit is usually a left mover for
us anyways)
Modified Paths:
--------------
trunk/.project
trunk/src/gov/nasa/jpf/jvm/ThreadInfo.java
trunk/src/gov/nasa/jpf/jvm/bytecode/ReturnInstruction.java
Added Paths:
-----------
trunk/examples/jpfESAS/doc/
trunk/examples/jpfESAS/doc/Ascent-ambiguity.graffle
trunk/examples/jpfESAS/doc/Ascent-ambiguity.png
trunk/examples/jpfESAS/doc/Ascent-las.graffle
trunk/examples/jpfESAS/doc/Ascent-las.png
trunk/examples/jpfESAS/doc/Ascent.graffle
trunk/examples/jpfESAS/doc/Ascent.png
trunk/examples/jpfESAS/doc/CEV-example.html
trunk/examples/jpfESAS/doc/CEV_15EOR_LOR-DRM.png
trunk/examples/jpfESAS/doc/CEV_15EOR_LOR-model.png
trunk/examples/jpfESAS/doc/CEV_15EOR_LOR.graffle
trunk/examples/jpfESAS/doc/CEV_15EOR_LOR.png
trunk/examples/jpfESAS/doc/EarthOrbit-safehold.graffle
trunk/examples/jpfESAS/doc/EarthOrbit-safehold.png
trunk/examples/jpfESAS/doc/EarthOrbit-tli.graffle
trunk/examples/jpfESAS/doc/EarthOrbit-tli.png
trunk/examples/jpfESAS/doc/EarthOrbit.graffle
trunk/examples/jpfESAS/doc/EarthOrbit.png
trunk/examples/jpfESAS/doc/Entry.graffle
trunk/examples/jpfESAS/doc/Entry.png
trunk/examples/jpfESAS/doc/LunarOps.graffle
trunk/examples/jpfESAS/doc/LunarOps.png
trunk/examples/jpfESAS/doc/Transit.graffle
trunk/examples/jpfESAS/doc/cv.html
trunk/examples/jpfESAS/doc/demo-script.html
trunk/examples/jpfESAS/doc/doc.css
trunk/examples/jpfESAS/doc/executable-models.html
trunk/examples/jpfESAS/doc/jpf-statecharts.html
trunk/examples/jpfESAS/doc/model.html
trunk/examples/jpfESAS/doc/toolchain.graffle
trunk/examples/jpfESAS/doc/toolchain.png
trunk/examples/jpfESAS/doc/uml.html
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