Menu
▾
▴
javapathfinder-svn
|
From: <pcm...@us...> - 2009-02-04 22:19:15
|
Revision: 1162
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1162&view=rev
Author: pcmehlitz
Date: 2009-02-04 21:39:37 +0000 (Wed, 04 Feb 2009)
Log Message:
-----------
* Eclipse screwed up the previous commit and added some temporary files. Removed those
Removed Paths:
-------------
trunk/test/gov/nasa/jpf/test/TestHeuristic.launch
trunk/trace
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2009-02-04 22:19:30
|
Revision: 1161
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1161&view=rev
Author: pcmehlitz
Date: 2009-02-04 21:36:47 +0000 (Wed, 04 Feb 2009)
Log Message:
-----------
* SimStateMachine didn't set the StateMachine.arguments (which start with the masterstate name)
* replaced the SimStateMachine '-i' option with a property 'sc.sim_mode' which defaults to 'interactive'
* improved the input parsing a bit (it now also recognized "." and "x" input for quitting)
Modified Paths:
--------------
trunk/extensions/statechart/env/jpf/gov/nasa/jpf/sc/StateMachine.java
trunk/extensions/statechart/src/gov/nasa/jpf/tools/sc/SimStateMachine.java
Added Paths:
-----------
trunk/test/gov/nasa/jpf/test/TestHeuristic.launch
trunk/trace
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2009-02-05 04:20:08
|
Revision: 1164
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1164&view=rev
Author: pcmehlitz
Date: 2009-02-05 04:20:05 +0000 (Thu, 05 Feb 2009)
Log Message:
-----------
* fixed stupid bug in NativeSentSCEvent.setProcessed() that was causing the PendingEventQueue mess up (updating JPF object structures from the native side sucks)
* left the NativeStateMachine SCEvent recycling in the bottom half of getEnablingEvent(). We could move it back to setEnablingEventProcessed() (which is still used for logging/debugging), but that might waste a heap object (and hence program states) in case we re-send the currently processing event. For model checking, it's best if we put the currently processing event back into the EventSpec pool as soon as we are done with state matching. Added lots of related comments
* changed ExecTrackers 'et.skip_init' default to true. Who wants to debug static class init of system classes anyways
Modified Paths:
--------------
trunk/extensions/statechart/env/jpf/gov/nasa/jpf/sc/StateMachine.java
trunk/extensions/statechart/env/jvm/gov/nasa/jpf/jvm/NativeStateMachine.java
trunk/extensions/statechart/src/gov/nasa/jpf/jvm/choice/sc/NativeSentSCEvent.java
trunk/src/gov/nasa/jpf/tools/ExecTracker.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2009-02-12 04:04:30
|
Revision: 1169
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1169&view=rev
Author: pcmehlitz
Date: 2009-02-12 04:04:24 +0000 (Thu, 12 Feb 2009)
Log Message:
-----------
* rework of the FieldLockInfo mechanism - this came up because of some examples where JPF didn't find races in very simple programs. It turned out that the simplicity was the problem: if JPF comes up with a 'protected' StatisticFieldLockInfo assumption, but the related object gets recycled along this path before we ever hit a path that violates the assumption, we don't notice. Ideally, StatisticFieldLockInfos should be search-global, but since neither ElementInfo nor their reference values are guaranteed to be invariant, we hardly can enforce this over a GC.
* there now is a 'pindown' option to avoid GCing objects that have 'protected' StatisticFieldLockInfo assumptions, so that we can at least get subsequent warnings
* we now have a factory for FieldLockInfo instantiation
* consequently, the whole StatisticFieldLockInfo stuff is now in StatisticFieldLockInfoFactory
* since we have a real factory now, we can instantiate after the first lock protection, saving both checks *and* FieldLockInfo instances
* field attributes (previously used for filtering) have been moved over to the (almost abandoned) DefaultAttributor, since it's much more effective to check at class load time
* the filtering has changed: we can specify field names that are never supposed to be scheduling relevant (library classes), and we can specify field names that should always break transitions if the object is shared (even if vm.por.sync_detection is on and there are locks)
* slight change in Area.remove() - we first ask the object via ElementInfo.recycle() if it is willing to leave this world. This is an implicit pindown, so be careful. There is a symmetric ElementInfo.resurrect() which can be used to restore volatile info that is not part of the state storage
The refactored system is more sound, but can still miss races if not configured properly. The configuration is now more conservative and orthogonal, but still confusing:
+vm.por.fli_factory.class - the factory class name for FieldLockInfo creation
+vm.por.field_boundaries.never - never break on these field name patterns (e.g. java.*)
+vm.por.field_boundaries.break - always break on these patterns if the object is shared (e.g. for app class fields that caused assumption warnings)
+vm.por.sync_detection.pindown - don't GC an object that has a 'protected' StatisticFieldLockInfo assumption
+vm.por.sync_detection.agressive - look for supposed to be related locks (field owner, sibling field etc.) - THIS IS PRONE TO MISSING RACES IN SIMPLE EXAMPLES (hence it's now turned off by default)
The problem with this is that some of the options only make sense in a vm.por.field_boundaries & vm.por.sync_detection context
Modified Paths:
--------------
trunk/default.properties
trunk/src/gov/nasa/jpf/jvm/Area.java
trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
trunk/src/gov/nasa/jpf/jvm/CollapsingRestorer.java
trunk/src/gov/nasa/jpf/jvm/ConfigAttributor.java
trunk/src/gov/nasa/jpf/jvm/DefaultAttributor.java
trunk/src/gov/nasa/jpf/jvm/ElementInfo.java
trunk/src/gov/nasa/jpf/jvm/FieldInfo.java
trunk/src/gov/nasa/jpf/jvm/FieldLockInfo.java
trunk/src/gov/nasa/jpf/jvm/KernelState.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
trunk/test/gov/nasa/jpf/mc/TestRace.java
Added Paths:
-----------
trunk/src/gov/nasa/jpf/jvm/FieldLockInfoFactory.java
trunk/src/gov/nasa/jpf/jvm/StatisticFieldLockInfoFactory.java
Removed Paths:
-------------
trunk/src/gov/nasa/jpf/jvm/SingleFieldLockInfo.java
trunk/src/gov/nasa/jpf/jvm/StatisticFieldLockInfo.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2009-02-12 04:18:40
|
Revision: 1172
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1172&view=rev
Author: pcmehlitz
Date: 2009-02-12 04:18:37 +0000 (Thu, 12 Feb 2009)
Log Message:
-----------
a bunch of patches from Nathan Reynolds - thanks Nathan!
* added missing features to AtomicReferenceFieldUpdater + regression tests
* added missing AtomicInteger/LongFieldUpdater + regression tests
* better CoverageAnalyzer output formatting (Eclipse source links)
Modified Paths:
--------------
trunk/env/jpf/java/util/concurrent/atomic/AtomicReferenceFieldUpdater.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_util_concurrent_atomic_AtomicReferenceFieldUpdater.java
trunk/src/gov/nasa/jpf/tools/CoverageAnalyzer.java
trunk/test/gov/nasa/jpf/jvm/TestAtomicReferenceFieldUpdater.java
Added Paths:
-----------
trunk/env/jpf/java/util/concurrent/atomic/AtomicIntegerFieldUpdater.java
trunk/env/jpf/java/util/concurrent/atomic/AtomicLongFieldUpdater.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_util_concurrent_atomic_AtomicIntegerFieldUpdater.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_util_concurrent_atomic_AtomicLongFieldUpdater.java
trunk/test/gov/nasa/jpf/jvm/TestAtomicIntegerFieldUpdater.java
trunk/test/gov/nasa/jpf/jvm/TestAtomicIntegerFieldUpdaterJPF.java
trunk/test/gov/nasa/jpf/jvm/TestAtomicLongFieldUpdater.java
trunk/test/gov/nasa/jpf/jvm/TestAtomicLongFieldUpdaterJPF.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2009-03-06 23:29:34
|
Revision: 1258
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1258&view=rev
Author: pcmehlitz
Date: 2009-03-06 23:29:20 +0000 (Fri, 06 Mar 2009)
Log Message:
-----------
* reverted the Source fix that checked for non-existing default vm.sourcedirs, and turned the log warning into an info. Come to think of it, there is no difference between non-existing hardwired and configured dirs, and it would be very misleading to depend on warnings that only cover the first case
* added a build-tools/bin/build-svn-snapshot bash script, o that we finally can have Sourceforge file snapshots on a more regular basis
* changed bin/jpf so that *.class files always have precedence over lib/*.jars (which are used in the binary release)
Modified Paths:
--------------
trunk/bin/jpf
trunk/src/gov/nasa/jpf/util/Source.java
Added Paths:
-----------
trunk/build-tools/bin/build-svn-snapshot
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2009-03-09 16:07:22
|
Revision: 1263
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1263&view=rev
Author: pcmehlitz
Date: 2009-03-09 16:07:20 +0000 (Mon, 09 Mar 2009)
Log Message:
-----------
* missing AtomicInteger peer caused ULE - thanks John Kerich
* Search.forward() was calling JVM.isNewState() instead of Search.isNewState(), thus ignoring 'search.match_depth' - thanks Guowei Yang
Modified Paths:
--------------
trunk/src/gov/nasa/jpf/search/Search.java
Added Paths:
-----------
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_util_concurrent_atomic_AtomicInteger.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2009-03-11 04:13:19
|
Revision: 1268
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1268&view=rev
Author: pcmehlitz
Date: 2009-03-11 04:12:50 +0000 (Wed, 11 Mar 2009)
Log Message:
-----------
* added a bit more support for java.text.DateFormat, plus basic test. While the idea was to use native peers to cut off the whole calendar and parse/format processing, this doesn't really work right now - there are too many insns executed, and if somebody seriously uses the xxFormat APIs, there's a bad chance of hitting missing natives and/or only partially initialized JPF (proxy) objects. Needs more work
* added an MJIEnv.getDateObject() converter
Modified Paths:
--------------
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_text_DateFormat.java
trunk/src/gov/nasa/jpf/jvm/MJIEnv.java
Added Paths:
-----------
trunk/test/gov/nasa/jpf/jvm/TestJavaTextDateFormat.java
trunk/test/gov/nasa/jpf/jvm/TestJavaTextDateFormatJPF.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2009-03-21 01:23:29
|
Revision: 1304
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1304&view=rev
Author: pcmehlitz
Date: 2009-03-21 01:23:23 +0000 (Sat, 21 Mar 2009)
Log Message:
-----------
patches from Nathan Reynolds:
* more AtomicXXUpdater field access CGs, but this needs to be unified with the ThreadInfo.usePorFieldBoundaries() and get/putfield (shared object, runnable threads etc)
* added StackTracker, which probes application call stacks at given time intervals, to find out what the application is doing
* added do..while() support for the IdleFilters
*upped the default OOME safety margin to 64k
Modified Paths:
--------------
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_util_concurrent_atomic_AtomicIntegerFieldUpdater.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_util_concurrent_atomic_AtomicLongFieldUpdater.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_util_concurrent_atomic_AtomicReferenceFieldUpdater.java
trunk/src/gov/nasa/jpf/JPF.java
trunk/src/gov/nasa/jpf/jvm/bytecode/IfInstruction.java
Added Paths:
-----------
trunk/examples/Hang.java
trunk/src/gov/nasa/jpf/tools/StackTracker.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2009-03-25 22:47:01
|
Revision: 1321
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1321&view=rev
Author: pcmehlitz
Date: 2009-03-25 22:46:50 +0000 (Wed, 25 Mar 2009)
Log Message:
-----------
* little cleanup of AtomicFieldUpdater peers, based on the (uneducated) assumption that we want to interleave with "non-protected" gets/puts
- should probably check and create a CG for the field owner, not the updater
- replaced the 'enumerateCAS' misnomer with the existing porFieldBoundaries settings
- refactored common code in AtomicFieldUpdater (but beware - only statics allowed)
in order to make this useful, we still have to update the RaceDetectors
Modified Paths:
--------------
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_util_concurrent_atomic_AtomicIntegerFieldUpdater.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_util_concurrent_atomic_AtomicLongFieldUpdater.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_util_concurrent_atomic_AtomicReferenceFieldUpdater.java
trunk/src/gov/nasa/jpf/jvm/MJIEnv.java
trunk/src/gov/nasa/jpf/jvm/bytecode/InstanceFieldInstruction.java
trunk/src/gov/nasa/jpf/tools/PreciseRaceDetector.java
Added Paths:
-----------
trunk/env/jvm/gov/nasa/jpf/jvm/AtomicFieldUpdater.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2009-03-27 05:08:32
|
Revision: 1332
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1332&view=rev
Author: pcmehlitz
Date: 2009-03-27 05:08:30 +0000 (Fri, 27 Mar 2009)
Log Message:
-----------
batch of patches from Nathan Reynolds - thanks
* HTMLPublisher - this creates a bunch of scripted web pages with various result topics, suitable for browsing (but not storing). It still needs some cleanup to remove PublisherExtension dependencies (a Publisher should NOT have to be aware of specific extensions), and it doesn't (yet) follow the publisher configuration scheme, but it's a pretty sophisticated web interface.
* the only PublisherExtension that currently supports it is the CoverageAnalyzer, which got refactored so that publisher specific methods are kept together (also needs some cleanup once HtmlPublisher is more conformant)
* the VarRecorder is a little utility listener that adds trace comments for variable access ops
* store state id and ThreadInfo in Transition
* some little optimizations in SimpleIdleFilter and Source
Modified Paths:
--------------
trunk/default.properties
trunk/src/gov/nasa/jpf/jvm/ClassInfo.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/Transition.java
trunk/src/gov/nasa/jpf/tools/CoverageAnalyzer.java
trunk/src/gov/nasa/jpf/tools/SimpleIdleFilter.java
trunk/src/gov/nasa/jpf/util/Source.java
Added Paths:
-----------
trunk/src/gov/nasa/jpf/report/HTMLPublisher.java
trunk/src/gov/nasa/jpf/tools/VarRecorder.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2009-03-28 02:02:10
|
Revision: 1346
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1346&view=rev
Author: pcmehlitz
Date: 2009-03-28 02:02:00 +0000 (Sat, 28 Mar 2009)
Log Message:
-----------
* added some NetBeans UI actions so that we can run JPF on *.jpf|*.properties files (you have to use shift-F6 since NB doesn't display the "Run" context menu item for non *.java), run normal Java apps in examples and test, and Test*JPF apps (with JUnit) in test - that should cover almost all bases. If you want property file editor support, name your JPF config "*.jpf.properties"
* changed JPF accordingly, so that it also accepts a single *.properties as argument. Also changed the config /usage print to happen before we call a shell (useful for debugging)
* fixed bug in build.xml when compiling extension examples (wasn't looking for build/app)
* bad hack in UIInspector while checking jpf.shell.class usage. Inspector execpts "inspect.*" properties, but the ui framework uses "awt.*" => turn this into Inspector ctor arguments (we want to keep everything "awt" in ui)
Modified Paths:
--------------
trunk/build.xml
trunk/extensions/ui/env/jvm/gov/nasa/jpf/jvm/JPF_java_awt_EventDispatchThread.java
trunk/extensions/ui/examples/RobotManager-nothread.jpf
trunk/extensions/ui/src/gov/nasa/jpf/tools/UIInspector.java
trunk/nbproject/ide-file-targets.xml
trunk/nbproject/project.xml
trunk/src/gov/nasa/jpf/JPF.java
Added Paths:
-----------
trunk/examples/oldclassic.jpf.properties
Removed Paths:
-------------
trunk/examples/oldclassic.properties
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <jt...@us...> - 2009-03-17 18:10:48
|
Revision: 1285
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1285&view=rev
Author: jtzwu
Date: 2009-03-17 18:10:33 +0000 (Tue, 17 Mar 2009)
Log Message:
-----------
Add JPF config options documentation tool
Modified Paths:
--------------
trunk/.classpath
trunk/build.xml
trunk/env/jpf/java/util/regex/Matcher.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_util_regex_Matcher.java
Added Paths:
-----------
trunk/build-tools/optionsdoc/
trunk/build-tools/optionsdoc/build/
trunk/build-tools/optionsdoc/src/
trunk/build-tools/optionsdoc/src/gov/
trunk/build-tools/optionsdoc/src/gov/nasa/
trunk/build-tools/optionsdoc/src/gov/nasa/jpf/
trunk/build-tools/optionsdoc/src/gov/nasa/jpf/doc/
trunk/build-tools/optionsdoc/src/gov/nasa/jpf/doc/BytecodeOptionsScanner.java
trunk/build-tools/optionsdoc/src/gov/nasa/jpf/doc/CodeScanner.java
trunk/build-tools/optionsdoc/src/gov/nasa/jpf/doc/CodeScannerFactory.java
trunk/build-tools/optionsdoc/src/gov/nasa/jpf/doc/ConfigDoc.java
trunk/build-tools/optionsdoc/src/gov/nasa/jpf/doc/ConfigDoclet.java
trunk/build-tools/optionsdoc/src/gov/nasa/jpf/doc/ConfigIOException.java
trunk/build-tools/optionsdoc/src/gov/nasa/jpf/doc/ConfigIOImpl.java
trunk/build-tools/optionsdoc/src/gov/nasa/jpf/doc/DocAppFactory.java
trunk/build-tools/optionsdoc/src/gov/nasa/jpf/doc/DocletArguments.java
trunk/build-tools/optionsdoc/src/gov/nasa/jpf/doc/MethodScanner.java
trunk/build-tools/optionsdoc/src/gov/nasa/jpf/doc/MethodScannerFactory.java
trunk/build-tools/optionsdoc/src/gov/nasa/jpf/doc/Options.java
trunk/build-tools/optionsdoc/src/gov/nasa/jpf/doc/OptionsFactory.java
trunk/build-tools/optionsdoc/src/gov/nasa/jpf/doc/OptionsFactoryImpl.java
trunk/build-tools/optionsdoc/src/gov/nasa/jpf/doc/OptionsFileReader.java
trunk/build-tools/optionsdoc/src/gov/nasa/jpf/doc/OptionsFileWriter.java
trunk/build-tools/optionsdoc/src/gov/nasa/jpf/doc/OptionsHandler.java
trunk/build-tools/optionsdoc/src/gov/nasa/jpf/doc/OptionsHandlerImpl.java
trunk/build-tools/optionsdoc/src/gov/nasa/jpf/doc/OptionsIO.java
trunk/build-tools/optionsdoc/src/gov/nasa/jpf/doc/OptionsReader.java
trunk/build-tools/optionsdoc/src/gov/nasa/jpf/doc/OptionsScanner.java
trunk/build-tools/optionsdoc/src/gov/nasa/jpf/doc/OptionsWriter.java
trunk/build-tools/optionsdoc/src/gov/nasa/jpf/doc/TagReader.java
trunk/build-tools/optionsdoc/src/gov/nasa/jpf/doc/stacksim/
trunk/build-tools/optionsdoc/src/gov/nasa/jpf/doc/stacksim/KnownValue.java
trunk/build-tools/optionsdoc/src/gov/nasa/jpf/doc/stacksim/StackSimulator.java
trunk/build-tools/optionsdoc/src/gov/nasa/jpf/doc/stacksim/StackValue.java
trunk/build-tools/optionsdoc/src/gov/nasa/jpf/doc/stacksim/UnknownValue.java
trunk/test/gov/nasa/jpf/test/TestRegex.java
trunk/test/gov/nasa/jpf/test/TestUtilsJPF.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2009-04-01 18:35:41
|
Revision: 1360
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1360&view=rev
Author: pcmehlitz
Date: 2009-04-01 18:35:38 +0000 (Wed, 01 Apr 2009)
Log Message:
-----------
* running a selected Test..JPF in NetBeans has to depend on the "compile-tests" ant target
* added some more java.io.File peer methods + tests (thanks Taehoon)
Somebody should really make this more efficient, and look into a backtrackable filesystem model
Modified Paths:
--------------
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_io_File.java
trunk/nbproject/ide-file-targets.xml
trunk/test/gov/nasa/jpf/jvm/TestFileIO.java
trunk/test/gov/nasa/jpf/jvm/TestFileIOJPF.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2009-04-15 01:01:11
|
Revision: 1403
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1403&view=rev
Author: pcmehlitz
Date: 2009-04-15 01:01:08 +0000 (Wed, 15 Apr 2009)
Log Message:
-----------
* added a synthetic "config" and "config_path" entry to Config, which is set from the mode property file (if there is any). With that, you can finally specify scripts relative to where the *.jpf is stored, like
inspect.script = ${config_path}/myscript.es
* fixed a little bug in Config.getTargetArgParameters
* removed the awt.* -> inspect.* hack in the UIInspector. Still need to change a bunch of launch configs accordingly, but they now can be replaced with *.jpf's anyways
* moved all the non-test extensions/ui launch configs to *.jpf's
Modified Paths:
--------------
trunk/extensions/ui/examples/RobotManager test.launch
trunk/extensions/ui/examples/RobotManager-nothread.jpf
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/extensions/ui/src/gov/nasa/jpf/tools/UIInspector.java
trunk/src/gov/nasa/jpf/Config.java
trunk/src/gov/nasa/jpf/util/Inspector.java
Removed Paths:
-------------
trunk/extensions/ui/examples/RobotManager nothread.launch
trunk/extensions/ui/examples/RobotManager thread.launch
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.
|
|
From: <pcm...@us...> - 2009-04-16 03:08:50
|
Revision: 1406
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1406&view=rev
Author: pcmehlitz
Date: 2009-04-16 03:08:39 +0000 (Thu, 16 Apr 2009)
Log Message:
-----------
* fixed Config ctor for property file w/o path
* patch from Nathan moving to "*.html" HTMLPublisher file extensions and adding StateCountEstimator listener
* small refactoring to make TestJPF more robust. Should probably be reworked for better error messages
Modified Paths:
--------------
trunk/src/gov/nasa/jpf/Config.java
trunk/src/gov/nasa/jpf/jvm/JVM.java
trunk/src/gov/nasa/jpf/report/HTMLPublisher.java
trunk/test/gov/nasa/jpf/jvm/TestJPF.java
Added Paths:
-----------
trunk/src/gov/nasa/jpf/tools/StateCountEstimator.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <jt...@us...> - 2009-04-17 23:28:41
|
Revision: 1417
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1417&view=rev
Author: jtzwu
Date: 2009-04-17 23:28:26 +0000 (Fri, 17 Apr 2009)
Log Message:
-----------
Fix bug 1882764. The StateSpaceDot listener was tracking the previous
state of the machine and placing it in the graph when the graph search
ended. If there is only one state, the previous state is null. When
StateSpaceDot attempts to place the previous state into the graph, a
null pointer exception is hit. I placed a guard in front of the add
function to check that the previous state is not null.
Modified Paths:
--------------
trunk/extensions/symbc/test/gov/nasa/jpf/symbc/TestExJPF.java
trunk/src/gov/nasa/jpf/tools/StateSpaceDot.java
Added Paths:
-----------
trunk/test/gov/nasa/jpf/tools/
trunk/test/gov/nasa/jpf/tools/TestStateSpaceDotJPF.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pc...@us...> - 2009-04-22 01:11:14
|
Revision: 1433
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1433&view=rev
Author: pcorina
Date: 2009-04-22 01:11:08 +0000 (Wed, 22 Apr 2009)
Log Message:
-----------
fixed conflicts, classpath and weird characters in copyright notice
Modified Paths:
--------------
trunk/.classpath
trunk/examples/Termination.java
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/JPF_gov_nasa_jpf_complexcoverage_Debug.java
trunk/extensions/complexcoverage/test/gov/nasa/jpf/complexcoverage/test/TestFile.java
trunk/extensions/symbc/examples/StringTest.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/SymbolicStringHandler.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/mixednumstrg/SpecialIntegerExpression.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/mixednumstrg/SpecialRealExpression.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/PathCondition.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/string/StringConstant.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/string/StringConstraint.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/string/StringOperator.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/string/StringPathCondition.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/string/StringSymbolic.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/string/SymbolicStringBuilder.java
trunk/extensions/symbc/test/gov/nasa/jpf/symbc/ExSymExe1.java
trunk/extensions/symbc/test/gov/nasa/jpf/symbc/ExSymExeMathIAsolver.java
trunk/extensions/symbc/test/gov/nasa/jpf/symbc/TestSymbolic.java
trunk/src/gov/nasa/jpf/jvm/bytecode/InvokeInstruction.java
Added Paths:
-----------
trunk/TestFileSimpleCoverage.java-trace
trunk/double-test.txt
trunk/extensions/complexcoverage/test/ComplexCoverage TestFun SimpleCoverage.launch
trunk/extensions/complexcoverage/test/gov/nasa/jpf/complexcoverage/test/TestFileSimpleCoverage.java
trunk/extensions/symbc/env/jvm/gov/nasa/jpf/symbc/JPF_java_lang_String.java
trunk/extensions/symbc/env/jvm/gov/nasa/jpf/symbc/JPF_java_lang_StringBuffer.java
trunk/extensions/symbc/env/jvm/gov/nasa/jpf/symbc/JPF_java_lang_StringBuilder.java
trunk/extensions/symbc/outFile.txt
trunk/extensions/symbc/src.tar.gz
trunk/extensions/symbc/test/gov/nasa/jpf/symbc/ExDarko.java
trunk/extensions/symbc/test/gov/nasa/jpf/symbc/ExMIT.java
trunk/extensions/symbc/test/gov/nasa/jpf/symbc/ExStateflow.java
trunk/extensions/symbc/test/gov/nasa/jpf/symbc/ExSymExeHeap2.java
trunk/extensions/symbc/test/gov/nasa/jpf/symbc/ExSymExeHeap3.java
trunk/extensions/symbc/test/gov/nasa/jpf/symbc/ExSymExeSimple.java
trunk/extensions/symbc/test/gov/nasa/jpf/symbc/ExSymExeStrings.java
trunk/extensions/symbc/test/gov/nasa/jpf/symbc/symtest.sh
trunk/extensions/symbc/test.tar.gz
trunk/extensions/symbc.tar.gz
trunk/javapathfinder-972.patch.txt
trunk/osm_method.dot
trunk/osm_sequence.dot
trunk/outFile.txt
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2009-04-22 19:24:22
|
Revision: 1438
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1438&view=rev
Author: pcmehlitz
Date: 2009-04-22 19:24:20 +0000 (Wed, 22 Apr 2009)
Log Message:
-----------
* removed a bunch of temp files that percolated up from extensions
* reworked synthesized code a bit - this was triggered by mango through an ill-placed RETURN.initilialize(). Excplicit insn reation had several mechanisms with a lot of pitfalls. Now it's using a MethodInfo local CodeBuilder object, which sets MethodInfo, location and offset of added insns while it builds the code array.
* the various "initialize()" methods in Insn classes that happened to be synthesized have been renamed to their concrete class purpose (e.g. InvokeInstruction.setInvokedMethod), and stripped of their location initialization (which is done by the CodeBuilder).
Modified Paths:
--------------
trunk/extensions/symts/src/gov/nasa/jpf/ts/TSVM.java
trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
trunk/src/gov/nasa/jpf/jvm/MethodInfo.java
trunk/src/gov/nasa/jpf/jvm/bytecode/ALOAD.java
trunk/src/gov/nasa/jpf/jvm/bytecode/FieldInstruction.java
trunk/src/gov/nasa/jpf/jvm/bytecode/GETFIELD.java
trunk/src/gov/nasa/jpf/jvm/bytecode/INVOKECG.java
trunk/src/gov/nasa/jpf/jvm/bytecode/Instruction.java
trunk/src/gov/nasa/jpf/jvm/bytecode/InvokeInstruction.java
trunk/src/gov/nasa/jpf/jvm/bytecode/RETURN.java
trunk/src/gov/nasa/jpf/jvm/bytecode/ReturnInstruction.java
trunk/test/gov/nasa/jpf/jvm/TestFileIO.java
Removed Paths:
-------------
trunk/TestFileSimpleCoverage.java-trace
trunk/double-test.txt
trunk/javapathfinder-972.patch.txt
trunk/osm_method.dot
trunk/osm_sequence.dot
trunk/outFile.txt
trunk/src/gov/nasa/jpf/jvm/CodeBuilder.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2009-05-01 05:57:25
|
Revision: 1474
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1474&view=rev
Author: pcmehlitz
Date: 2009-05-01 05:57:17 +0000 (Fri, 01 May 2009)
Log Message:
-----------
* opened the exception firewall in JPF.run() - if we encounter a JPFException or another RuntimeException, we pass it on. This is necessary to enable callers to find out if a JPF run was prematurely terminated
* added JPFListenerException and JPFNativePeerException, which are wrapping everything (well almost) that can go wrong during listener notification and native method execution. Both conceptually don't belong to the JPF core, and listener exceptions could even be recoverable (depending on what listener it is)
* renamed JPFTest.runJPFException() -> runJPFappException(), to indicate that we expect an exception in the application. added a runJPFException() to indicate that we expect an exception thrown by JPF (which mostly makes sense for the two JPFExceptions above)
* added a patch to throw InstantiationException and IllegalAccessException during Class.newInstance() - thanks Taehoon Lee
* added test + modified TestNativePeer/JPF accordingly
Modified Paths:
--------------
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Class.java
trunk/extensions/numeric/test/gov/nasa/jpf/numeric/TestNumericJPF.java
trunk/extensions/symbc/test/gov/nasa/jpf/symbc/TestExJPF.java
trunk/src/gov/nasa/jpf/JPF.java
trunk/src/gov/nasa/jpf/JPFException.java
trunk/src/gov/nasa/jpf/jvm/ExceptionInfo.java
trunk/src/gov/nasa/jpf/jvm/JVM.java
trunk/src/gov/nasa/jpf/jvm/MethodInfo.java
trunk/src/gov/nasa/jpf/jvm/NativePeer.java
trunk/src/gov/nasa/jpf/jvm/Transition.java
trunk/src/gov/nasa/jpf/search/Search.java
trunk/test/gov/nasa/jpf/jvm/RawTest.java
trunk/test/gov/nasa/jpf/jvm/TestCastJPF.java
trunk/test/gov/nasa/jpf/jvm/TestExceptionJPF.java
trunk/test/gov/nasa/jpf/jvm/TestJPF.java
trunk/test/gov/nasa/jpf/jvm/TestJavaLangClass.java
trunk/test/gov/nasa/jpf/jvm/TestJavaLangClassJPF.java
trunk/test/gov/nasa/jpf/jvm/TestNativePeerJPF.java
trunk/test/gov/nasa/jpf/mc/TestRaceJPF.java
trunk/test/gov/nasa/jpf/mc/TestRandomJPF.java
Added Paths:
-----------
trunk/src/gov/nasa/jpf/JPFListenerException.java
trunk/src/gov/nasa/jpf/JPFNativePeerException.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2009-05-11 04:52:35
|
Revision: 1498
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1498&view=rev
Author: pcmehlitz
Date: 2009-05-11 04:52:25 +0000 (Mon, 11 May 2009)
Log Message:
-----------
* added Milos Gligoric's & Tihomir Gvero's delayed CG extension - the general idea is to delay choice generation until the point where the choice value is used. See delayed/doc and the referenced paper
http://infoscience.epfl.ch/record/128816
Modified Paths:
--------------
trunk/.classpath
Added Paths:
-----------
trunk/extensions/delayed/
trunk/extensions/delayed/build.xml
trunk/extensions/delayed/doc/
trunk/extensions/delayed/doc/index.html
trunk/extensions/delayed/src/
trunk/extensions/delayed/src/gov/
trunk/extensions/delayed/src/gov/nasa/
trunk/extensions/delayed/src/gov/nasa/jpf/
trunk/extensions/delayed/src/gov/nasa/jpf/delayed/
trunk/extensions/delayed/src/gov/nasa/jpf/delayed/NCPInstructionFactory.java
trunk/extensions/delayed/src/gov/nasa/jpf/delayed/ObjectPool.java
trunk/extensions/delayed/src/gov/nasa/jpf/delayed/attr/
trunk/extensions/delayed/src/gov/nasa/jpf/delayed/attr/AnyObjNCPDelayedAttr.java
trunk/extensions/delayed/src/gov/nasa/jpf/delayed/attr/BooleanNCPDelayedAttr.java
trunk/extensions/delayed/src/gov/nasa/jpf/delayed/attr/IntNCPDelayedAttr.java
trunk/extensions/delayed/src/gov/nasa/jpf/delayed/attr/NCPDelayedAttr.java
trunk/extensions/delayed/src/gov/nasa/jpf/delayed/attr/NewObjNCPDelayedAttr.java
trunk/extensions/delayed/src/gov/nasa/jpf/delayed/attr/ObjNCPDelayedAttr.java
trunk/extensions/delayed/src/gov/nasa/jpf/delayed/bytecode/
trunk/extensions/delayed/src/gov/nasa/jpf/delayed/bytecode/AALOAD.java
trunk/extensions/delayed/src/gov/nasa/jpf/delayed/bytecode/ALOAD.java
trunk/extensions/delayed/src/gov/nasa/jpf/delayed/bytecode/BALOAD.java
trunk/extensions/delayed/src/gov/nasa/jpf/delayed/bytecode/CHECKCAST.java
trunk/extensions/delayed/src/gov/nasa/jpf/delayed/bytecode/GETFIELD.java
trunk/extensions/delayed/src/gov/nasa/jpf/delayed/bytecode/GETSTATIC.java
trunk/extensions/delayed/src/gov/nasa/jpf/delayed/bytecode/IALOAD.java
trunk/extensions/delayed/src/gov/nasa/jpf/delayed/bytecode/IINC.java
trunk/extensions/delayed/src/gov/nasa/jpf/delayed/bytecode/ILOAD.java
trunk/extensions/delayed/src/gov/nasa/jpf/delayed/bytecode/INVOKESPECIAL.java
trunk/extensions/delayed/src/gov/nasa/jpf/delayed/bytecode/INVOKESTATIC.java
trunk/extensions/delayed/src/gov/nasa/jpf/delayed/bytecode/INVOKEVIRTUAL.java
trunk/extensions/delayed/src/gov/nasa/jpf/delayed/bytecode/VirtualInvocation.java
trunk/extensions/delayed/src/gov/nasa/jpf/delayed/cg/
trunk/extensions/delayed/src/gov/nasa/jpf/delayed/cg/DelayedCG.java
trunk/extensions/delayed/src/gov/nasa/jpf/delayed/cg/ObjDelayedCG.java
trunk/extensions/delayed/src/gov/nasa/jpf/delayed/state/
trunk/extensions/delayed/src/gov/nasa/jpf/delayed/state/AnyOrderEntry.java
trunk/extensions/delayed/src/gov/nasa/jpf/delayed/state/NCPDelayedStateExtensionClient.java
trunk/extensions/delayed/src/gov/nasa/jpf/delayed/state/NewOrderEntry.java
trunk/extensions/delayed/src/gov/nasa/jpf/delayed/state/Order.java
trunk/extensions/delayed/src/gov/nasa/jpf/delayed/state/OrderEntry.java
trunk/extensions/delayed/src/gov/nasa/jpf/delayed/state/UnderlineObjectPool.java
trunk/extensions/delayed/src/gov/nasa/jpf/delayed/util/
trunk/extensions/delayed/src/gov/nasa/jpf/delayed/util/NCPUtils.java
trunk/extensions/delayed/src/gov/nasa/jpf/delayed/util/Pair.java
trunk/extensions/delayed/src/gov/nasa/jpf/delayed/util/Roundtrip.java
trunk/extensions/delayed/src/gov/nasa/jpf/jvm/
trunk/extensions/delayed/src/gov/nasa/jpf/jvm/NCPDelayedRestorer.java
trunk/extensions/delayed/test/
trunk/extensions/delayed/test/gov/
trunk/extensions/delayed/test/gov/nasa/
trunk/extensions/delayed/test/gov/nasa/jpf/
trunk/extensions/delayed/test/gov/nasa/jpf/delayed/
trunk/extensions/delayed/test/gov/nasa/jpf/delayed/TestAALOAD.java
trunk/extensions/delayed/test/gov/nasa/jpf/delayed/TestAALOADJPF.java
trunk/extensions/delayed/test/gov/nasa/jpf/delayed/TestALOAD.java
trunk/extensions/delayed/test/gov/nasa/jpf/delayed/TestALOADJPF.java
trunk/extensions/delayed/test/gov/nasa/jpf/delayed/TestBALOAD.java
trunk/extensions/delayed/test/gov/nasa/jpf/delayed/TestBALOADJPF.java
trunk/extensions/delayed/test/gov/nasa/jpf/delayed/TestDefaultObjectPool.java
trunk/extensions/delayed/test/gov/nasa/jpf/delayed/TestDefaultObjectPoolJPF.java
trunk/extensions/delayed/test/gov/nasa/jpf/delayed/TestGETFIELD.java
trunk/extensions/delayed/test/gov/nasa/jpf/delayed/TestGETFIELDJPF.java
trunk/extensions/delayed/test/gov/nasa/jpf/delayed/TestGETSTATIC.java
trunk/extensions/delayed/test/gov/nasa/jpf/delayed/TestGETSTATICJPF.java
trunk/extensions/delayed/test/gov/nasa/jpf/delayed/TestIALOAD.java
trunk/extensions/delayed/test/gov/nasa/jpf/delayed/TestIALOADJPF.java
trunk/extensions/delayed/test/gov/nasa/jpf/delayed/TestILOAD.java
trunk/extensions/delayed/test/gov/nasa/jpf/delayed/TestILOADJPF.java
trunk/extensions/delayed/test/gov/nasa/jpf/delayed/test/
trunk/extensions/delayed/test/gov/nasa/jpf/delayed/test/conf/
trunk/extensions/delayed/test/gov/nasa/jpf/delayed/test/conf/ConfigurableTestJPF.java
trunk/extensions/delayed/test/gov/nasa/jpf/delayed/test/conf/DefaultConfigurableTestJPF.java
trunk/extensions/delayed/test/gov/nasa/jpf/delayed/test/conf/NCPConfigurableTestJPF.java
trunk/extensions/delayed/test/gov/nasa/jpf/delayed/test/util/
trunk/extensions/delayed/test/gov/nasa/jpf/delayed/test/util/JPF_gov_nasa_jpf_delayed_test_util_TestUtils.java
trunk/extensions/delayed/test/gov/nasa/jpf/delayed/test/util/TestUtils.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2009-05-13 18:46:42
|
Revision: 1508
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1508&view=rev
Author: pcmehlitz
Date: 2009-05-13 18:46:28 +0000 (Wed, 13 May 2009)
Log Message:
-----------
* fixed bug in single choice CGs in ui and statechart, causing trace replay to fail
* added a replay test
* added a trace.verbose, which adds a commented out CG printout for each line. Just for debugging purposes of shorter traces, so it's off by default
* statechart scripting can now use pathnames relative to *.jpf
Modified Paths:
--------------
trunk/extensions/statechart/env/jpf/gov/nasa/jpf/sc/PendingEventQueue.java
trunk/extensions/statechart/env/jvm/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_sc_StateMachine.java
trunk/extensions/statechart/env/jvm/gov/nasa/jpf/jvm/NativeStateMachine.java
trunk/extensions/statechart/src/gov/nasa/jpf/jvm/choice/sc/SCEventSingleChoice.java
trunk/extensions/ui/src/gov/nasa/jpf/jvm/choice/ui/UIActionSingleChoice.java
trunk/src/gov/nasa/jpf/jvm/ChoicePoint.java
trunk/src/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_jvm_Verify.java
trunk/src/gov/nasa/jpf/jvm/JVM.java
trunk/src/gov/nasa/jpf/tools/ChoiceSelector.java
trunk/src/gov/nasa/jpf/tools/TraceStorer.java
trunk/test/gov/nasa/jpf/mc/TestPartialTrace.java
trunk/test/gov/nasa/jpf/mc/TestPartialTraceJPF.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2009-05-13 23:38:55
|
Revision: 1511
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1511&view=rev
Author: pcmehlitz
Date: 2009-05-13 23:38:49 +0000 (Wed, 13 May 2009)
Log Message:
-----------
* had to temporarily comment out HAMPI dependent code - the HAMPI build.xml doesn't work, there is no HAMPI.jar, and Eclipse just silently stops building because of compile errors
>>>>> symbc please fix this <<<<<
* Config.getStringArray() and it's various variants were returning empty arrays for "x.y=" settings, where it should return null / the default values
* mod of ConsolePublisher to print "started"/"finished" markers only if there are "start" or "finished" topics, assuming that users otherwise want no output whatsoever
Modified Paths:
--------------
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/string/SymbolicStringConstraintsGeneral.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/string/SymbolicStringConstraintsHAMPI.java
trunk/src/gov/nasa/jpf/Config.java
trunk/src/gov/nasa/jpf/report/ConsolePublisher.java
trunk/src/gov/nasa/jpf/report/Publisher.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2009-05-18 21:47:19
|
Revision: 1532
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1532&view=rev
Author: pcmehlitz
Date: 2009-05-18 21:47:10 +0000 (Mon, 18 May 2009)
Log Message:
-----------
* IMPORTANT - Config initialization is now flattened, and values are expanded upon entry. This means that clients that need to process raw values (including var names) would not work anymore, and the order of symbolic entries does now matter (processed sequentially). On the other hand, we didn't have such clients in the distrib, but lots of clients didn't use getExpandedXX() instead of getXX(), so this is going to fix a lot of config problems.
Note that we can also do recursive init now, like in
vm.classpath=my/path,${vm.classpath}
the old '+=' append still works too, but with the same restrictions in property files (no blanks between key and '+') - we should use our own parsing at some point.
* since there is no Config.defaults anymore, the publishers had to be updated. Decided against throwing a Config.Exception if defaults.properties is not found, since a lot of clients do not handle exceptions during Config init, and some of them don't even need default.properties
Modified Paths:
--------------
trunk/examples/launch/basic-random.launch
trunk/examples/launch/conc-1-RA.launch
trunk/extensions/cv/src/gov/nasa/jpf/cv/SCSafetyListener.java
trunk/extensions/statechart/env/jvm/gov/nasa/jpf/jvm/NativeStateMachine.java
trunk/extensions/statechart/src/gov/nasa/jpf/tools/sc/SCInspector.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/ClassInfo.java
trunk/src/gov/nasa/jpf/report/ConsolePublisher.java
trunk/src/gov/nasa/jpf/report/HTMLPublisher.java
trunk/src/gov/nasa/jpf/report/XMLPublisher.java
trunk/src/gov/nasa/jpf/tools/JavaJPF.java
trunk/src/gov/nasa/jpf/util/Inspector.java
trunk/test/gov/nasa/jpf/jvm/TestJPF.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <ne...@us...> - 2009-06-17 22:52:31
|
Revision: 1648
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1648&view=rev
Author: nehas
Date: 2009-06-17 22:49:44 +0000 (Wed, 17 Jun 2009)
Log Message:
-----------
Initial commit of the guided execution engine for JPF
* Contains the abstraction, refinement and heuristic computation in the absrefine.jar
* Currently guides the concrete execution
* The hook for guiding symbolic is coming soon
Updating the class path for the absrefine dependency.
Modified Paths:
--------------
trunk/.classpath
Added Paths:
-----------
trunk/extensions/guidedsymbolic/lib/
trunk/extensions/guidedsymbolic/lib/absrefine.jar
trunk/extensions/guidedsymbolic/src/
trunk/extensions/guidedsymbolic/src/edu/
trunk/extensions/guidedsymbolic/src/edu/byu/
trunk/extensions/guidedsymbolic/src/edu/byu/cs/
trunk/extensions/guidedsymbolic/src/edu/byu/cs/guided/
trunk/extensions/guidedsymbolic/src/edu/byu/cs/guided/jpf/
trunk/extensions/guidedsymbolic/src/edu/byu/cs/guided/jpf/GuidedListener.java
trunk/extensions/guidedsymbolic/src/edu/byu/cs/guided/jpf/TrackLocations.java
trunk/extensions/guidedsymbolic/src/edu/byu/cs/guided/search/
trunk/extensions/guidedsymbolic/src/edu/byu/cs/guided/search/heuristic/
trunk/extensions/guidedsymbolic/src/edu/byu/cs/guided/search/heuristic/DebugGuided.java
trunk/extensions/guidedsymbolic/src/edu/byu/cs/guided/search/heuristic/GuidedDFSearch.java
trunk/extensions/guidedsymbolic/src/edu/byu/cs/guided/search/heuristic/MetaHeuristic.java
trunk/extensions/guidedsymbolic/src/edu/byu/cs/guided/search/heuristic/MetaHeuristicState.java
trunk/extensions/guidedsymbolic/src/edu/byu/cs/guided/search/heuristic/MetaLevelComparator.java
trunk/extensions/guidedsymbolic/src/edu/byu/cs/guided/search/heuristic/PFSMHeuristic.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
×
Want the latest updates on software, tech news, and AI?
Get latest updates about software, tech news, and AI from SourceForge directly in your inbox once a month.
Thanks for helping keep SourceForge clean.
X