Menu
▾
▴
javapathfinder-svn — source repository related messages (SVN)
You can subscribe to this list here.
| 2008 |
Jan
|
Feb
|
Mar
|
Apr
|
May
(16) |
Jun
(42) |
Jul
(46) |
Aug
(48) |
Sep
(33) |
Oct
(26) |
Nov
(28) |
Dec
(38) |
|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 2009 |
Jan
(35) |
Feb
(80) |
Mar
(112) |
Apr
(108) |
May
(102) |
Jun
(126) |
Jul
(89) |
Aug
(82) |
Sep
(36) |
Oct
(7) |
Nov
(1) |
Dec
(4) |
| 2010 |
Jan
(87) |
Feb
|
Mar
(2) |
Apr
(1) |
May
|
Jun
|
Jul
|
Aug
|
Sep
|
Oct
|
Nov
|
Dec
|
|
From: <ar...@us...> - 2008-10-15 23:41:54
|
Revision: 1041
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1041&view=rev
Author: artimid
Date: 2008-10-15 23:41:45 +0000 (Wed, 15 Oct 2008)
Log Message:
-----------
updated CVState field name and reaction to stateBacktracked to get value of that field
Modified Paths:
--------------
trunk/extensions/cv/src/gov/nasa/jpf/cv/SCSafetyListener.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <ar...@us...> - 2008-10-15 23:41:17
|
Revision: 1040
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1040&view=rev
Author: artimid
Date: 2008-10-15 23:41:09 +0000 (Wed, 15 Oct 2008)
Log Message:
-----------
updated field name in CVState and reaction to stateBacktracked to just get value of that field
Modified Paths:
--------------
trunk/extensions/cv/src/gov/nasa/jpf/cv/SCConformanceListener.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <ar...@us...> - 2008-10-15 23:40:22
|
Revision: 1039
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1039&view=rev
Author: artimid
Date: 2008-10-15 23:40:17 +0000 (Wed, 15 Oct 2008)
Log Message:
-----------
Modified Paths:
--------------
trunk/extensions/cv/src/gov/nasa/jpf/cv/SCCommandSafetyListener.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <ar...@us...> - 2008-10-15 23:39:30
|
Revision: 1038
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1038&view=rev
Author: artimid
Date: 2008-10-15 23:38:56 +0000 (Wed, 15 Oct 2008)
Log Message:
-----------
changed field name to cover all cases
Modified Paths:
--------------
trunk/extensions/cv/env/jpf/gov/nasa/jpf/cv/CVState.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-10-15 18:22:18
|
Revision: 1036
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1036&view=rev
Author: pcmehlitz
Date: 2008-10-15 17:53:12 +0000 (Wed, 15 Oct 2008)
Log Message:
-----------
* added a typed Config.getClass(key,type)
* slightly cleaned up PathOutputMonitor error reporting and added factory method for PathOutputSpecs (so that
it could also accommodate real parsers via +pom.output_spec.class)
Modified Paths:
--------------
trunk/src/gov/nasa/jpf/Config.java
trunk/src/gov/nasa/jpf/tools/PathOutputMonitor.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-10-15 18:16:43
|
Revision: 1037
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1037&view=rev
Author: pcmehlitz
Date: 2008-10-15 18:16:33 +0000 (Wed, 15 Oct 2008)
Log Message:
-----------
* finally changed the default DeadlockAnalyzer format to "essential". Not that anybody would
ever use anything different
* changed the JPF main() so that it can take a *.jpf mode property file as the last argument
(kind of redundant to "-c <property file>", but then again that can be used to have shared
mode property files w/o a "target" spec)
Modified Paths:
--------------
trunk/src/gov/nasa/jpf/JPF.java
trunk/src/gov/nasa/jpf/tools/DeadlockAnalyzer.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <Ta...@us...> - 2008-10-15 05:56:08
|
Revision: 1035
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1035&view=rev
Author: Taehoon
Date: 2008-10-15 05:55:57 +0000 (Wed, 15 Oct 2008)
Log Message:
-----------
Initial codes for XPDL model checking.
A detailed description and examples would be committed within a week.
Added Paths:
-----------
trunk/extensions/XPDL/
trunk/extensions/XPDL/src/
trunk/extensions/XPDL/src/edu/
trunk/extensions/XPDL/src/edu/kgu/
trunk/extensions/XPDL/src/edu/kgu/xpdl/
trunk/extensions/XPDL/src/edu/kgu/xpdl/XPDL_AND_Fire.java
trunk/extensions/XPDL/src/edu/kgu/xpdl/XPDL_AND_join.java
trunk/extensions/XPDL/src/edu/kgu/xpdl/XPDL_AND_split.java
trunk/extensions/XPDL/src/edu/kgu/xpdl/XPDL_Env.java
trunk/extensions/XPDL/src/edu/kgu/xpdl/XPDL_Node.java
trunk/extensions/XPDL/src/edu/kgu/xpdl/XPDL_Resource.java
trunk/extensions/XPDL/src/edu/kgu/xpdl/XPDL_Transition.java
trunk/extensions/XPDL/src/edu/kgu/xpdl/XPDL_XOR_Join.java
trunk/extensions/XPDL/src/edu/kgu/xpdl/XPDL_Xor_split.java
trunk/extensions/XPDL/src/edu/kgu/xpdl/XPDL_activity.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: <pc...@us...> - 2008-10-14 18:58:26
|
Revision: 1033
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1033&view=rev
Author: pcorina
Date: 2008-10-14 18:44:32 +0000 (Tue, 14 Oct 2008)
Log Message:
-----------
added place-holder for concolic extension and fuzzer
Added Paths:
-----------
trunk/extensions/concolic/
trunk/extensions/concolic/build.xml
trunk/extensions/concolic/doc/
trunk/extensions/concolic/examples/
trunk/extensions/concolic/lib/
trunk/extensions/concolic/src/
trunk/extensions/concolic/test/
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <ar...@us...> - 2008-10-08 22:46:40
|
Revision: 1032
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1032&view=rev
Author: artimid
Date: 2008-10-08 22:46:22 +0000 (Wed, 08 Oct 2008)
Log Message:
-----------
changes a comment to reflect the real use of scCheckOracle2
Modified Paths:
--------------
trunk/extensions/cv/src/gov/nasa/jpf/cv/SCModularTeacher.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 23:07:29
|
Revision: 1031
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1031&view=rev
Author: pcmehlitz
Date: 2008-10-03 23:07:17 +0000 (Fri, 03 Oct 2008)
Log Message:
-----------
* some MethodTester fixes for default package test classes
Modified Paths:
--------------
trunk/src/gov/nasa/jpf/test/TestContext.java
trunk/src/gov/nasa/jpf/tools/MethodTester.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-02 04:21:19
|
Revision: 1029
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1029&view=rev
Author: pcmehlitz
Date: 2008-10-02 04:21:03 +0000 (Thu, 02 Oct 2008)
Log Message:
-----------
* annotation proxies did not have source file names, and SourceRef didn't check for a null name, resulting
in NPEs during trace print - thanks to Michal Kebrt
Modified Paths:
--------------
trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
trunk/src/gov/nasa/jpf/util/SourceRef.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-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: <st...@us...> - 2008-09-26 17:59:15
|
Revision: 1026
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1026&view=rev
Author: staats
Date: 2008-09-26 17:59:06 +0000 (Fri, 26 Sep 2008)
Log Message:
-----------
Modified Paths:
--------------
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/Debug.java
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/JPF_gov_nasa_jpf_complexcoverage_Debug.java
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/TestCase.java
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
Added Paths:
-----------
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/choice/TaggedDoubleChoiceFromSet.java
trunk/extensions/complexcoverage/test/ComplexCoverage DoubleTest Normal.launch
trunk/extensions/complexcoverage/test/gov/nasa/jpf/complexcoverage/test/DoubleTest.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-09-26 05:19:20
|
Revision: 1025
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1025&view=rev
Author: pcmehlitz
Date: 2008-09-26 05:19:08 +0000 (Fri, 26 Sep 2008)
Log Message:
-----------
some ad hoc HeuristicSearch fixes
* Interleaving was totally broken, using 'HeuristicState.otherData' to store int[] arrays representing
the scheduling history. It then NPEd when setting this in the next h_state before that even got created.
The catch is that the vm path represents the scheduling history, so all this 'otherData' and 'new_h_state'
stuff isn't needed. Removed it. However, I don't think the algorithm maximizes interleavings
* the DFSHeuristic was broken (doing nothing because of h_value < 0) in case there was no depth limit.
Again, I wonder what this heuristic is really good at
TreeSet seems to be quite inefficient for the operation profile we have. Will briefly investigate if
this warrants our own ordered set class (ConcurrentSkipListSet is a total failure, though)
Modified Paths:
--------------
trunk/src/gov/nasa/jpf/search/heuristic/DFSHeuristic.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
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <sj...@us...> - 2008-09-25 16:08:10
|
Revision: 1024
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1024&view=rev
Author: sjp100
Date: 2008-09-25 16:07:57 +0000 (Thu, 25 Sep 2008)
Log Message:
-----------
added check to see if a config value was set before trying to use it
Modified Paths:
--------------
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/HeapSymbolicListener.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <st...@us...> - 2008-09-25 00:49:23
|
Revision: 1023
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1023&view=rev
Author: staats
Date: 2008-09-25 00:49:13 +0000 (Thu, 25 Sep 2008)
Log Message:
-----------
Updated README for complex coverage
Modified Paths:
--------------
trunk/extensions/complexcoverage/doc/README.txt
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
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2008-09-25 00:00:33
|
Revision: 1022
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1022&view=rev
Author: pcmehlitz
Date: 2008-09-25 00:00:28 +0000 (Thu, 25 Sep 2008)
Log Message:
-----------
* unsupported argument types of SCEvents were just silently mapped to null, causing NPEs downstream.
Now this throws an IllegalArgumentException for anything that's not a string, a number, or a boolean
(which is of course wrapped into a InvocationTargetException in StateMachine).
String literals can also use single quotes (like 'blah') to make the annotations more readable
I really have to get out of the UML business
Modified Paths:
--------------
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: <st...@us...> - 2008-09-24 23:20:40
|
Revision: 1021
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1021&view=rev
Author: staats
Date: 2008-09-24 23:20:35 +0000 (Wed, 24 Sep 2008)
Log Message:
-----------
Added Paths:
-----------
trunk/extensions/complexcoverage/doc/README.txt
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-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-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-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.
|
