Menu
▾
▴
javapathfinder-svn
|
From: <pcm...@us...> - 2008-09-18 18:47:56
|
Revision: 1017
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1017&view=rev
Author: pcmehlitz
Date: 2008-09-19 01:47:52 +0000 (Fri, 19 Sep 2008)
Log Message:
-----------
* added a dedicated NonSharedChecker, together with a better spec of what @NonShared means (this goes beyond
@NotThreadSafe, which is mostly covered by our race detection)
* added a test for @NonShared
* fixed a ConstChecker bug
* started on an annotation interface for Config settings, called @JPFConfig. In order to make this work,
we need a changelistener support for the Config object, which is done by adding a change API to Config
(append, setProperty - we leave the HashMap.put as a backdoor for now), and by adding a ConfigChangeListener
interface. It's going to take a while to add all the required listeners, but at least we have the
infrastructure. The Verify interface still needs to be added. There's also no class loadtime processing
for @JPFConfig yet (that's next)
I consider this feature to be only of use for main classes of SuT's that use property annotations which
should not be in the autoload list (e.g. like the NonSharedChecker, which packs a memory & performance
penalty).
Modified Paths:
--------------
trunk/app/gov/nasa/jpf/NonShared.java
trunk/src/gov/nasa/jpf/Config.java
trunk/src/gov/nasa/jpf/jvm/ElementInfo.java
trunk/src/gov/nasa/jpf/jvm/JVM.java
trunk/src/gov/nasa/jpf/tools/ConstChecker.java
trunk/src/gov/nasa/jpf/tools/ObjectTracker.java
trunk/src/gov/nasa/jpf/util/StateExtensionClient.java
trunk/src/gov/nasa/jpf/util/StateExtensionListener.java
trunk/test/gov/nasa/jpf/mc/TestAnnotationPropertiesJPF.java
Added Paths:
-----------
trunk/app/gov/nasa/jpf/JPFConfig.java
trunk/src/gov/nasa/jpf/ConfigChangeListener.java
trunk/src/gov/nasa/jpf/tools/NonSharedChecker.java
trunk/test/gov/nasa/jpf/test/TestNonShared.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-09-23 02:16:03
|
Revision: 1018
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1018&view=rev
Author: pcmehlitz
Date: 2008-09-23 02:15:51 +0000 (Tue, 23 Sep 2008)
Log Message:
-----------
* slightly modified the ConfigChangeListener interface, to include the Config object in the notification
* added some String[] delta methods to gov.nasa.jpf.util.Misc
* refactored Config a bit to better support runtime changes (incl. normalization) - there should be
a value processing layer that gets values passed in as Strings, instead of looking them up with a key
(only done ad hoc for a few methods so far)
* implemented JPF and JPF_java_util_Random ConfigChangeListeners. So far, that only supports
change of jpf.listener and cg.enuerate_random, but that's enough for TestNonShared and shows
how this is done (it's going to be a long haul, but in the end we can use this to control
JPF at runtime, e.g. from the plugins)
next up is to support a program interface via Verify
Modified Paths:
--------------
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_util_Random.java
trunk/src/gov/nasa/jpf/Config.java
trunk/src/gov/nasa/jpf/ConfigChangeListener.java
trunk/src/gov/nasa/jpf/JPF.java
trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
trunk/src/gov/nasa/jpf/jvm/InfoObject.java
trunk/src/gov/nasa/jpf/util/Misc.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-09-23 18:32:13
|
Revision: 1019
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1019&view=rev
Author: pcmehlitz
Date: 2008-09-23 18:27:50 +0000 (Tue, 23 Sep 2008)
Log Message:
-----------
* changed/activated the programmatic Verify.setProperties() API (same functionality as @JPFConfig)
* fixed Config.append()/setProperty() - beware of never using HashMap.get() unless you explicitly
want to avoid default lookup!
* reinstated '-show' command line arg. Nobody (including me) was able to remember the
jpf.report..start=..config.. (which is still there to support complete, reproducible reports)
* moved list property values (like vm.classpath etc.) from using ':' separators to ','
hopefully this will make it more easy to exchange property files between Windows and Unix
(the old ones [;: ] are still supported, but we might drop them to avoid filesystem clashes
and "L<typename>;" problems
Modified Paths:
--------------
trunk/default.properties
trunk/src/gov/nasa/jpf/Config.java
trunk/src/gov/nasa/jpf/JPF.java
trunk/src/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_jvm_Verify.java
trunk/test/gov/nasa/jpf/test/TestNonShared.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-09-24 18:45:27
|
Revision: 1020
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1020&view=rev
Author: pcmehlitz
Date: 2008-09-24 18:45:18 +0000 (Wed, 24 Sep 2008)
Log Message:
-----------
* added JPF.addUniqueTypeListener(..), to better support autoload capabilities (somebody might also load
those listeners explicitly). This required inclusion checks in Search/VM and the Multicasters
* fixed bug in Classnfo autoload mechanism (should keep own registry nonetheless)
* extended NonNullChecker to also support static and instance field checks. Semantics are debatable, but
at least consistent: throw AssertionErrors if
- a class with declared @NonNull ref fields doesn't have a ctor or clinit
- if a declared @NonNull reference field is not initialized at the end of a ctor or clinit execution
- if a PUTFIELD/PUTSTATIC nullifies a @NonNull field
maybe the ctor/clinit checks should only be performed at the end of the concrete type clinit/ctor, but I'd
rather keep attributes class local
Modified Paths:
--------------
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/VMListenerMulticaster.java
trunk/src/gov/nasa/jpf/search/Search.java
trunk/src/gov/nasa/jpf/search/SearchListenerMulticaster.java
trunk/src/gov/nasa/jpf/tools/NonNullChecker.java
trunk/test/gov/nasa/jpf/test/TestNonNull.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-09-27 03:00:07
|
Revision: 1027
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1027&view=rev
Author: pcmehlitz
Date: 2008-09-27 03:00:02 +0000 (Sat, 27 Sep 2008)
Log Message:
-----------
some more HeuristicSearch cleanup:
* created very simple HeuristicStateQueue. Much less sophisticated than the red-black tree based TreeMap,
but for limited queue sizes (which is one of the main purposes in life for HeuristicSearch) the simple
insert/remove and compare (no more Comparator) already offset the slower lookup. Uses less memory because
it is based on HeuristicState next/prev link fields (they ever get re-used)
* the sort order has changed slightly (was using state-id and hashcodes as secondary orders, but the
state-id is redundant to order of insert, and the hash codes are meaningless with respect to
heuristics. Still it might produce different traces than the old version
* DFSComparator wasn't overriding compare. DefaultComparator not required anymore. Removed
* not sure what the BeamSearch parent copying was about, it seemed superfluous. Removed
Modified Paths:
--------------
trunk/default.properties
trunk/src/gov/nasa/jpf/search/heuristic/BeamSearch.java
trunk/src/gov/nasa/jpf/search/heuristic/HeuristicSearch.java
trunk/src/gov/nasa/jpf/search/heuristic/HeuristicState.java
trunk/test/gov/nasa/jpf/mc/TestCrossingJPF.java
Added Paths:
-----------
trunk/src/gov/nasa/jpf/search/heuristic/HeuristicStateQueue.java
Removed Paths:
-------------
trunk/src/gov/nasa/jpf/search/heuristic/DFSComparator.java
trunk/src/gov/nasa/jpf/search/heuristic/DefaultComparator.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-10-01 01:20:06
|
Revision: 1028
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1028&view=rev
Author: pcmehlitz
Date: 2008-10-01 01:19:54 +0000 (Wed, 01 Oct 2008)
Log Message:
-----------
* updated the Eclipse launch configs (which are hopefully going away with the advent of Eclipse/NetBeans
*.jpf files) so that statechart extension scripts are specified with "+sc.script=..". This became
necessary because we've added the capability to query the arguments from the model code, which shouldn't
include the script.
* slight change in String expansion - alternatives ('..|..') and char classes ('..[..]..') are
expanded within string literals, and single quotes are automatically replaced with double quotes
('ab|cd' -> {"ab","cd"}. This is to make it more readable for double quote contexts like
annotation parameters, but it's not ideal. If single or double quotes should be preserved, they
have to be '\' escaped.
* for some unknown reason, the TestContext lost the check for compatible ctor args. Reinstated
(should make the MethodTester run again)
Modified Paths:
--------------
trunk/examples/jpfESAS/launch/CEV-ascent-guards.launch
trunk/examples/jpfESAS/launch/CEV-interactive-sim.launch
trunk/examples/jpfESAS/launch/CEV-las-defect-sim.launch
trunk/examples/jpfESAS/launch/CEV-las-defect.launch
trunk/examples/jpfESAS/launch/CEV-nominal-sim.launch
trunk/examples/jpfESAS/launch/CEV-safehold.launch
trunk/examples/jpfESAS/launch/CEV-scriptless-constraints.launch
trunk/examples/jpfESAS/launch/CEV-tli-sim.launch
trunk/examples/jpfESAS/launch/CEV-tli.launch
trunk/extensions/statechart/src/gov/nasa/jpf/tools/sc/SimStateMachine.java
trunk/src/gov/nasa/jpf/test/TestContext.java
trunk/src/gov/nasa/jpf/util/ExpandableStringReader.java
trunk/src/gov/nasa/jpf/util/StringExpander.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-10-03 02:30:59
|
Revision: 1030
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1030&view=rev
Author: pcmehlitz
Date: 2008-10-03 02:30:52 +0000 (Fri, 03 Oct 2008)
Log Message:
-----------
* the native Thread.sleep() had a twister, registering the CG in the never executed bottom half
* added a +et.skip_first option for the ExecTracker, to skip logging the first transition (which
is mostly the static init)
we need to have path set checkers for the mc test suite (some sort of 'expect' over path output)
Modified Paths:
--------------
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Thread.java
trunk/src/gov/nasa/jpf/tools/ExecTracker.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-10-14 22:29:11
|
Revision: 1034
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1034&view=rev
Author: pcmehlitz
Date: 2008-10-14 22:29:00 +0000 (Tue, 14 Oct 2008)
Log Message:
-----------
* added a first version of the PathOutputMonitor, which takes output specs and compares it
to the path outputs produced by the SuT. The error reporting still
needs to be polished, but it's mainly a tool for JPF verification anyways
the output matching could be significantly extended. So far it only supports simple per line
reg exps (plus a ". . ." ellipsis), but this could also use a parser and more elaborate
languages
* added a TestSchedules reg test that uses the PathOutputMonitor to check for transition breaks
upon Thread.sleep() calls with +cg.threads.break_all=true
Modified Paths:
--------------
trunk/default.properties
trunk/src/gov/nasa/jpf/jvm/JVM.java
Added Paths:
-----------
trunk/src/gov/nasa/jpf/tools/PathOutputMonitor.java
trunk/test/gov/nasa/jpf/mc/TestSchedules-output
trunk/test/gov/nasa/jpf/mc/TestSchedules.java
trunk/test/gov/nasa/jpf/mc/TestSchedulesJPF.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <ada...@us...> - 2008-10-20 15:09:42
|
Revision: 1044
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1044&view=rev
Author: adam_kiezun
Date: 2008-10-20 15:09:17 +0000 (Mon, 20 Oct 2008)
Log Message:
-----------
initial check in of concolic extension and jFuzz whitebox fuzzer (contributed by Adam Kiezun and David Harvison from MIT)
Modified Paths:
--------------
trunk/.classpath
Added Paths:
-----------
trunk/extensions/concolic/ReadMe.html
trunk/extensions/concolic/lib/jpaul-2.5.1.jar
trunk/extensions/concolic/lib/jpaul-license.txt
trunk/extensions/concolic/src/gov/
trunk/extensions/concolic/src/gov/nasa/
trunk/extensions/concolic/src/gov/nasa/jpf/
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/ConcolicInstructionFactory.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/BytecodeUtils.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/D2I.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/D2L.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/DADD.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/DCMPG.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/DCMPL.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/DDIV.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/DMUL.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/DNEG.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/DREM.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/DSUB.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/F2I.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/F2L.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/FADD.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/FCMPG.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/FCMPL.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/FDIV.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/FMUL.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/FNEG.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/FREM.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/FSUB.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/I2D.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/I2F.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/IADD.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/IAND.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/IDIV.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/IFEQ.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/IFGE.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/IFGT.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/IFLE.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/IFLT.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/IFNE.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/IF_ICMPEQ.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/IF_ICMPGE.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/IF_ICMPGT.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/IF_ICMPLE.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/IF_ICMPLT.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/IF_ICMPNE.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/IINC.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/IMUL.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/INEG.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/INVOKESPECIAL.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/INVOKESTATIC.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/INVOKEVIRTUAL.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/IOR.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/IREM.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/ISUB.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/IXOR.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/L2D.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/L2F.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/LADD.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/LAND.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/LCMP.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/LDIV.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/LMUL.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/LNEG.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/LOR.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/LREM.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/LSHL.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/LSHR.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/LSUB.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/LUSHR.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/LXOR.java
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/bytecode/package.html
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/package.html
trunk/extensions/concolic/src/gov/nasa/jpf/util/
trunk/extensions/concolic/src/gov/nasa/jpf/util/CollectionsExt.java
trunk/extensions/concolic/src/gov/nasa/jpf/util/Command.java
trunk/extensions/concolic/src/gov/nasa/jpf/util/Files.java
trunk/extensions/concolic/src/jfuzz/
trunk/extensions/concolic/src/jfuzz/ConcolicListener.java
trunk/extensions/concolic/src/jfuzz/DebugFuzz.java
trunk/extensions/concolic/src/jfuzz/JFuzz.java
trunk/extensions/concolic/src/jfuzz/JFuzzConfig.java
trunk/extensions/concolic/src/jfuzz/JPF_jfuzz_DebugFuzz.java
trunk/extensions/concolic/src/jfuzz/PathCache.java
trunk/extensions/concolic/src/jfuzz/SimplifyPC.java
trunk/extensions/concolic/src/jfuzz/package.html
trunk/extensions/concolic/src/jfuzz/termination/
trunk/extensions/concolic/src/jfuzz/termination/NeverTerminate.java
trunk/extensions/concolic/src/jfuzz/termination/TerminationStrategy.java
trunk/extensions/concolic/src/jfuzz/termination/TimedTermination.java
trunk/extensions/concolic/src/jfuzz/termination/UpToFixedNumber.java
trunk/extensions/concolic/test/gov/
trunk/extensions/concolic/test/gov/nasa/
trunk/extensions/concolic/test/gov/nasa/jpf/
trunk/extensions/concolic/test/gov/nasa/jpf/concolic/
trunk/extensions/concolic/test/gov/nasa/jpf/concolic/tests/
trunk/extensions/concolic/test/gov/nasa/jpf/concolic/tests/CharMultiArrayPC.java
trunk/extensions/concolic/test/gov/nasa/jpf/concolic/tests/CharPC.java
trunk/extensions/concolic/test/gov/nasa/jpf/concolic/tests/JPF_gov_nasa_jpf_concolic_tests_TestUtils.java
trunk/extensions/concolic/test/gov/nasa/jpf/concolic/tests/MultiArgsPC.java
trunk/extensions/concolic/test/gov/nasa/jpf/concolic/tests/MultiPC.java
trunk/extensions/concolic/test/gov/nasa/jpf/concolic/tests/SimpleCharArrayPC.java
trunk/extensions/concolic/test/gov/nasa/jpf/concolic/tests/SimplePC.java
trunk/extensions/concolic/test/gov/nasa/jpf/concolic/tests/TestUtils.java
trunk/extensions/concolic/test/gov/nasa/jpf/concolic/unitTests/
trunk/extensions/concolic/test/gov/nasa/jpf/concolic/unitTests/AbstractConcolicTest.java
trunk/extensions/concolic/test/gov/nasa/jpf/concolic/unitTests/AllTests.java
trunk/extensions/concolic/test/gov/nasa/jpf/concolic/unitTests/ArrayTest.java
trunk/extensions/concolic/test/gov/nasa/jpf/concolic/unitTests/SimpleTest.java
trunk/extensions/concolic/test/jfuzz/
trunk/extensions/concolic/test/jfuzz/tests/
trunk/extensions/concolic/test/jfuzz/tests/LargePC.java
trunk/extensions/concolic/test/jfuzz/tests/MultipleVars.java
trunk/extensions/concolic/test/jfuzz/tests/MyClass3.java
trunk/extensions/concolic/test/jfuzz/tests/ReadChars.java
trunk/extensions/concolic/test/jfuzz/tests/ReadChars2.java
trunk/extensions/concolic/test/jfuzz/tests/ReadFile.java
trunk/extensions/concolic/test/jfuzz/tests/ReadLargeFile.java
trunk/extensions/concolic/test/jfuzz/tests/StringSym.java
trunk/extensions/concolic/test/jfuzz/tests/StringTest.java
trunk/extensions/concolic/test/jfuzz/tests/TwoClass.java
trunk/extensions/concolic/test/jfuzz/tests/TwoClass2.java
trunk/extensions/concolic/test/jfuzz/unitTests/
trunk/extensions/concolic/test/jfuzz/unitTests/AbstractJFuzzTest.java
trunk/extensions/concolic/test/jfuzz/unitTests/AllTests.java
trunk/extensions/concolic/test/jfuzz/unitTests/ReadTest.java
trunk/extensions/concolic/test/jfuzz/unitTests/SimpleTest.java
trunk/extensions/concolic/test/jfuzz/unitTests/SimplifyPCTest.java
trunk/extensions/concolic/test/txtfiles/
trunk/extensions/concolic/test/txtfiles/2class.txt
trunk/extensions/concolic/test/txtfiles/file.txt
trunk/extensions/concolic/test/txtfiles/largepc.txt
trunk/extensions/concolic/test/txtfiles/multiVars.txt
trunk/extensions/concolic/test/txtfiles/myclass3.txt
trunk/extensions/concolic/test/txtfiles/readChars.txt
trunk/extensions/concolic/test/txtfiles/stringsym.txt
trunk/extensions/concolic/test/txtfiles/ulyss12.txt
Property Changed:
----------------
trunk/extensions/concolic/
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-10-22 18:41:52
|
Revision: 1047
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1047&view=rev
Author: pcmehlitz
Date: 2008-10-22 18:41:46 +0000 (Wed, 22 Oct 2008)
Log Message:
-----------
* added a few more tests for a missing 'target' property, which should be intercepted at the very beginning,
before JPF ever tries to initialize the JVM
Modified Paths:
--------------
trunk/doc/about_us.html
trunk/doc/navigation.html
trunk/src/gov/nasa/jpf/JPF.java
trunk/src/gov/nasa/jpf/jvm/JVM.java
trunk/test/gov/nasa/jpf/mc/TestRandom.java
trunk/test/gov/nasa/jpf/mc/TestRandomJPF.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-11-04 02:40:53
|
Revision: 1057
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1057&view=rev
Author: pcmehlitz
Date: 2008-11-04 02:40:45 +0000 (Tue, 04 Nov 2008)
Log Message:
-----------
* added ClassLoader support for NativePeer and InstructionFactory. Actually, NativePeer was already using a loader, only that it was missing the init. InstructionFactory also loads the bcel classes with the loader, which is questionable (but should always work because it is parented). Now we have the following (optional) new classpath properties
jpf.listener.classpath
vm.peer.classpath
vm.insn_factory.classpath
a malformed path inside those properties now throws a Config.Exception
* moved the loader instantiation into Config, since it's used from different places
* WATCH OUT: changed vm.peer_packages into vm.peer.packages. Could only find two refs in the concolic extension *.launch files, which have been updated, but people might have their own launch configs
Modified Paths:
--------------
trunk/default.properties
trunk/extensions/complexcoverage/test/ComplexCoverage DoubleTest Normal.launch
trunk/extensions/complexcoverage/test/ComplexCoverage TestFun Symbolic.launch
trunk/src/gov/nasa/jpf/Config.java
trunk/src/gov/nasa/jpf/JPF.java
trunk/src/gov/nasa/jpf/jvm/DefaultInstructionFactory.java
trunk/src/gov/nasa/jpf/jvm/InstructionFactory.java
trunk/src/gov/nasa/jpf/jvm/MethodInfo.java
trunk/src/gov/nasa/jpf/jvm/NativePeer.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...> - 2008-11-07 01:55:52
|
Revision: 1060
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1060&view=rev
Author: pcmehlitz
Date: 2008-11-07 01:55:48 +0000 (Fri, 07 Nov 2008)
Log Message:
-----------
sometimes less is more..
* replaced all the specialized classloader properties (jpf.listener.classpath, vm.peer.classpath, vm.insn_factory.classpath) with the one and only "jpf.native_classpath", together with Config.{sg}etCurrentClassLoader() methods that manage a Config global classloader, which is implicitly used in all the getClass()/get[Essential]Instance() methods
RATIONALE: extending the host VM classpath via JPF properties serves the purpose of enabling JPF extensions outside the JPF project, to be usable in environments where the system class.path cannot be controlled (e.g. when using JPF from an Eclipse plugin). In this case, it is most likely that there is more than one extension component involved (e.g. listener and native peer), but they are probably kept in the same jar or project. In this case, having all these dedicated classloader properties would require a lot of duplication, running the danger of inconsistencies. This is even more important because we should consistently support classpath extensions for (almost) all configured JPF classes (Search, Heuristic, SchedulerFactory, whatever), i.e. there would have been a lot more of dedicated ...classpaths. Now we just do this once during JPF init. The lost functionality of not being able to mix different components from name-clashing external extension projects seems acceptable.
A a side effect, the Config API becomes more manageable again, too. Sorry if somebody already used the new ...classpaths - typical case of premature idea
Modified Paths:
--------------
trunk/default.properties
trunk/src/gov/nasa/jpf/Config.java
trunk/src/gov/nasa/jpf/JPF.java
trunk/src/gov/nasa/jpf/jvm/DefaultInstructionFactory.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...> - 2008-11-08 03:30:59
|
Revision: 1062
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1062&view=rev
Author: pcmehlitz
Date: 2008-11-08 03:30:54 +0000 (Sat, 08 Nov 2008)
Log Message:
-----------
* fixed the broken GenericInstructionFactory init. Concrete InstructionFactory implementors now have to pass the Config argument up to their super classes. The DefaultInstructionFactory ctor initializes the factory's classloader. With this, the InstructionFactory.init(conf) becomes obsolete and gets removed. - Thanks Taehoon
Had to update the extension factory ctors with "super(Config,..)" calls, but that should not affect anything else in there.
Modified Paths:
--------------
trunk/extensions/concolic/src/gov/nasa/jpf/concolic/ConcolicInstructionFactory.java
trunk/extensions/numeric/src/gov/nasa/jpf/numeric/NumericInstructionFactory.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/SymbolicInstructionFactory.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/DefaultInstructionFactory.java
trunk/src/gov/nasa/jpf/jvm/InstructionFactory.java
trunk/src/gov/nasa/jpf/jvm/MethodInfo.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...> - 2008-11-18 02:21:19
|
Revision: 1063
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1063&view=rev
Author: pcmehlitz
Date: 2008-11-18 02:21:14 +0000 (Tue, 18 Nov 2008)
Log Message:
-----------
* overhaul of the HeuristicSearch infrastructure. There was a combination of over-engineering (search class and separate Heuristic) and lack of flexibility (only static int priority for each state, computed at state storage time). Now there are only concrete HeuristicSearch subclasses, which can also define their own queue mechanism, which for instance can be used to compute priorities once all child states have been generated, or at state restore time. We don't make assumptions in HeuristicSearch about either the queue or the underlying concrete HeuristicState, which could also have more elaborated ways to store priorities. As a side effect, configuration has become more easy, since we only have to set +search.heuristic.class
* added parentState and childStates fields to HeuristicSearch, which can be used in subclasses to compute heuristic values depending on the parent or the complete child set
* added a SimplePriorityHeuristics base class that implements the old, static, int- based priority states, which are queued in a bounded TreeSet. Did some extensive performance comparisons with PriorityQueues and binary-sorted arrays w/ block copies, but there was no clearly superior solution that is independent of queue limit, add/remove ratio, or even processor architecture, so we use the least expensive implementation, which was the existing java.util.TreeSet
I didn't dare to fix the inverse priorities, i.e. '0' still represents the highest priority
Modified Paths:
--------------
trunk/src/gov/nasa/jpf/search/DFSearch.java
trunk/src/gov/nasa/jpf/search/PathSearch.java
trunk/src/gov/nasa/jpf/search/RandomSearch.java
trunk/src/gov/nasa/jpf/search/Search.java
trunk/src/gov/nasa/jpf/search/Simulation.java
trunk/src/gov/nasa/jpf/search/heuristic/BFSHeuristic.java
trunk/src/gov/nasa/jpf/search/heuristic/ChooseFree.java
trunk/src/gov/nasa/jpf/search/heuristic/DFSHeuristic.java
trunk/src/gov/nasa/jpf/search/heuristic/GlobalSwitchThread.java
trunk/src/gov/nasa/jpf/search/heuristic/HeuristicSearch.java
trunk/src/gov/nasa/jpf/search/heuristic/HeuristicState.java
trunk/src/gov/nasa/jpf/search/heuristic/Interleaving.java
trunk/src/gov/nasa/jpf/search/heuristic/MostBlocked.java
trunk/src/gov/nasa/jpf/search/heuristic/PreferThreads.java
trunk/src/gov/nasa/jpf/search/heuristic/RandomHeuristic.java
trunk/src/gov/nasa/jpf/search/heuristic/UserHeuristic.java
trunk/src/gov/nasa/jpf/tools/CGMonitor.java
trunk/test/gov/nasa/jpf/mc/TestCrossingJPF.java
trunk/test/gov/nasa/jpf/mc/TestOldClassicJPF.java
trunk/test/gov/nasa/jpf/mc/TestRandomJPF.java
Removed Paths:
-------------
trunk/src/gov/nasa/jpf/search/heuristic/BeamSearch.java
trunk/src/gov/nasa/jpf/search/heuristic/DefaultHeuristic.java
trunk/src/gov/nasa/jpf/search/heuristic/Heuristic.java
trunk/src/gov/nasa/jpf/search/heuristic/HeuristicStateQueue.java
trunk/src/gov/nasa/jpf/search/heuristic/PathSensitiveHeuristic.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-11-18 18:39:11
|
Revision: 1065
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1065&view=rev
Author: pcmehlitz
Date: 2008-11-18 18:39:05 +0000 (Tue, 18 Nov 2008)
Log Message:
-----------
* we can't use TreeSet.pollFirst()/pollLast() because they are only in Java 1.6, which we can't switch to because it's not available for PPC. Going back to Java 1.5 remove(first()/last()) requires "compareTo(o)==0" equivalence to "equals(o) == true" for PrioritizedState [I don't know how often I get this wrong]
* also re-renamed 'priority' to 'heuristicValue', since the inverted priorities were too confusing. Lower heuristicValues mean higher priorities
* on top of that, PrioritizedState.compareTo() had a leftover debug-bug (yesterday wasn't my best day)
NOTE: even my previous commit message was wrong - of course it's (only) +search.class that has to be set. In fact, the old +search.heuristic.class is obsolete (should update default.properties)
Modified Paths:
--------------
trunk/examples/Rand.java
trunk/src/gov/nasa/jpf/search/heuristic/PrioritizedState.java
trunk/src/gov/nasa/jpf/search/heuristic/SimplePriorityHeuristic.java
trunk/src/gov/nasa/jpf/search/heuristic/StaticPriorityQueue.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-11-20 06:09:46
|
Revision: 1070
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1070&view=rev
Author: pcmehlitz
Date: 2008-11-20 06:09:43 +0000 (Thu, 20 Nov 2008)
Log Message:
-----------
* added value appends to Config - a spec like "foo.bar+=,doo" now appends ",doo" to whatever current value is stored under "foo.bar". Needless to say it's useless within defaults.properties, but it is supported for both mode property files and command line args
NOTE - since we use the standard Properties.load(), this is a bit quirked: there is no blank allowed between the last key char and the '+', i.e. "foo.bar += ,doo" DOES NOT WORK
* first part of reworked +vm.sourcepath handling (now done centralized from ClassInfo, i.e. no more hardcoded defaults in jpf.util.Sources). So far, not much has changed for the user, but this will be extended towards *.jar support
Modified Paths:
--------------
trunk/jpf.properties
trunk/src/gov/nasa/jpf/Config.java
trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
trunk/src/gov/nasa/jpf/util/Source.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-11-21 05:32:18
|
Revision: 1074
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1074&view=rev
Author: pcmehlitz
Date: 2008-11-21 05:32:11 +0000 (Fri, 21 Nov 2008)
Log Message:
-----------
* vm.sourcepath now also supports jars, including archive internal root dirs (as in ../hum/di/dum/src.jar/src). Note that even on Windows, archive internal paths have to use '/', i.e. these "jar paths" have a filesystem- and an archive- part.
* because of this, Config now only recognizes ',' as separator for String arrays
!!!! IF YOU USED ':' OR ' ' OR ';' AS SEPARATORS IN *.properties, *.jpf OR ECLIPSE *.launch FILES, YOU HAVE TO CHANGE THEM !!!!
* little fix on the go - if BCEL doesn't report a source file, and we have to guess it from the class name, we should use the outermost encapsulating class name (note this doesn't help for non-public classes)
Modified Paths:
--------------
trunk/default.properties
trunk/examples/ICSETutorial/launch/Tutorial-CEV-scriptless-bt.launch
trunk/examples/ICSETutorial/launch/Tutorial-CV-generate-assumption-1.launch
trunk/examples/ICSETutorial/launch/Tutorial-CV-generate-assumption-2.launch
trunk/examples/ICSETutorial/launch/Tutorial-InputWithProperty-UseAssumption.launch
trunk/examples/ICSETutorial/launch/Tutorial-InputWithProperty-generateAssumption.launch
trunk/examples/ICSETutorial/launch/Tutorial-InputWithProperty-scriptless.launch
trunk/examples/ICSETutorial/launch/Tutorial-Output-dischargeAssumption.launch
trunk/examples/jpfESAS/launch/CEV-scriptless-bt.launch
trunk/examples/jpfESAS/launch/CEV-scriptless-constraints.launch
trunk/examples/jpfESAS/launch/CEV-scriptless.launch
trunk/examples/jpfESAS/launch/CV-assumption-1.launch
trunk/examples/jpfESAS/launch/CV-assumptions-1-2.launch
trunk/examples/jpfESAS/launch/CV-generate-assumption-1.launch
trunk/examples/jpfESAS/launch/CV-generate-assumption-2.launch
trunk/examples/launch/basic-racer.launch
trunk/examples/launch/basic-random.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
trunk/extensions/complexcoverage/test/ComplexCoverage DoubleTest Normal.launch
trunk/extensions/complexcoverage/test/ComplexCoverage TestFun Normal.launch
trunk/extensions/complexcoverage/test/ComplexCoverage TestFun Reduce.launch
trunk/extensions/complexcoverage/test/ComplexCoverage TestFun Run Reduced Test #0.launch
trunk/extensions/complexcoverage/test/ComplexCoverage TestFun Symbolic.launch
trunk/src/gov/nasa/jpf/Config.java
trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
trunk/src/gov/nasa/jpf/jvm/JVM.java
trunk/src/gov/nasa/jpf/report/ConsolePublisher.java
trunk/src/gov/nasa/jpf/report/Reporter.java
trunk/src/gov/nasa/jpf/report/XMLPublisher.java
trunk/src/gov/nasa/jpf/util/Source.java
trunk/src/gov/nasa/jpf/util/SourceRef.java
trunk/test/gov/nasa/jpf/mc/TestAnnotationPropertiesJPF.java
trunk/test/gov/nasa/jpf/mc/TestDataChoiceJPF.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-11-22 02:45:45
|
Revision: 1075
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1075&view=rev
Author: pcmehlitz
Date: 2008-11-22 02:45:39 +0000 (Sat, 22 Nov 2008)
Log Message:
-----------
* added a "jpf.report.show_repository" property (which is 'false' by default) for debugging purposes. If it is set, and JPF is built from an SVN checkout, the reporter tries to locate the "{jpf.basedir}/.svn/entries" file, and pulls the revision, DTG and repository location out of it. The whole shebang is reported in the JPF banner
This is mostly to verify what versions where used for bug reports
Modified Paths:
--------------
trunk/default.properties
trunk/src/gov/nasa/jpf/report/ConsolePublisher.java
trunk/src/gov/nasa/jpf/report/Reporter.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-11-25 20:18:58
|
Revision: 1081
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1081&view=rev
Author: pcmehlitz
Date: 2008-11-25 20:18:56 +0000 (Tue, 25 Nov 2008)
Log Message:
-----------
NetBeans 6.5 compatibility
* a number of changes to make the NetBeans 6.5 compiler happy when compiling overridden lib classes (mostly visibility and type erasure stuff)
* with the release of NetBeans 6.5, the RunJPF dependencies had to be changed (ClassPath API is now in it's own module)
NOTE - this will cause problems when trying to build on NetBeans 6.1, but we can only support one version, so it's the latest & greatest
Modified Paths:
--------------
trunk/env/jpf/gov/nasa/jpf/SerializationConstructor.java
trunk/env/jpf/java/lang/System.java
trunk/env/jpf/java/lang/reflect/Constructor.java
trunk/env/jpf/java/text/DecimalFormat.java
trunk/env/jpf/java/text/NumberFormat.java
trunk/ide/examples/JPFTest/build.xml
trunk/ide/examples/JPFTest/nbproject/build-impl.xml
trunk/ide/examples/JPFTest/nbproject/genfiles.properties
trunk/ide/netbeans/RunJPF/nbproject/genfiles.properties
trunk/ide/netbeans/RunJPF/nbproject/project.xml
trunk/ide/netbeans/RunJPF/src/gov/nasa/runjpf/RunJPF.java
trunk/nbproject/project.xml
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-12-04 20:14:39
|
Revision: 1097
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1097&view=rev
Author: pcmehlitz
Date: 2008-12-04 20:14:37 +0000 (Thu, 04 Dec 2008)
Log Message:
-----------
* finally added a daemon-aware termination policy, but as usual it's just raising more questions. Depending on the OS, a production VM might still run daemons for a few cycles after the last non-daemon dies. Apparently, the guarantee is only that daemons terminate *eventually* (even though that's not what the documentation says). Depending on whether that's a bug or a feature, we actually might check for this case because it could cause some interestig defects if people rely on daemons being terminated instantaneously.
Implementing daemon termination also brought back to attention that program termination and SchedulingPolicy are sort of redundant (which makes it error prone). Currently, we can return a non-empty CG upon thread termination and still implement VM.isEndState() to say differently (as it is the case right now). This is bad if we want to rely on SchedulingPolicy to model platforms ==> re-check what the VM spec says about daemons
* added a daemon termination test case
* added a JTextField model, to support TextField entries with/without return (to model the latter, we can just do a setText("...\n") to fire the ActionEvent, which wouldn't work with the real JTextField).
That's not nice, since in general we just want to cut off the BasicTextFieldUI (i.e. leave the plaf independent model classes alone so that we don't have to muck with swing data/selection models), but that would force us to split events, i.e. blow up scripts and hence state space. This raises the interesting question of adding dedicated event APIs. So far, we just go with public Swing component methods (like doClick() etc.), but that might not be enough (e.g. if there is no "high level" user action API in the component), or inconvenient (like with the 'return' case above)
* little unit test for UIScriptEnvironment parameter expansion
* added a missing InputStreamReader ctor used by Taehoon's servlet extension - in general, we should strive to avoid replaced core classes in extensions if this is only about missing standard APIs that don't require extension specific implementation. This is NOT to say people should start to wildly commit to core because of extension requirements - just report
Modified Paths:
--------------
trunk/env/jpf/java/io/InputStreamReader.java
trunk/extensions/ui/env/jpf/javax/swing/JComponent.java
trunk/extensions/ui/src/gov/nasa/jpf/jvm/choice/ui/UIScriptEnvironment.java
trunk/src/gov/nasa/jpf/jvm/DefaultSchedulerFactory.java
trunk/src/gov/nasa/jpf/jvm/KernelState.java
trunk/src/gov/nasa/jpf/jvm/ThreadList.java
trunk/test/gov/nasa/jpf/jvm/TestThread.java
trunk/test/gov/nasa/jpf/jvm/TestThreadJPF.java
Added Paths:
-----------
trunk/extensions/ui/env/jpf/javax/swing/JTextField.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-12-07 03:07:28
|
Revision: 1105
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1105&view=rev
Author: pcmehlitz
Date: 2008-12-07 03:07:23 +0000 (Sun, 07 Dec 2008)
Log Message:
-----------
* par force trip to add javax.swing.JList selection modeling, which in turn required the plaf UI, the JScrollPane, which in turn required the JScrollBars and the JViewport. Needless to say all these classes are only fragments, but the JList preserves the ListModel, the SelectionModel, and the component hierarchy (including CellRendererPane for client controlled item rendering). I'm actually surprised it didn't suck in more
* fixed the state enforcement in the EventDispatchThread peer - we shouldn't enforce for every event, but for every new CG. If we don't do that, chances are we miss important paths because we have scripts that revert previous actions before we throw interesting actions at the system (like clicking twice on JCheckBoxes - which we currently need if we want all permutations of a CheckBox set).
We certainly loose on a couple of states we could match, but we still can match ANY choices that don't change the program state, and of course all UI external CGs (like threading)
* with that, implemented RobotManager - a fairly involved UI model checking example that has two defects: (1) violating an assertion due to "illegal" checkbox state combinations, and (2) a null object call due to a thread interleaving. The latter one is pretty cool and JPF finds it in ~25000 states
* finally set the Inspector background color so that it can be distinguished from the application windows
* in the age of AutoLoadedListeners, the TestConst/TestNonNull/TestNonShared launch configs don't need explicit jpf.listener settings anymore
* null handling in Instruction.getSourceLine() - thanks Michal!
Modified Paths:
--------------
trunk/.classpath
trunk/extensions/ui/env/jpf/java/awt/Component.java
trunk/extensions/ui/env/jpf/java/awt/Container.java
trunk/extensions/ui/env/jpf/java/awt/Toolkit.java
trunk/extensions/ui/env/jpf/javax/swing/JComponent.java
trunk/extensions/ui/env/jpf/javax/swing/JLabel.java
trunk/extensions/ui/env/jpf/javax/swing/UIManager.java
trunk/extensions/ui/env/jpf/javax/swing/plaf/ListUI.java
trunk/extensions/ui/env/jpf/javax/swing/plaf/TextUI.java
trunk/extensions/ui/env/jpf/javax/swing/plaf/basic/BasicTextFieldUI.java
trunk/extensions/ui/env/jpf/javax/swing/plaf/basic/BasicTextUI.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/extensions/ui/src/gov/nasa/jpf/tools/UIInspector.java
trunk/src/gov/nasa/jpf/jvm/bytecode/Instruction.java
trunk/src/gov/nasa/jpf/util/Inspector.java
trunk/src/gov/nasa/jpf/util/script/ScriptEnvironment.java
trunk/test/gov/nasa/jpf/test/TestConst.launch
trunk/test/gov/nasa/jpf/test/TestContracts.java
Added Paths:
-----------
trunk/extensions/ui/env/jpf/javax/swing/JList.java
trunk/extensions/ui/env/jpf/javax/swing/JScrollBar.java
trunk/extensions/ui/env/jpf/javax/swing/JScrollPane.java
trunk/extensions/ui/env/jpf/javax/swing/JViewport.java
trunk/extensions/ui/env/jpf/javax/swing/plaf/basic/BasicListUI.java
trunk/extensions/ui/env/jpf/javax/swing/plaf/basic/BasicViewportUI.java
trunk/extensions/ui/examples/
trunk/extensions/ui/examples/RobotManager.java
trunk/test/gov/nasa/jpf/test/TestNonNull.launch
trunk/test/gov/nasa/jpf/test/TestNonShared.launch
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-12-09 07:47:49
|
Revision: 1109
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1109&view=rev
Author: pcmehlitz
Date: 2008-12-09 07:47:43 +0000 (Tue, 09 Dec 2008)
Log Message:
-----------
too much..
* expanded the RobotManager UI model checking example with a data acquisition thread - blowing up the state space a bit (JPF finds the high level race after about 25k states). This includes a number of launch configs, input scripts, and mode property files
* extended the Inspector to include mode properties. The JTextArea contents are taken at JPF start time and superpositioned to the config that was used to start the Inspector
* to completely confuse people - added a 'jpf.shell' property which can be used to start JPF starters (like the UIInspector) from JPF.main. This is mainly so that people just have to start JPF with a mode property file (*.jpf) and can push everything else into the *.jpf
* extended and renamed the NonSharedChecker so that we can specify a number of thread names via @Shared({tn1,tn2,...}). Also optimized its inner workings (working off GETFIELD, using the pushed value). Now it's the SharedChecker
* added a MethodAnalyzer listener that keeps track of method operations (call, call/execute, execute, return), pretty much like the DealockAnalyzer does so for threading operations (i.e. not requiring step tracing). This definitely needs more testing and some functional enhancements, but it already can help to understand large traces.
However, ultimately we need the external trace server with configured filters - that should be more effective to save memory and avoids backtracking overhead
Modified Paths:
--------------
trunk/examples/launch/conc-0-RA-test.launch
trunk/extensions/ui/examples/RobotManager.java
trunk/extensions/ui/src/gov/nasa/jpf/tools/UIInspector.java
trunk/src/gov/nasa/jpf/Config.java
trunk/src/gov/nasa/jpf/JPF.java
trunk/src/gov/nasa/jpf/jvm/bytecode/VirtualInvocation.java
trunk/src/gov/nasa/jpf/tools/ExecTracker.java
trunk/src/gov/nasa/jpf/util/Inspector.java
trunk/src/gov/nasa/jpf/util/JPFRunner.java
trunk/test/gov/nasa/jpf/test/TestNonShared.java
Added Paths:
-----------
trunk/app/gov/nasa/jpf/Shared.java
trunk/extensions/ui/examples/RobotManager nothread.launch
trunk/extensions/ui/examples/RobotManager test.launch
trunk/extensions/ui/examples/RobotManager thread.launch
trunk/extensions/ui/examples/RobotManager-nothread.es
trunk/extensions/ui/examples/RobotManager-nothread.jpf
trunk/extensions/ui/examples/RobotManager-thread.es
trunk/extensions/ui/examples/RobotManager-thread1.jpf
trunk/extensions/ui/examples/RobotManager-thread2.jpf
trunk/extensions/ui/examples/RobotManager-thread3.jpf
trunk/extensions/ui/examples/RobotManager-thread4.jpf
trunk/src/gov/nasa/jpf/tools/MethodAnalyzer.java
trunk/src/gov/nasa/jpf/tools/SharedChecker.java
Removed Paths:
-------------
trunk/src/gov/nasa/jpf/tools/NonSharedChecker.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2009-01-03 01:23:50
|
Revision: 1125
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1125&view=rev
Author: pcmehlitz
Date: 2009-01-03 01:23:45 +0000 (Sat, 03 Jan 2009)
Log Message:
-----------
* added a vm.por.skip_finals, which causes GET/PUT insns on shared finals to be ignored as POR field
boundaries. For statics, that should be mostly true (esp. since the compiler should inline most of
the GETs anyways). For instance fields it is relatively easy to construct a ctor that leaks
it's reference and then gets suspended before it assigns the final field. However, such pathologic ctors
should be rare enough to warrant a skip_finals=true default
Modified Paths:
--------------
trunk/default.properties
trunk/extensions/ui/examples/RobotManager-nothread.es
trunk/extensions/ui/examples/RobotManager-thread.es
trunk/extensions/ui/examples/RobotManager.java
trunk/src/gov/nasa/jpf/jvm/bytecode/FieldInstruction.java
trunk/src/gov/nasa/jpf/jvm/bytecode/InstanceFieldInstruction.java
trunk/src/gov/nasa/jpf/jvm/bytecode/StaticFieldInstruction.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2009-01-24 03:20:55
|
Revision: 1139
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1139&view=rev
Author: pcmehlitz
Date: 2009-01-24 03:20:51 +0000 (Sat, 24 Jan 2009)
Log Message:
-----------
* changed the way State.isActive() is set/reset, which is now done from setNextState(), AND ALSO IS HIERARCHICAL (i.e. we can now easily determine if a parent state is active)
BUT: it only tells you if the state is still active in this step, or we already know it's going to be active in the next step. It doesn't separate the two cases
* added a StateMachine.isInActiveStates(s), to answer at least if the provided state is still going to be processed in this step.
* reworked the state entry processing, to hierarchically update 'isActive' and execute entry actions accordingly
!! this isn't a real solution yet - UML just deals very badly with concurrency, and the 'active state' concept isn't very suitable to model it.
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/NativeStateMachine.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...> - 2009-01-30 02:04:08
|
Revision: 1153
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1153&view=rev
Author: pcmehlitz
Date: 2009-01-30 02:04:03 +0000 (Fri, 30 Jan 2009)
Log Message:
-----------
* set thread name for EventDispatchThread to the official "AWT-EventQueue-0"
* rename RobotManagerView field that stores the selected target to "selectedRobotName", to make the need for a subsequent getOnlineRobot(..) call more obvious
* added a JVM.getMainClassInfo()
* modified the ExecTracker "et.skip_init" property handling to only skip static init, but start to log as soon as we enter main() - this is far better than skipping the whole first transition
Modified Paths:
--------------
trunk/extensions/ui/env/jpf/java/awt/EventDispatchThread.java
trunk/extensions/ui/examples/RobotManager-thread1.jpf
trunk/extensions/ui/examples/RobotManager-thread4.jpf
trunk/extensions/ui/examples/RobotManager.java
trunk/src/gov/nasa/jpf/jvm/JVM.java
trunk/src/gov/nasa/jpf/tools/ExecTracker.java
Added Paths:
-----------
trunk/extensions/ui/examples/RobotManager-nothread-console.jpf
trunk/extensions/ui/examples/RobotManager-thread-console.jpf
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