Thread: [Javapathfinder-svn] SF.net SVN: javapathfinder:[931] trunk

Status: Beta

Brought to you by: artimid, johnpenix, masoud_mansouri, pcdillinger, and 3 others

javapathfinder-svn

[Javapathfinder-svn] SF.net SVN: javapathfinder:[931] trunk

From: <pcm...@us...> - 2008-07-18 08:04:10

Revision: 931
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=931&view=rev
Author:   pcmehlitz
Date:     2008-07-18 08:04:04 +0000 (Fri, 18 Jul 2008)

Log Message:
-----------
* backported the nasty v5 SharedSecrets stuff to make the trunk compatible with Java 6

* moved from the old UIActionGenerator (EventGenerator) mechanism to the new
ScriptEnvironment. Not sure if we ever need the power of sequence interpreters
for UI model checking (which should always have finite event sequences), but
I don't want to support two mechanisms (EventGenerator loops were apparently broken!)

* turned the ScriptEnvironment into a generic class so that we don't need the
silly concrete CG type casts in clients anymore

* added ChoiceGenerator subsystem init(config). Required if we ever use ChoiceGenerators
outside a JVM context (like SimStateMachine, or UIInspector)


that leaves only the new interrupt handling to be backported from v5
(which is going to take more time to become operational, so trunk should be up-to-date)  

Modified Paths:
--------------
    trunk/env/jpf/java/lang/Class.java
    trunk/env/jpf/java/lang/System.java
    trunk/env/jpf/java/lang/reflect/Method.java
    trunk/env/jpf/sun/misc/Unsafe.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_sun_misc_Unsafe.java
    trunk/extensions/statechart/env/jvm/gov/nasa/jpf/jvm/NativeStateMachine.java
    trunk/extensions/statechart/src/gov/nasa/jpf/jvm/choice/sc/SCScriptEnvironment.java
    trunk/extensions/ui/env/jvm/gov/nasa/jpf/jvm/JPF_java_awt_EventDispatchThread.java
    trunk/extensions/ui/src/gov/nasa/jpf/jvm/choice/ui/UIAction.java
    trunk/extensions/ui/src/gov/nasa/jpf/jvm/choice/ui/UIActionFromSet.java
    trunk/extensions/ui/src/gov/nasa/jpf/jvm/choice/ui/UIActionSingleChoice.java
    trunk/extensions/ui/src/gov/nasa/jpf/tools/UIInspector.java
    trunk/src/gov/nasa/jpf/jvm/ChoiceGenerator.java
    trunk/src/gov/nasa/jpf/jvm/JVM.java
    trunk/src/gov/nasa/jpf/util/Inspector.java
    trunk/src/gov/nasa/jpf/util/script/ScriptEnvironment.java

Added Paths:
-----------
    trunk/env/jpf/java/lang/annotation/
    trunk/env/jpf/java/lang/annotation/Inherited.java
    trunk/env/jpf/java/lang/annotation/Retention.java
    trunk/env/jpf/sun/misc/JavaIOAccess.java
    trunk/env/jpf/sun/misc/JavaIODeleteOnExitAccess.java
    trunk/env/jpf/sun/misc/JavaIOFileDescriptorAccess.java
    trunk/env/jpf/sun/misc/JavaLangAccess.java
    trunk/env/jpf/sun/misc/JavaNetAccess.java
    trunk/env/jpf/sun/misc/SharedSecrets.java
    trunk/env/jpf/sun/nio/
    trunk/env/jpf/sun/nio/ch/
    trunk/env/jpf/sun/nio/ch/Interruptible.java
    trunk/env/jpf/sun/reflect/
    trunk/env/jpf/sun/reflect/ConstantPool.java
    trunk/env/jpf/sun/reflect/annotation/
    trunk/env/jpf/sun/reflect/annotation/AnnotationType.java
    trunk/extensions/ui/src/gov/nasa/jpf/jvm/choice/ui/UIScriptEnvironment.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

[Javapathfinder-svn] SF.net SVN: javapathfinder:[933] trunk

From: <pcm...@us...> - 2008-07-18 20:48:28

Revision: 933
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=933&view=rev
Author:   pcmehlitz
Date:     2008-07-18 20:48:25 +0000 (Fri, 18 Jul 2008)

Log Message:
-----------
* backported the new interrupt handling from v5

that should bring trunk to par with v5 with respect to Java 1.5/6 compatibility

Modified Paths:
--------------
    trunk/env/jpf/java/lang/Thread.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Object.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Thread.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_sun_misc_Unsafe.java
    trunk/src/gov/nasa/jpf/jvm/DefaultSchedulerFactory.java
    trunk/src/gov/nasa/jpf/jvm/ElementInfo.java
    trunk/src/gov/nasa/jpf/jvm/Monitor.java
    trunk/src/gov/nasa/jpf/jvm/SchedulerFactory.java
    trunk/src/gov/nasa/jpf/jvm/ThreadInfo.java
    trunk/src/gov/nasa/jpf/jvm/choice/ThreadChoiceFromSet.java

Added Paths:
-----------
    trunk/test/gov/nasa/jpf/jvm/TestExecutorService.java
    trunk/test/gov/nasa/jpf/jvm/TestExecutorServiceJPF.java
    trunk/test/gov/nasa/jpf/jvm/TestInterrupt.java
    trunk/test/gov/nasa/jpf/jvm/TestInterruptJPF.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

[Javapathfinder-svn] SF.net SVN: javapathfinder:[935] trunk

From: <pcm...@us...> - 2008-07-22 06:08:59

Revision: 935
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=935&view=rev
Author:   pcmehlitz
Date:     2008-07-22 06:08:58 +0000 (Tue, 22 Jul 2008)

Log Message:
-----------
* basic NetBeans project support. It's very incomplete since it's not dealing with
extensions yet, and the only way to run stuff is by using single-file-run actions
(which have to be folder-specific). But at least it builds, and we can specify
mode properties in a *.properties file that is associated with the single-run target

Modified Paths:
--------------
    trunk/build.xml

Added Paths:
-----------
    trunk/examples/oldclassic.properties
    trunk/nbproject/
    trunk/nbproject/genfiles.properties
    trunk/nbproject/ide-file-targets.xml
    trunk/nbproject/jdk.xml
    trunk/nbproject/nbjdk.xml
    trunk/nbproject/project.xml


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

[Javapathfinder-svn] SF.net SVN: javapathfinder:[936] trunk

From: <pcm...@us...> - 2008-07-25 16:12:23

Revision: 936
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=936&view=rev
Author:   pcmehlitz
Date:     2008-07-25 16:12:21 +0000 (Fri, 25 Jul 2008)

Log Message:
-----------
* added optional include/exclude filter for PreciseRaceDetector

* added test cases for field filters

Modified Paths:
--------------
    trunk/src/gov/nasa/jpf/tools/PreciseRaceDetector.java
    trunk/test/gov/nasa/jpf/mc/TestRace.java
    trunk/test/gov/nasa/jpf/mc/TestRaceJPF.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

[Javapathfinder-svn] SF.net SVN: javapathfinder:[937] trunk

From: <pcm...@us...> - 2008-07-29 05:34:01

Revision: 937
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=937&view=rev
Author:   pcmehlitz
Date:     2008-07-29 05:33:59 +0000 (Tue, 29 Jul 2008)

Log Message:
-----------
* made the log handler class configurable (+log.handler.class), to better interface to IDEs. The fallback is still
our LogHandler, but the warning should be changed

Modified Paths:
--------------
    trunk/build.xml
    trunk/default.properties
    trunk/nbproject/project.xml
    trunk/src/gov/nasa/jpf/util/LogManager.java

Property Changed:
----------------
    trunk/nbproject/


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

[Javapathfinder-svn] SF.net SVN: javapathfinder:[939] trunk

From: <pcm...@us...> - 2008-07-29 19:34:48

Revision: 939
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=939&view=rev
Author:   pcmehlitz
Date:     2008-07-29 19:34:45 +0000 (Tue, 29 Jul 2008)

Log Message:
-----------
* moved choco-1_2_04.jar to symbc/lib, where it belongs

* updated the build paths accordingly

Modified Paths:
--------------
    trunk/.classpath

Added Paths:
-----------
    trunk/extensions/symbc/lib/choco-1_2_04.jar

Removed Paths:
-------------
    trunk/choco-1_2_04.jar


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

[Javapathfinder-svn] SF.net SVN: javapathfinder:[940] trunk

From: <pcm...@us...> - 2008-07-30 01:25:11

Revision: 940
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=940&view=rev
Author:   pcmehlitz
Date:     2008-07-30 01:25:08 +0000 (Wed, 30 Jul 2008)

Log Message:
-----------
* attempt to clean up nbproject/project.xml so that the NB internal compiler doesn't do bogus complains anymore (some things were spurious)

* added a JPF.createConfig(String configName,String[] args) so that we don't need to create silly pseudo args if we just run off a config file
(this required some sanity checks in Config in case the args are null)

Modified Paths:
--------------
    trunk/nbproject/project.xml
    trunk/src/gov/nasa/jpf/Config.java
    trunk/src/gov/nasa/jpf/JPF.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

[Javapathfinder-svn] SF.net SVN: javapathfinder:[946] trunk

From: <pcm...@us...> - 2008-07-31 17:12:44

Revision: 946
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=946&view=rev
Author:   pcmehlitz
Date:     2008-07-31 17:04:41 +0000 (Thu, 31 Jul 2008)

Log Message:
-----------
* StateMachine.wasGuardedCompletion was reset within a log level block - Duhh! That fixes Corina's open state space example (was working w/o logging)

* of course there was a state space leak when logging sendEvent (was creating a StringBuilder). Replaced this with a native
logAppend(String)...log() API, which maps to ThreadLocal StringBuilders

   having separate NativeStateMachine and SimStateMachine implementations sucks - move into model

* ChoiceTracker config error report fixed

* standard example launch configs were still using +vm.enumerate_random, should be +cg.

Modified Paths:
--------------
    trunk/examples/launch/basic-racer-test.launch
    trunk/examples/launch/basic-random-test.launch
    trunk/examples/launch/basic-random.launch
    trunk/extensions/statechart/env/jpf/gov/nasa/jpf/sc/State.java
    trunk/extensions/statechart/env/jpf/gov/nasa/jpf/sc/StateMachine.java
    trunk/extensions/statechart/env/jvm/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_sc_StateMachine.java
    trunk/extensions/statechart/env/jvm/gov/nasa/jpf/jvm/NativeStateMachine.java
    trunk/extensions/statechart/src/gov/nasa/jpf/tools/sc/SimStateMachine.java
    trunk/src/gov/nasa/jpf/tools/ChoiceTracker.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

[Javapathfinder-svn] SF.net SVN: javapathfinder:[952] trunk

From: <pcm...@us...> - 2008-08-05 20:40:39

Revision: 952
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=952&view=rev
Author:   pcmehlitz
Date:     2008-08-05 20:40:32 +0000 (Tue, 05 Aug 2008)

Log Message:
-----------
* some more build.xml changes to make NetBeans (6.1) happy with JPF as a free form project

* added an ide subdir. ideally, this should hold all our IDE plugins, but for Eclipse that's rather unlikely (until they finally support nested projects)

* added RunJPF as a VERY simple NetBeans module. This doesn't do much except of adding a "Run JPF" item to the file context menu of *.jpf files,
which are properties files that can reside anywhere in the project (good by Eclipse *.launch configs!) This is the same mechanism to configure
and run JPF that is used by Sandro's VJP (Eclipse plugin)

* added a simple ide/examples/JPFTest project. This is going to evolve into a suite that can be used for NetBeans and Eclipse demos 

Modified Paths:
--------------
    trunk/build.xml

Added Paths:
-----------
    trunk/ide/
    trunk/ide/examples/
    trunk/ide/examples/JPFTest/
    trunk/ide/examples/JPFTest/build.xml
    trunk/ide/examples/JPFTest/manifest.mf
    trunk/ide/examples/JPFTest/nbproject/
    trunk/ide/examples/JPFTest/nbproject/build-impl.xml
    trunk/ide/examples/JPFTest/nbproject/genfiles.properties
    trunk/ide/examples/JPFTest/nbproject/project.properties
    trunk/ide/examples/JPFTest/nbproject/project.xml
    trunk/ide/examples/JPFTest/src/
    trunk/ide/examples/JPFTest/src/jpftest/
    trunk/ide/examples/JPFTest/src/jpftest/Hello.java
    trunk/ide/examples/JPFTest/src/jpftest/Hello.jpf
    trunk/ide/examples/JPFTest/src/jpftest/OldClassic-analyzer.jpf
    trunk/ide/examples/JPFTest/src/jpftest/OldClassic-basic.jpf
    trunk/ide/examples/JPFTest/src/jpftest/OldClassic.java
    trunk/ide/examples/JPFTest/src/jpftest/Racer-exception.jpf
    trunk/ide/examples/JPFTest/src/jpftest/Racer-listener.jpf
    trunk/ide/examples/JPFTest/src/jpftest/Racer.java
    trunk/ide/examples/JPFTest/src/jpftest/Rand.java
    trunk/ide/examples/JPFTest/src/jpftest/Rand.jpf
    trunk/ide/examples/JPFTest/test/
    trunk/ide/netbeans/
    trunk/ide/netbeans/RunJPF/
    trunk/ide/netbeans/RunJPF/build.xml
    trunk/ide/netbeans/RunJPF/manifest.mf
    trunk/ide/netbeans/RunJPF/nbproject/
    trunk/ide/netbeans/RunJPF/nbproject/build-impl.xml
    trunk/ide/netbeans/RunJPF/nbproject/genfiles.properties
    trunk/ide/netbeans/RunJPF/nbproject/platform.properties
    trunk/ide/netbeans/RunJPF/nbproject/project.properties
    trunk/ide/netbeans/RunJPF/nbproject/project.xml
    trunk/ide/netbeans/RunJPF/release/
    trunk/ide/netbeans/RunJPF/release/modules/
    trunk/ide/netbeans/RunJPF/release/modules/ext/
    trunk/ide/netbeans/RunJPF/src/
    trunk/ide/netbeans/RunJPF/src/gov/
    trunk/ide/netbeans/RunJPF/src/gov/nasa/
    trunk/ide/netbeans/RunJPF/src/gov/nasa/runjpf/
    trunk/ide/netbeans/RunJPF/src/gov/nasa/runjpf/Bundle.properties
    trunk/ide/netbeans/RunJPF/src/gov/nasa/runjpf/JPFConfigDataLoader.java
    trunk/ide/netbeans/RunJPF/src/gov/nasa/runjpf/JPFConfigDataLoaderBeanInfo.java
    trunk/ide/netbeans/RunJPF/src/gov/nasa/runjpf/JPFConfigDataNode.java
    trunk/ide/netbeans/RunJPF/src/gov/nasa/runjpf/JPFConfigDataObject.java
    trunk/ide/netbeans/RunJPF/src/gov/nasa/runjpf/JPFConfigEditorSupport.java
    trunk/ide/netbeans/RunJPF/src/gov/nasa/runjpf/JPFConfigResolver.xml
    trunk/ide/netbeans/RunJPF/src/gov/nasa/runjpf/JPFConfigTemplate.jpf
    trunk/ide/netbeans/RunJPF/src/gov/nasa/runjpf/OutputAdapter.java
    trunk/ide/netbeans/RunJPF/src/gov/nasa/runjpf/RunJPF.java
    trunk/ide/netbeans/RunJPF/src/gov/nasa/runjpf/layer.xml
    trunk/ide/netbeans/RunJPF/src/gov/nasa/runjpf/runjpf.gif
    trunk/ide/netbeans/RunJPF/test/
    trunk/ide/netbeans/RunJPF/test/unit/
    trunk/ide/netbeans/RunJPF/test/unit/src/
    trunk/ide/netbeans/RunJPF/test/unit/src/META-INF/
    trunk/ide/netbeans/RunJPF/test/unit/src/META-INF/services/
    trunk/ide/netbeans/RunJPF/test/unit/src/META-INF/services/org.openide.loaders.DataLoader


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

[Javapathfinder-svn] SF.net SVN: javapathfinder:[953] trunk

From: <pcm...@us...> - 2008-08-05 21:20:22

Revision: 953
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=953&view=rev
Author:   pcmehlitz
Date:     2008-08-05 21:20:17 +0000 (Tue, 05 Aug 2008)

Log Message:
-----------
* Mirko's and Igor's java.lang.reflect patches - Thanks 

Modified Paths:
--------------
    trunk/env/jpf/java/lang/reflect/Field.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_reflect_Array.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_reflect_Field.java
    trunk/test/gov/nasa/jpf/jvm/TestFieldReflection.java
    trunk/test/gov/nasa/jpf/jvm/TestFieldReflectionJPF.java

Added Paths:
-----------
    trunk/test/gov/nasa/jpf/jvm/TestArrayReflection.java
    trunk/test/gov/nasa/jpf/jvm/TestArrayReflectionJPF.java

Property Changed:
----------------
    trunk/ide/examples/JPFTest/
    trunk/ide/examples/JPFTest/nbproject/
    trunk/ide/netbeans/RunJPF/nbproject/


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

[Javapathfinder-svn] SF.net SVN: javapathfinder:[960] trunk

From: <pcm...@us...> - 2008-08-13 18:50:43

Revision: 960
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=960&view=rev
Author:   pcmehlitz
Date:     2008-08-13 18:50:38 +0000 (Wed, 13 Aug 2008)

Log Message:
-----------
* missing guards for getAnnotationInfo() on classes that don't have any, triggering NPEs e.g. when executing JUnit

Modified Paths:
--------------
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Class.java
    trunk/src/gov/nasa/jpf/jvm/ClassInfo.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.

[Javapathfinder-svn] SF.net SVN: javapathfinder:[964] trunk

From: <pcm...@us...> - 2008-08-20 20:08:59

Revision: 964
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=964&view=rev
Author:   pcmehlitz
Date:     2008-08-20 20:08:51 +0000 (Wed, 20 Aug 2008)

Log Message:
-----------
* moved MethodInfo attributes to flag fields (like Field/Class/ElementInfo). That just makes it easier
to add new attributes, of which we have two new ones: EXEC_HIDDEN and FIREWALL. The first one is used
for methods that are not only executed atomically, but should also not appear in the path. The second
one is for methods that should act as exception firewalls, i.e. turn JPF-executed exceptions into
UnhandledException throws. That's for all methods which should not let exceptions pass in lower stack
frames, mostly because they aren't called by them (like clinit or other direct calls)

* streamlined ThreadInfo.throwException to use these attributes

* since we can now have UnhandledExceptions in code we still want to continue from, we also
need a way to clear the pendingException, the NoUnhandledExceptionProperty, drop frames and
advance the pc in the topframe (or else we run the danger of infinite loops)

* with that, improved the code for atomic round trips (i.e. atomically executing bytecode by JPF
from listeners or native peers). This is still a dangerous feature, but - if supported - should
leave the choice of path-hidden execution and exception handling to the host-VM executed code that
starts it. Still the same restrictions like for executeMethodAtomic apply. See TestNativePeerJPF
for examples (hidden exec with and w/o exceptions)

Modified Paths:
--------------
    trunk/src/gov/nasa/jpf/jvm/MethodInfo.java
    trunk/src/gov/nasa/jpf/jvm/StackFrame.java
    trunk/src/gov/nasa/jpf/jvm/ThreadInfo.java
    trunk/src/gov/nasa/jpf/test/Satisfies.java
    trunk/test/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_jvm_TestNativePeer.java
    trunk/test/gov/nasa/jpf/jvm/TestNativePeer.java
    trunk/test/gov/nasa/jpf/jvm/TestNativePeerJPF.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

[Javapathfinder-svn] SF.net SVN: javapathfinder:[973] trunk

From: <ubn...@us...> - 2008-08-23 00:16:51

Revision: 973
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=973&view=rev
Author:   ubnepvpb
Date:     2008-08-23 00:16:48 +0000 (Sat, 23 Aug 2008)

Log Message:
-----------
Carl Albach's StateChart animation GUI
Changes to core JPF methods are mostly visibility changes

Modified Paths:
--------------
    trunk/env/jpf/java/lang/reflect/Field.java
    trunk/env/jpf/java/lang/reflect/Method.java
    trunk/extensions/statechart/env/jpf/gov/nasa/jpf/sc/State.java
    trunk/extensions/statechart/env/jpf/gov/nasa/jpf/sc/StateMachine.java
    trunk/src/gov/nasa/jpf/tools/ChoiceTracker.java

Added Paths:
-----------
    trunk/extensions/statechart/examples/samplevisualizeconfigs/
    trunk/extensions/statechart/examples/samplevisualizeconfigs/cev-ascent-guards
    trunk/extensions/statechart/examples/samplevisualizeconfigs/cev-las-defect
    trunk/extensions/statechart/examples/samplevisualizeconfigs/cev-safehold
    trunk/extensions/statechart/examples/samplevisualizeconfigs/cev-scriptless
    trunk/extensions/statechart/examples/samplevisualizeconfigs/cev-scriptless-bt
    trunk/extensions/statechart/examples/samplevisualizeconfigs/cev-scriptless-constraints
    trunk/extensions/statechart/examples/samplevisualizeconfigs/cev-tli
    trunk/extensions/statechart/examples/samplevisualizeconfigs/cv-assumption
    trunk/extensions/statechart/examples/visualize/
    trunk/extensions/statechart/examples/visualize/CEV_15EOR_LOR.java
    trunk/extensions/statechart/examples/visualize/ErrorLog.java
    trunk/extensions/statechart/examples/visualize/Failures.java
    trunk/extensions/statechart/examples/visualize/README-ESAS.txt
    trunk/extensions/statechart/examples/visualize/README-annotations.txt
    trunk/extensions/statechart/examples/visualize/Spacecraft.java
    trunk/extensions/statechart/src/gov/nasa/jpf/tools/visualize/
    trunk/extensions/statechart/src/gov/nasa/jpf/tools/visualize/EdgeUtility.java
    trunk/extensions/statechart/src/gov/nasa/jpf/tools/visualize/NotificationConsole.java
    trunk/extensions/statechart/src/gov/nasa/jpf/tools/visualize/ReadMe
    trunk/extensions/statechart/src/gov/nasa/jpf/tools/visualize/StateMachineDiagram.java
    trunk/extensions/statechart/src/gov/nasa/jpf/tools/visualize/TextDiagram.java
    trunk/extensions/statechart/src/gov/nasa/jpf/tools/visualize/VisualDiagram.java
    trunk/extensions/statechart/src/gov/nasa/jpf/tools/visualize/VisualDriver.java
    trunk/extensions/statechart/src/gov/nasa/jpf/tools/visualize/VisualModel.java
    trunk/extensions/statechart/src/gov/nasa/jpf/tools/visualize/VisualResource.java
    trunk/extensions/statechart/src/gov/nasa/jpf/tools/visualize/VisualSimStateMachine.java
    trunk/extensions/statechart/src/gov/nasa/jpf/tools/visualize/VisualView.java
    trunk/extensions/statechart/src/gov/nasa/jpf/tools/visualize/annotations/
    trunk/extensions/statechart/src/gov/nasa/jpf/tools/visualize/annotations/ExternalState.java
    trunk/extensions/statechart/src/gov/nasa/jpf/tools/visualize/annotations/NextNeighbor.java
    trunk/extensions/statechart/src/gov/nasa/jpf/tools/visualize/annotations/README-annotations.txt
    trunk/extensions/statechart/src/gov/nasa/jpf/tools/visualize/annotations/Transitions.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

[Javapathfinder-svn] SF.net SVN: javapathfinder:[988] trunk

From: <pcm...@us...> - 2008-08-28 17:47:43

Revision: 988
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=988&view=rev
Author:   pcmehlitz
Date:     2008-08-28 17:47:38 +0000 (Thu, 28 Aug 2008)

Log Message:
-----------
* implemented native Class.getMethods()

* applied Taehoon's Class/ClassLoader patch (sans getMethods())

* added a little reg test for getMethods()

Modified Paths:
--------------
    trunk/env/jpf/java/lang/Class.java
    trunk/env/jpf/java/lang/ClassLoader.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Class.java
    trunk/test/gov/nasa/jpf/jvm/TestJavaLangClass.java
    trunk/test/gov/nasa/jpf/jvm/TestJavaLangClassJPF.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

[Javapathfinder-svn] SF.net SVN: javapathfinder:[1235] trunk

From: <pcm...@us...> - 2009-02-26 23:51:03

Revision: 1235
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1235&view=rev
Author:   pcmehlitz
Date:     2009-02-26 23:50:48 +0000 (Thu, 26 Feb 2009)

Log Message:
-----------
* non-deterministic AtomicFieldUpdater patch from Nathan Reynolds. The spec says that compareAndSwap() is only atomic with respect to the same updater (how useful is that - begs for a tool like JPF), so we turn it into a potential scheduling point if cg.enumerate_cas=true (false by default)

still needs some refactoring to avoid duplication, and should check for shared objects/multiple runnables

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/JPF_gov_nasa_jpf_jvm_Verify.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
    trunk/test/gov/nasa/jpf/jvm/TestAtomicReferenceFieldUpdater.java
    trunk/test/gov/nasa/jpf/jvm/TestAtomicReferenceFieldUpdaterJPF.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

[Javapathfinder-svn] SF.net SVN: javapathfinder:[989] trunk

From: <pc...@us...> - 2008-08-28 19:04:18

Revision: 989
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=989&view=rev
Author:   pcorina
Date:     2008-08-28 19:04:13 +0000 (Thu, 28 Aug 2008)

Log Message:
-----------
Committed patch contributed by Adam Kiezun (ak...@gm...) and David Harvison (dha...@mi...) -- thank you!

Modified Paths:
--------------
    trunk/extensions/symbc/examples/coverage/JPF_coverage_CheckCoverage.java
    trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/BinaryLinearIntegerExpression.java
    trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/Constraint.java
    trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/IntegerConstant.java
    trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/IntegerExpression.java
    trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/LinearIntegerConstraint.java
    trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/LinearIntegerExpression.java
    trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/MixedConstraint.java
    trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/NonLinearIntegerConstraint.java
    trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/Operator.java
    trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/PathCondition.java
    trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/RealConstant.java
    trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/RealConstraint.java
    trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/SymbolicConstraintsChoco.java
    trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/SymbolicConstraintsGeneral.java
    trunk/extensions/symbc/test/gov/nasa/jpf/symbc/JPF_gov_nasa_jpf_symbc_TestUtils.java
    trunk/extensions/symbc/test/gov/nasa/jpf/symbc/PathConditionListener.java
    trunk/src/gov/nasa/jpf/JPFException.java
    trunk/src/gov/nasa/jpf/jvm/DynamicElementInfo.java
    trunk/src/gov/nasa/jpf/jvm/StaticElementInfo.java
    trunk/src/gov/nasa/jpf/search/Simulation.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

[Javapathfinder-svn] SF.net SVN: javapathfinder:[991] trunk

From: <pcm...@us...> - 2008-08-29 00:22:06

Revision: 991
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=991&view=rev
Author:   pcmehlitz
Date:     2008-08-29 00:22:02 +0000 (Fri, 29 Aug 2008)

Log Message:
-----------
* bug in class initialization - we also need static class init of interface ClassInfos. This sucks, since it is tree recursive. It showed up with interface class objects being null 

* with that, fixed Class.getMethods() native peer - for abstract classes, we have to add all unimplemented interface methods, i.e. we have to get all interface methods, and then check if we can map to any of the methods found in the class hierarchy. Also removed the isStatic() filter (which was brain failure)

Modified Paths:
--------------
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Class.java
    trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
    trunk/test/gov/nasa/jpf/jvm/TestJavaLangClass.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

[Javapathfinder-svn] SF.net SVN: javapathfinder:[993] trunk

From: <pcm...@us...> - 2008-08-30 02:09:16

Revision: 993
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=993&view=rev
Author:   pcmehlitz
Date:     2008-08-30 02:09:13 +0000 (Sat, 30 Aug 2008)

Log Message:
-----------
* fixed build.xml compile-extension-examples misspeller - thanks Darko

* removed some more erased ChoiceGenerator type refs, which unveiled two (trivial) symbc/DCMPx compiler errors

* added Annotation.annotationType() to the AnnotationProxyBase. This again showed a missing annotation class
object. Ad hoc fixed the init in ClassInfo.getAnnotationProxy(), but this is a general problem - maybe we
should just set the class objects for non-clinit classes from their ctors

* added Class.getConstructors()

* modified JPF_java_lang_System to use the ClassInfo.buildPath for setting the java.class.path (if it's
not overridden with vm.system.properties), otherwise we get inconsistent if anybody ever uses it

* started on the budget control via java.lang.management, but it's not functional yet

Modified Paths:
--------------
    trunk/build.xml
    trunk/env/jpf/gov/nasa/jpf/AnnotationProxyBase.java
    trunk/env/jpf/java/lang/Class.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_AnnotationProxyBase.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Class.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_System.java
    trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/DCMPG.java
    trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/DCMPL.java
    trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
    trunk/src/gov/nasa/jpf/jvm/SystemState.java
    trunk/src/gov/nasa/jpf/jvm/ThreadInfo.java
    trunk/test/gov/nasa/jpf/jvm/TestAttrs.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

[Javapathfinder-svn] SF.net SVN: javapathfinder:[995] trunk

From: <st...@us...> - 2008-09-02 05:25:38

Revision: 995
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=995&view=rev
Author:   staats
Date:     2008-09-02 05:25:34 +0000 (Tue, 02 Sep 2008)

Log Message:
-----------
Initial check-in of ComplexCoverage extension

Modified Paths:
--------------
    trunk/.classpath

Added Paths:
-----------
    trunk/extensions/complexcoverage/src/gov/
    trunk/extensions/complexcoverage/src/gov/nasa/
    trunk/extensions/complexcoverage/src/gov/nasa/jpf/
    trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/
    trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/Debug.java
    trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/DebugListener.java
    trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/GenericTestSuiteListener.java
    trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/JPF_crisys_jpf_Debug.java
    trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/TestCase.java
    trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/TestSuite.java
    trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/choice/
    trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/choice/SymbolicChoiceGenerator.java
    trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/choice/TaggedBooleanChoiceGenerator.java
    trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/choice/TaggedIntChoiceGenerator.java
    trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/mcdc/
    trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/mcdc/MCDCCoveragePrinter.java
    trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/mcdc/MeasureTestSuiteByMCDC.java
    trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/mcdc/MeasureTestSuiteByMCDCListener.java
    trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/mcdc/ReduceTestSuiteByMCDC.java
    trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/mcdc/ReduceTestSuiteByMCDCListener.java
    trunk/extensions/complexcoverage/test/ComplexCoverage TestFun Measure Reduced.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.launch
    trunk/extensions/complexcoverage/test/ComplexCoverage TestFun Symbolic.launch
    trunk/extensions/complexcoverage/test/ComplexCoverage TestFun2 Symbolic.launch
    trunk/extensions/complexcoverage/test/ComplexCoverage TestFun2.launch
    trunk/extensions/complexcoverage/test/gov/
    trunk/extensions/complexcoverage/test/gov/nasa/
    trunk/extensions/complexcoverage/test/gov/nasa/jpf/
    trunk/extensions/complexcoverage/test/gov/nasa/jpf/complexcoverage/
    trunk/extensions/complexcoverage/test/gov/nasa/jpf/complexcoverage/test/
    trunk/extensions/complexcoverage/test/gov/nasa/jpf/complexcoverage/test/Docking.java
    trunk/extensions/complexcoverage/test/gov/nasa/jpf/complexcoverage/test/SimpleExampleWDebug.java
    trunk/extensions/complexcoverage/test/gov/nasa/jpf/complexcoverage/test/TestFile.java
    trunk/extensions/complexcoverage/test/gov/nasa/jpf/complexcoverage/test/TestFile2.java

Removed Paths:
-------------
    trunk/extensions/complexcoverage/src/test.txt


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

[Javapathfinder-svn] SF.net SVN: javapathfinder:[1003] trunk

From: <pcm...@us...> - 2008-09-06 01:58:44

Revision: 1003
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1003&view=rev
Author:   pcmehlitz
Date:     2008-09-06 01:58:42 +0000 (Sat, 06 Sep 2008)

Log Message:
-----------
* missing class object and clinit execution for Method and Constructor reflection
(getReturnType() and getParameterTypes()). The latter one was delegating to 
MJIEnv, using a ClinitRequired exception, which was lame - wherever the caller
can detect the need for re-exec of a known insn or native method, it should do so w/o
reverting to control flow exceptions. Consequently removed the MJIEnv.getParameterTypeArray(),
but left the ClinitRequired exception type in there, in case this happens from a location
where we don't know how to repeat

* refactored Consructor/Method native peers a bit to avoid code duplication (beware - we use
different registries for ctors and methods)

* added some test cases for this to TestMethodReflection

this should solve Taehoon's problem  

Modified Paths:
--------------
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_reflect_Constructor.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_reflect_Method.java
    trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
    trunk/src/gov/nasa/jpf/jvm/MJIEnv.java
    trunk/test/gov/nasa/jpf/jvm/TestJavaLangString.java
    trunk/test/gov/nasa/jpf/jvm/TestMethodReflection.java
    trunk/test/gov/nasa/jpf/jvm/TestMethodReflectionJPF.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

[Javapathfinder-svn] SF.net SVN: javapathfinder:[1006] trunk

From: <pcm...@us...> - 2008-09-10 18:31:21

Revision: 1006
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1006&view=rev
Author:   pcmehlitz
Date:     2008-09-10 18:31:19 +0000 (Wed, 10 Sep 2008)

Log Message:
-----------
* getAnnotations() always returns an array - if there are no annotations for a class/method/field,
a global empty array is returned. We init this lazily ince not too many programs use it

Modified Paths:
--------------
    trunk/env/jpf/java/lang/Class.java
    trunk/env/jpf/java/lang/System.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Class.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_reflect_Field.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_reflect_Method.java
    trunk/src/gov/nasa/jpf/JPF.java
    trunk/src/gov/nasa/jpf/jvm/AnnotationInfo.java
    trunk/src/gov/nasa/jpf/jvm/JVM.java
    trunk/src/gov/nasa/jpf/jvm/MJIEnv.java
    trunk/src/gov/nasa/jpf/report/Statistics.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

[Javapathfinder-svn] SF.net SVN: javapathfinder:[1007] trunk

From: <pcm...@us...> - 2008-09-13 02:40:17

Revision: 1007
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1007&view=rev
Author:   pcmehlitz
Date:     2008-09-13 02:40:15 +0000 (Sat, 13 Sep 2008)

Log Message:
-----------
* changed run scripts so that $CLASSPATH is inserted *before* jpf elements, otherwise you can't override

* extended the OutOfMemory handling in JPF.run a little, using a safety margin object that gets released
before some Runtime.gc() calls, to give the VM something to complete JPF reporting

* checked for non-public peer classes in NativePeer.locatePeerCls(), since we otherwise just get
IllegalAccessExceptions that are passed down into the app, which might just catch it silently. Also
added a log warning in case a non-public peer class is skipped, and added log records for
executeMethod() exceptions that are passed down

* sure enough, the ConsoleOutputStream peer wasn't public (but just called within package)

* added a PublisherExtensionAdapter so that it's more easy to create separate PublisherExtension objects,
which is required if we want to use existing Listeners with new Publishers (e.g. for IDEs). In this case,
first the listener is created, then the PublisherExtension with that listener object as parameter, and
then both are registered with JPF

* after much consideration, added a minimal budget management solution in form of the BudgetChecker listener.
It's far from ideal because there is way too much redundancy with Statistics mgnt (which has to be streamlined!),
and there is considerable confusion between "search constraints" (which do *not* terminate the search but only
prune the tree), "budget constraints" (which do terminate, but are optional), and out-of-memory exceptions
(which also terminate, but are our mandatory last line of defense).

Better integration has to wait until v5, since it requires some sort of JPF Result object, encapsulating the
four possible outcomes of a JPF run:
 - proper termination (possibly with constraints)
 - property violation (error detected)
 - budget threshold termination
 - JPF exception (incl. out-of-memory) 

What also becomes clear is that we really have to reduce the instruction logging (Step) cost, since this is
in most cases the budget limiter 

Modified Paths:
--------------
    trunk/bin/javajpf
    trunk/bin/jpf
    trunk/bin/jpf.bat
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_ConsoleOutputStream.java
    trunk/src/gov/nasa/jpf/Config.java
    trunk/src/gov/nasa/jpf/JPF.java
    trunk/src/gov/nasa/jpf/jvm/NativePeer.java
    trunk/src/gov/nasa/jpf/report/Publisher.java
    trunk/src/gov/nasa/jpf/report/Reporter.java

Added Paths:
-----------
    trunk/src/gov/nasa/jpf/report/PublisherExtensionAdapter.java
    trunk/src/gov/nasa/jpf/tools/BudgetChecker.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

[Javapathfinder-svn] SF.net SVN: javapathfinder:[1014] trunk

From: <pcm...@us...> - 2008-09-16 22:43:55

Revision: 1014
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1014&view=rev
Author:   pcmehlitz
Date:     2008-09-17 05:43:53 +0000 (Wed, 17 Sep 2008)

Log Message:
-----------
* the beginnings of an annotation based listener autoloading mechanism. The idea is to have a configured
list of annotation to listener class name mappings, and to check upon class load time if a class, field
or method has an autoload listener annotation. If so, the coresponding listener gets automatically
instantiated and registered. If this fails, the annotation is removed from the autoload set (to prevent
having gazillions of failed load attempts).

If an annotation is in the list, but does not have an explicit listener class property, JPF tries
the annotation class name with appended "Checker".

this is mostly aimed at loads of small, dedicated standard listeners like @Const, @NonNull etc., which
would cause rather long jpf.listener lists. We don't want to create hodgepodge listeners just to
keep jpf.listeners small

Modified Paths:
--------------
    trunk/default.properties
    trunk/src/gov/nasa/jpf/Config.java
    trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
    trunk/src/gov/nasa/jpf/search/Search.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

[Javapathfinder-svn] SF.net SVN: javapathfinder:[1015] trunk

From: <pcm...@us...> - 2008-09-17 11:55:26

Revision: 1015
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1015&view=rev
Author:   pcmehlitz
Date:     2008-09-17 18:55:23 +0000 (Wed, 17 Sep 2008)

Log Message:
-----------
* fixed autoload init bug

* added little NonNullChecker listener tool

* added TestNonNull example

so far, only @Const and @NonNull are in default.properties. Now we should populate this with more, and add
regression tests

the gov.nasa.jpf.tools should be probably moved to allow for automatic lookup, but that would break a lot
of existing Eclipse launch configs and mode property files

another thought is to put some of the app stuff into default package, so that apps using them really don't
have to have any JPF reference

Modified Paths:
--------------
    trunk/app/gov/nasa/jpf/Const.java
    trunk/default.properties
    trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
    trunk/src/gov/nasa/jpf/tools/ConstChecker.java

Added Paths:
-----------
    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.

[Javapathfinder-svn] SF.net SVN: javapathfinder:[1016] trunk

From: <pcm...@us...> - 2008-09-18 11:08:08

Revision: 1016
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1016&view=rev
Author:   pcmehlitz
Date:     2008-09-18 18:08:05 +0000 (Thu, 18 Sep 2008)

Log Message:
-----------
* added Throwable printStackTrace(PrintWriter/PrintStream) support plus a simple reg. test
(required for running systems that store traces, like JUnit)

Modified Paths:
--------------
    trunk/env/jpf/java/lang/Throwable.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Throwable.java
    trunk/test/gov/nasa/jpf/jvm/TestException.java
    trunk/test/gov/nasa/jpf/jvm/TestExceptionJPF.java

Added Paths:
-----------
    trunk/app/gov/nasa/jpf/NonShared.java

Removed Paths:
-------------
    trunk/app/gov/nasa/jpf/NonShared.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.

1 2 3 4 > >> (Page 1 of 4)