javapathfinder-devel — development related topics (your place if you work with the sources)

[Javapathfinder-devel] javapathfinder/examples/DEOS Thread.java,1.1.1.1,1.2 DEOSProcess.java,1.1.1.1,1.2 DEOSKernel.java,1.1.1.1,1.2 PriorityListOfThreads.java,1.1.1.1,1.2 Scheduler.java,1.1.1.1,1.2 NewTimer.java,1.1.1.1,1.2 PeriodicClock.java,1.1.1.1,1.2

[John P. <joh...@us...>]

Update of /cvsroot/javapathfinder/javapathfinder/examples/DEOS
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv8639/examples/DEOS

Modified Files:
	Thread.java DEOSProcess.java DEOSKernel.java 
	PriorityListOfThreads.java Scheduler.java NewTimer.java 
	PeriodicClock.java 
Log Message:
* fixed a couple of static methods being called via objects
* small changes/fixes to a few comments
* remove unused imports

Index: PeriodicClock.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/examples/DEOS/PeriodicClock.java,v
retrieving revision 1.1.1.1
retrieving revision 1.2
diff -u -d -r1.1.1.1 -r1.2
--- PeriodicClock.java	26 Apr 2005 19:43:49 -0000	1.1.1.1
+++ PeriodicClock.java	17 Oct 2005 11:13:07 -0000	1.2
@@ -18,11 +18,8 @@
 //
 package DEOS;
 
-import gov.nasa.jpf.jvm.Verify;
-
-
 /**
- * DOCUMENT ME!
+ * Clock that goes tick, tick, tick
  */
 public class PeriodicClock {
   int     microSecsPeriod = 0;
@@ -34,7 +31,7 @@
   /**
    * Main constructor
    * @param periodIn, the period of the clock - clock resets to zero
-   * after period time elapsed
+   * after period time has elapsed
    */
   public PeriodicClock (int periodIn) {
     microSecsPeriod = periodIn;
@@ -75,7 +72,7 @@
 
   /**
    * To get the time used in period
-   * @param currentTime the current time on the clock
+   * @return currentTime the current time on the clock
    */
   public int getUsedTime () {
     if (systemInterrupt) {

Index: PriorityListOfThreads.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/examples/DEOS/PriorityListOfThreads.java,v
retrieving revision 1.1.1.1
retrieving revision 1.2
diff -u -d -r1.1.1.1 -r1.2
--- PriorityListOfThreads.java	26 Apr 2005 19:43:49 -0000	1.1.1.1
+++ PriorityListOfThreads.java	17 Oct 2005 11:13:07 -0000	1.2
@@ -18,9 +18,6 @@
 //
 package DEOS;
 
-import gov.nasa.jpf.jvm.Verify;
-
-
 /**
  * DOCUMENT ME!
  */

Index: DEOSKernel.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/examples/DEOS/DEOSKernel.java,v
retrieving revision 1.1.1.1
retrieving revision 1.2
diff -u -d -r1.1.1.1 -r1.2
--- DEOSKernel.java	26 Apr 2005 19:43:29 -0000	1.1.1.1
+++ DEOSKernel.java	17 Oct 2005 11:13:07 -0000	1.2
@@ -24,24 +24,24 @@
 class DEOSKernel {
   //typedef enum
   //{
-  public static int threadSuccess = 0;
-  public static int threadInvalidHandle = 1;
-  public static int threadInvalidInterrupt = 2;
-  public static int threadNotDormant = 3;
-  public static int threadNotSchedulable = 4;
-  public static int threadInsufficientPrivilege = 5;
-  public static int threadNotDynamic = 6;
-  public static int threadNotStatic = 7;
-  public static int threadMaximumThreadsExceeded = 8;
-  public static int threadInsufficientRAMForStack = 9;
-  public static int threadNoSuchThread = 10;
-  public static int threadInvalidTemplate = 11;
-  public static int threadNotActive = 12;
-  public static int threadInScheduleBefore = 13;
-  public static int threadInsufficientBudget = 14;
-  public static int threadDuplicateISR = 15;
-  public static int threadInvalidFromDynamicProcess = 16;
-  public static int threadPrimaryCannotBeISR = 17;
+  public static final int threadSuccess = 0;
+  public static final int threadInvalidHandle = 1;
+  public static final int threadInvalidInterrupt = 2;
+  public static final int threadNotDormant = 3;
+  public static final int threadNotSchedulable = 4;
+  public static final int threadInsufficientPrivilege = 5;
+  public static final int threadNotDynamic = 6;
+  public static final int threadNotStatic = 7;
+  public static final int threadMaximumThreadsExceeded = 8;
+  public static final int threadInsufficientRAMForStack = 9;
+  public static final int threadNoSuchThread = 10;
+  public static final int threadInvalidTemplate = 11;
+  public static final int threadNotActive = 12;
+  public static final int threadInScheduleBefore = 13;
+  public static final int threadInsufficientBudget = 14;
+  public static final int threadDuplicateISR = 15;
+  public static final int threadInvalidFromDynamicProcess = 16;
+  public static final int threadPrimaryCannotBeISR = 17;
 
   static void coldStartKernel () {
     //System.out.println("DEOSKernel.coldStartKernel");		
@@ -113,14 +113,12 @@
 
   static int localStartThread (Thread theThread, int requestedThreadBudget, 
                                int periodIndex) {
-    // changed the followign code because can't pass int (budget) by reference.
-    //  cpuTimeInMicroseconds budget; // budget set by following call.
+    // changed the following code because can't pass int (budget) by reference.
+    //  cpuTimeInMicroseconds budget; 
     int budget; // budget set by following call.
 
-
     //System.out.println("DEOSKernel.localStartThread");
-    budget = Scheduler.currentProcess()
-                      .allocateCPUBudgetForThread(theThread, 
+    budget = DEOSProcess.allocateCPUBudgetForThread(theThread, 
                                                   requestedThreadBudget, 
                                                   periodIndex);
 

Index: DEOSProcess.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/examples/DEOS/DEOSProcess.java,v
retrieving revision 1.1.1.1
retrieving revision 1.2
diff -u -d -r1.1.1.1 -r1.2
--- DEOSProcess.java	26 Apr 2005 19:43:29 -0000	1.1.1.1
+++ DEOSProcess.java	17 Oct 2005 11:13:07 -0000	1.2
@@ -35,7 +35,7 @@
   }
 
   // note - had to change this code because you can't pass an integer
-  // by reference in Java - so not, it returns -1 where it used to
+  // by reference in Java - so note, it returns -1 where it used to
   // return false.  the code in DEOSKernel.java (schedk.cpp) has also
   // been changed to reflect this. -jp
   public static int allocateCPUBudgetForThread (Thread theThread, 

Index: Thread.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/examples/DEOS/Thread.java,v
retrieving revision 1.1.1.1
retrieving revision 1.2
diff -u -d -r1.1.1.1 -r1.2
--- Thread.java	26 Apr 2005 19:43:50 -0000	1.1.1.1
+++ Thread.java	17 Oct 2005 11:13:07 -0000	1.2
@@ -18,9 +18,6 @@
 //
 package DEOS;
 
-import gov.nasa.jpf.jvm.Verify;
-
-
 /**
  * DOCUMENT ME!
  */

Index: NewTimer.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/examples/DEOS/NewTimer.java,v
retrieving revision 1.1.1.1
retrieving revision 1.2
diff -u -d -r1.1.1.1 -r1.2
--- NewTimer.java	26 Apr 2005 19:43:49 -0000	1.1.1.1
+++ NewTimer.java	17 Oct 2005 11:13:07 -0000	1.2
@@ -18,10 +18,6 @@
 //
 package DEOS;
 
-import gov.nasa.jpf.jvm.Verify;
-
-import java.lang.*;
-
 
 /**
  * DOCUMENT ME!

Index: Scheduler.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/examples/DEOS/Scheduler.java,v
retrieving revision 1.1.1.1
retrieving revision 1.2
diff -u -d -r1.1.1.1 -r1.2
--- Scheduler.java	26 Apr 2005 19:43:49 -0000	1.1.1.1
+++ Scheduler.java	17 Oct 2005 11:13:07 -0000	1.2
@@ -18,9 +18,6 @@
 //
 package DEOS;
 
-import gov.nasa.jpf.jvm.Verify;
-
-
 /**
  * DOCUMENT ME!
  */
@@ -59,7 +56,7 @@
     itsRunningThread.startChargingCPUTime();
     CPU.exitCritical(interruptState);
     theProcess = new DEOSProcess();
-    DEOSKernel.localStartThread(theProcess.mainThread(), 
+    DEOSKernel.localStartThread(DEOSProcess.mainThread(), 
                                 Registry.uSecsInFastestPeriod, 0);
   }
 

[Javapathfinder-devel] javapathfinder/src/gov/nasa/jpf/jvm/bytecode GETSTATIC.java,1.1.1.1,1.2 PUTSTATIC.java,1.1.1.1,1.2

[John P. <joh...@us...>]

Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/bytecode
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv535/src/gov/nasa/jpf/jvm/bytecode

Modified Files:
	GETSTATIC.java PUTSTATIC.java 
Log Message:
* bug 1307878
* look up class via FieldInfo (up class hierarchy) - don't use class in bytecode


Index: GETSTATIC.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/bytecode/GETSTATIC.java,v
retrieving revision 1.1.1.1
retrieving revision 1.2
diff -u -d -r1.1.1.1 -r1.2
--- GETSTATIC.java	26 Apr 2005 19:44:11 -0000	1.1.1.1
+++ GETSTATIC.java	17 Oct 2005 04:15:48 -0000	1.2
@@ -33,9 +33,9 @@
  */
 public class GETSTATIC extends StaticFieldInstruction {
   public Instruction execute (SystemState ss, KernelState ks, ThreadInfo ti) {
-    ElementInfo ei = ks.sa.get(className);
-    FieldInfo fi = getFieldInfo();
-    
+  	FieldInfo fi = getFieldInfo();
+  	ElementInfo ei = ks.sa.get(fi.getClassInfo().getName());
+  	    
     switch (size) {
       case 1:
         int ival = ei.getIntField(fi);

Index: PUTSTATIC.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/bytecode/PUTSTATIC.java,v
retrieving revision 1.1.1.1
retrieving revision 1.2
diff -u -d -r1.1.1.1 -r1.2
--- PUTSTATIC.java	26 Apr 2005 19:44:15 -0000	1.1.1.1
+++ PUTSTATIC.java	17 Oct 2005 04:15:48 -0000	1.2
@@ -19,7 +19,6 @@
 package gov.nasa.jpf.jvm.bytecode;
 
 import gov.nasa.jpf.JPFException;
-import gov.nasa.jpf.jvm.ClassInfo;
 import gov.nasa.jpf.jvm.ElementInfo;
 import gov.nasa.jpf.jvm.KernelState;
 import gov.nasa.jpf.jvm.SystemState;
@@ -35,9 +34,8 @@
 public class PUTSTATIC extends StaticFieldInstruction implements StoreInstruction
 {
   public Instruction execute (SystemState ss, KernelState ks, ThreadInfo ti) {
-    ClassInfo   ci = ClassInfo.getClassInfo(className);
-    ElementInfo ei = ks.sa.get(className);
     FieldInfo fi = getFieldInfo();
+    ElementInfo ei = ks.sa.get(fi.getClassInfo().getName());
     
     switch (fi.getStorageSize()) {
       case 1:

[Javapathfinder-devel] javapathfinder/src/gov/nasa/jpf/jvm/bytecode StaticFieldInstruction.java,1.2,1.3

[John P. <joh...@us...>]

Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/bytecode
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv32567/src/gov/nasa/jpf/jvm/bytecode

Modified Files:
	StaticFieldInstruction.java 
Log Message:
* javadoc to indicate that these methods search up the class hierarchy

Index: StaticFieldInstruction.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/bytecode/StaticFieldInstruction.java,v
retrieving revision 1.2
retrieving revision 1.3
diff -u -d -r1.2 -r1.3
--- StaticFieldInstruction.java	7 Sep 2005 22:08:20 -0000	1.2
+++ StaticFieldInstruction.java	17 Oct 2005 04:13:13 -0000	1.3
@@ -28,7 +28,10 @@
  */
 public abstract class StaticFieldInstruction extends FieldInstruction {
   
-  public FieldInfo getFieldInfo () {
+/**
+ * goes up hierarchy from className in bytecode
+ */
+	public FieldInfo getFieldInfo () {
     if (fi == null) {
       ClassInfo ci = ClassInfo.getClassInfo(className);
       if (ci != null) {

[Javapathfinder-devel] javapathfinder/src/gov/nasa/jpf/jvm ClassInfo.java,1.2,1.3

[John P. <joh...@us...>]

Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv31488/src/gov/nasa/jpf/jvm

Modified Files:
	ClassInfo.java 
Log Message:
* javadoc to indicate that these methods search up the class hierarchy

Index: ClassInfo.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/ClassInfo.java,v
retrieving revision 1.2
retrieving revision 1.3
diff -u -d -r1.2 -r1.3
--- ClassInfo.java	5 May 2005 01:03:53 -0000	1.2
+++ ClassInfo.java	17 Oct 2005 04:05:12 -0000	1.3
@@ -398,6 +398,12 @@
     return mi;
   }
   
+  /**
+   * Search up the class hierarchy to find a static field
+   * @param clsBase - name of class to start looking from
+   * @param fName - name of field
+   * @return returns null if field name not found (not declared)
+   */
   public FieldInfo getStaticField (String clsBase, String fName) {
     FieldInfo fi;
     ClassInfo c = getClassBase(clsBase);
@@ -410,7 +416,11 @@
     
     return null;
   }
-  
+  /**
+   * Search up hierarchy to find static field starting from this class
+   * @param fname
+   * @return
+   */
   public FieldInfo getStaticField (String fname) {
     return getStaticField(null, fname);
   }
@@ -418,7 +428,7 @@
   /**
    * FieldInfo lookup in the static fields that are declared in this class
    * <2do> pcm - should employ a map at some point, but it's usually not that
-   * important since we can cash the returned FieldInfo in the PUT/GET_STATIC insns
+   * important since we can cache the returned FieldInfo in the PUT/GET_STATIC insns
    */
   public FieldInfo getDeclaredStaticField (String fName) {
     for (int i=0; i<sFields.length; i++) {
@@ -860,6 +870,12 @@
     return instanceDataOffset;
   }
   
+  /**
+   * Search up class hierarchy for a parent class
+   * @param clsBase name of class to find
+   * @return - return current(this) class if clsBase is null.
+   * - return null if class not found
+   */
   ClassInfo getClassBase (String clsBase) {
     if ((clsBase == null) || (name.equals(clsBase))) return this;
     

[Javapathfinder-devel] /javapathfinder/examples IntChoices.java,1.2,1.3 testchoices.IntChoiceFromSet.properties,1.2,1.3

[John P. <joh...@us...>]

Update of /cvsroot/javapathfinder//javapathfinder/examples
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv25947/examples

Modified Files:
	IntChoices.java testchoices.IntChoiceFromSet.properties 
Log Message:
*updates to go with enhanced IntChoiceFromSet

Index: IntChoices.java
===================================================================
RCS file: /cvsroot/javapathfinder//javapathfinder/examples/IntChoices.java,v
retrieving revision 1.2
retrieving revision 1.3
diff -u -d -r1.2 -r1.3
--- IntChoices.java	12 Sep 2005 16:24:31 -0000	1.2
+++ IntChoices.java	11 Oct 2005 23:56:13 -0000	1.3
@@ -49,7 +49,8 @@
 	}
 
 	public static void main(String[] args) {
-	
+	int z = 22;
+		
 	x = gov.nasa.jpf.jvm.Verify.getInt("xTest");
 	System.out.println("x is "+x);
 

Index: testchoices.IntChoiceFromSet.properties
===================================================================
RCS file: /cvsroot/javapathfinder//javapathfinder/examples/testchoices.IntChoiceFromSet.properties,v
retrieving revision 1.2
retrieving revision 1.3
diff -u -d -r1.2 -r1.3
--- testchoices.IntChoiceFromSet.properties	12 Sep 2005 14:58:38 -0000	1.2
+++ testchoices.IntChoiceFromSet.properties	11 Oct 2005 23:56:13 -0000	1.3
@@ -12,30 +12,57 @@
 
 yTest.class = gov.nasa.jpf.jvm.choice.IntChoiceFromSet
 
-yTest.values = 3, 2, 1
+yTest.values = 3, x, z, IntChoices.FIFTY
 
 # expected output:
 	
-#	x is 1
-#	y is 3
-#	program end
-#	y is 2
-#	program end
-# 	y is 1
-#	program end
-#	x is 2
-#	y is 3
-#	program end
-#	y is 2
-#	program end
-# 	y is 1
-#	program end
-#	x is 3
-#	y is 3
-#	program end
-#	y is 2
-#	program end
-# 	y is 1
-#	program end
-	
+#Choice: xTest = 0(0)
+#x is 0
+#Choice: yTest = 3(3)
+#y is 3
+#program end
+#Choice: yTest = x(0)
+#y is 0
+#program end
+#Choice: yTest = z(22)
+#y is 22
+#program end
+#Choice: yTest = IntChoices.FIFTY(50)
+#y is 50
+#program end
+#Choice: xTest = 1(1)
+#x is 1
+#Choice: yTest = 3(3)
+#y is 3
+#program end
+#Choice: yTest = x(1)
+#y is 1
+#program end
+#Choice: yTest = z(22)
+#y is 22
+#program end
+#Choice: yTest = IntChoices.FIFTY(50)
+#y is 50
+#program end
+#Choice: xTest = 2(2)
+#x is 2
+#Choice: yTest = 3(3)
+#y is 3
+#program end
+#Choice: yTest = x(2)
+#y is 2
+#program end
+#Choice: yTest = z(22)
+#y is 22
+#program end
+#Choice: yTest = IntChoices.FIFTY(50)
+#y is 50
+#program end
+#------------------------------------ thread stacks
+#Thread: main
+#	at IntChoices.<clinit>(IntChoices.java:36)
+#	at IntChoices.main(IntChoices.java:52)
+#
+#------------------------------------ end thread stacks
+
 	

[Javapathfinder-devel] /javapathfinder/src/gov/nasa/jpf/jvm/choice IntChoiceFromSet.java,1.5,1.6

[John P. <joh...@us...>]

Update of /cvsroot/javapathfinder//javapathfinder/src/gov/nasa/jpf/jvm/choice
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv25225/src/gov/nasa/jpf/jvm/choice

Modified Files:
	IntChoiceFromSet.java 
Log Message:
* can now specify ints as: literals, local, static or other-class static:
x.class = IntChoiceFromSet
x.values = 1, _local_x, field_x, staticfield_x, OtherClass.x

Index: IntChoiceFromSet.java
===================================================================
RCS file: /cvsroot/javapathfinder//javapathfinder/src/gov/nasa/jpf/jvm/choice/IntChoiceFromSet.java,v
retrieving revision 1.5
retrieving revision 1.6
diff -u -d -r1.5 -r1.6
--- IntChoiceFromSet.java	6 Oct 2005 23:27:51 -0000	1.5
+++ IntChoiceFromSet.java	11 Oct 2005 23:52:07 -0000	1.6
@@ -71,7 +71,7 @@
 	      	// split out class name and variable name
 			String[] varId = values[count].split("[.]+");
 			
-			switch (values.length){
+			switch (varId.length){
 			case 1: { // variable name
 				ThreadInfo ti = vm.getSystemState().getRunningThread();
 				try {
@@ -80,14 +80,24 @@
 					// the name is not found...
 				}
 				catch (JPFException e){ //not local? try a field!
-					ElementInfo ei = DynamicArea.getHeap().get(ti.getThis());
-					ret = ei.getIntField(varId[0],null);
+					int id = ti.getThis();
+					if(id>=0){  // in a normal (non-static) method
+					  ElementInfo ei = DynamicArea.getHeap().get(id);
+					  ret = ei.getIntField(varId[0]);
+					}
+					else { // static method (no this)- must be static var
+				      ClassInfo ci = ti.getMethod().getClassInfo();
+				      StaticElementInfo ei = vm.getKernelState().sa.get(ci.getName());
+				      ret = ei.getIntField(varId[0]);
+					}
 				}
+				break;
 			}
 			case 2: { // static variable name TODO other cases here...
 				ClassInfo ci = ClassInfo.getClassInfo(varId[0]);
 				StaticElementInfo ei = vm.getKernelState().sa.get(ci.getName());
-				ret = ei.getIntField(varId[1], null);
+				ret = ei.getIntField(varId[1]);
+				break;
 			}
 			default: 
 		        throw new JPFException("Choice value format error for <" + id +">: parsing \"" + values[count] +"\"");

[Javapathfinder-devel] javapathfinder jpf.properties,1.5,1.6

[pcm <pcm...@us...>]

Update of /cvsroot/javapathfinder/javapathfinder
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv2829

Modified Files:
	jpf.properties 
Log Message:
removed the Md5StateSet and <sigh> it's accompanying util/Md5Set. Say
'good bye' to Owen's programming pearl - it served us well. Maybe somebody
finds a use someday so that we can re-introduce it


Index: jpf.properties
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/jpf.properties,v
retrieving revision 1.5
retrieving revision 1.6
diff -u -d -r1.5 -r1.6
--- jpf.properties	6 Oct 2005 21:59:59 -0000	1.5
+++ jpf.properties	7 Oct 2005 21:43:23 -0000	1.6
@@ -5,8 +5,8 @@
 
 # where are your apps? You can set this here to include your standard dirs
 # (don't forget to set sourcepath accordingly if you want error traces)
-#vm.classpath = /Users/pcmehlitz/tmp
-#vm.sourcepath = ${vm.classpath}
+vm.classpath = /Users/pcmehlitz/tmp
+vm.sourcepath = ${vm.classpath}
 
 
 # search.class = gov.nasa.jpf.search.heuristic.HeuristicSearch

[Javapathfinder-devel] javapathfinder/src/gov/nasa/jpf/util Md5Set.java,1.1.1.1,NONE

[pcm <pcm...@us...>]

Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/util
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv2829/src/gov/nasa/jpf/util

Removed Files:
	Md5Set.java 
Log Message:
removed the Md5StateSet and <sigh> it's accompanying util/Md5Set. Say
'good bye' to Owen's programming pearl - it served us well. Maybe somebody
finds a use someday so that we can re-introduce it


--- Md5Set.java DELETED ---

[Javapathfinder-devel] javapathfinder/test/gov/nasa/jpf/embedded TestVMListener.java,1.1.1.1,1.2

[pcm <pcm...@us...>]

Update of /cvsroot/javapathfinder/javapathfinder/test/gov/nasa/jpf/embedded
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv2829/test/gov/nasa/jpf/embedded

Modified Files:
	TestVMListener.java 
Log Message:
removed the Md5StateSet and <sigh> it's accompanying util/Md5Set. Say
'good bye' to Owen's programming pearl - it served us well. Maybe somebody
finds a use someday so that we can re-introduce it


Index: TestVMListener.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/test/gov/nasa/jpf/embedded/TestVMListener.java,v
retrieving revision 1.1.1.1
retrieving revision 1.2
diff -u -d -r1.1.1.1 -r1.2
--- TestVMListener.java	26 Apr 2005 19:44:24 -0000	1.1.1.1
+++ TestVMListener.java	7 Oct 2005 21:43:23 -0000	1.2
@@ -58,6 +58,42 @@
   public void exceptionThrown(VM vm) {
     // TODO
   }
+
+  public void threadWaiting (VM vm) {
+    // TODO
+  }
+
+  public void threadNotified (VM vm) {
+    // TODO
+  }
+
+  public void threadInterrupted (VM vm) {
+    // TODO
+  }
+
+  public void threadScheduled (VM vm) {
+    // TODO
+  }
+
+  public void objectLocked (VM vm) {
+    // TODO
+  }
+
+  public void objectUnlocked (VM vm) {
+    // TODO
+  }
+
+  public void objectWait (VM vm) {
+    // TODO
+  }
+
+  public void objectNotify (VM vm) {
+    // TODO
+  }
+
+  public void objectNotifyAll (VM vm) {
+    // TODO
+  }
   
   /**
    * new object was created

[Javapathfinder-devel] javapathfinder/src/gov/nasa/jpf/jvm Md5StateSet.java,1.1.1.1,NONE

[pcm <pcm...@us...>]

Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv2829/src/gov/nasa/jpf/jvm

Removed Files:
	Md5StateSet.java 
Log Message:
removed the Md5StateSet and <sigh> it's accompanying util/Md5Set. Say
'good bye' to Owen's programming pearl - it served us well. Maybe somebody
finds a use someday so that we can re-introduce it


--- Md5StateSet.java DELETED ---

[Javapathfinder-devel] javapathfinder/src/gov/nasa/jpf/jvm ElementInfo.java,1.2,1.3 IsEndStateProperty.java,1.1.1.1,1.2 JVM.java,1.11,1.12 NoAssertionViolatedProperty.java,1.1.1.1,1.2 NoUncaughtExceptionsProperty.java,1.1.1.1,1.2 NotDeadlockedProperty.java,1.1.1.1,1.2 Step.java,1.3,1.4 ThreadInfo.java,1.11,1.12

[pcm <pcm...@us...>]

Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv31984/src/gov/nasa/jpf/jvm

Modified Files:
	ElementInfo.java IsEndStateProperty.java JVM.java 
	NoAssertionViolatedProperty.java 
	NoUncaughtExceptionsProperty.java NotDeadlockedProperty.java 
	Step.java ThreadInfo.java 
Log Message:
(1) extended the VMListener interface to include (almost) everything that's
required to observe locks,signals and thread status changes. While it would have
been possibel to do this with instructionExecuted, this requires a lot more
internal JPF knowledge (and code duplication among listeners)

(2) moved the remaining tools from being explicit VMListeners to
extending ListenerAdapter / PropertyListenerAdapter so that future
listener interface changes are less pain

(3) fixed a little annoyance with reporting transitions that only contain
missing sources

(4) changed the Property interface to check(search,vm), the confusing
Object arg is gone (it was null anyways)


Index: IsEndStateProperty.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/IsEndStateProperty.java,v
retrieving revision 1.1.1.1
retrieving revision 1.2
diff -u -d -r1.1.1.1 -r1.2
--- IsEndStateProperty.java	26 Apr 2005 19:44:01 -0000	1.1.1.1
+++ IsEndStateProperty.java	7 Oct 2005 21:27:34 -0000	1.2
@@ -19,6 +19,7 @@
 package gov.nasa.jpf.jvm;
 
 import gov.nasa.jpf.GenericProperty;
+import gov.nasa.jpf.Search;
 import gov.nasa.jpf.VM;
 
 
@@ -30,7 +31,7 @@
     return "End State Reached";
   }
 
-  public boolean check (VM vm, Object arg) {
+  public boolean check (Search search, VM vm) {
     return ((JVM) vm).isEndState();
   }
 }
\ No newline at end of file

Index: ThreadInfo.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/ThreadInfo.java,v
retrieving revision 1.11
retrieving revision 1.12
diff -u -d -r1.11 -r1.12
--- ThreadInfo.java	6 Oct 2005 21:05:53 -0000	1.11
+++ ThreadInfo.java	7 Oct 2005 21:27:34 -0000	1.12
@@ -992,12 +992,25 @@
   public void setStatus (int s) {
     if (threadData.status != s) {
       
-      if ((s == RUNNING) || (s == SYNC_RUNNING)) {
-        JVM.getVM().notifyThreadStarted(this);
-      } else if (s == TERMINATED) {
-        JVM.getVM().notifyThreadTerminated(this);
+      switch (s) {
+      case RUNNING:
+      case SYNC_RUNNING:
+        vm.notifyThreadStarted(this);
+        break;
+      case TERMINATED:
+        vm.notifyThreadTerminated(this);
+        break;
+      case WAITING:
+        vm.notifyThreadWaiting(this);
+        break;
+      case INTERRUPTED:
+        vm.notifyThreadInterrupted(this);
+        break;
+      case NOTIFIED:
+        vm.notifyThreadNotified(this);
+        break;
       }
-      
+              
       threadDataClone().status = s;
     }
   }
@@ -1168,10 +1181,12 @@
   
   void addLockedObject (ElementInfo ei) {
     lockedObjects.add(ei);
+    vm.notifyObjectLocked(this, ei);
   }
   
   void removeLockedObject (ElementInfo ei) {
     lockedObjects.remove(ei);
+    vm.notifyObjectUnlocked(this, ei);
   }
   
   /**
@@ -1540,7 +1555,11 @@
    * @return false if intermediate step (due to Nondeterminism or Buchi observable)
    */
   public boolean executeStep () throws JPFException {
-    current = this;
+    
+    if (current != this) {
+      vm.notifyThreadScheduled(this);
+      current = this;
+    }
     
     if (porInEffect) {
       return executePorStep();

Index: ElementInfo.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/ElementInfo.java,v
retrieving revision 1.2
retrieving revision 1.3
diff -u -d -r1.2 -r1.3
--- ElementInfo.java	29 Jul 2005 21:02:26 -0000	1.2
+++ ElementInfo.java	7 Oct 2005 21:27:34 -0000	1.3
@@ -793,7 +793,7 @@
       th.addLockedObject(this);
     }
   }
-
+  
   public void lockNotified(ThreadInfo th) {
     cloneMonitor().lockNotified(th, getRef());
 
@@ -804,6 +804,14 @@
     th.addLockedObject(this); //wv: add locked object back here
   }
 
+  public void unlock(ThreadInfo th) {
+    cloneMonitor().unlock(th, getRef());
+
+    if (monitor.getLockCount() == 0) {
+      th.removeLockedObject(this);
+    }
+  }
+
   abstract public int getNumberOfFields();
 
   abstract public FieldInfo getFieldInfo(int i);
@@ -828,12 +836,23 @@
     monitor.log();
   }
 
+  public void wait(ThreadInfo th) {
+    cloneMonitor().wait(th, getRef());
+    th.removeLockedObject(this); //wv: remove locked object here
+    
+    JVM.getVM().notifyObjectWait(th, this);
+  }
+
   public void notifies() {
     cloneMonitor().notify(area.ks.ss);
+
+    JVM.getVM().notifyObjectNotifies(ThreadInfo.current, this);
   }
 
   public void notifiesAll() {
     cloneMonitor().notifyAll(area.ks.ss);
+
+    JVM.getVM().notifyObjectNotifiesAll(ThreadInfo.current, this);
   }
 
   public boolean outOfBounds(int index) {
@@ -869,18 +888,6 @@
     return 3;
   }
 
-  public void unlock(ThreadInfo th) {
-    cloneMonitor().unlock(th, getRef());
-
-    if (monitor.getLockCount() == 0) {
-      th.removeLockedObject(this);
-    }
-  }
-
-  public void wait(ThreadInfo th) {
-    cloneMonitor().wait(th, getRef());
-    th.removeLockedObject(this); //wv: remove locked object here
-  }
 
   protected void setFieldsIndex(int index) {
     if (fIndex == index) {

Index: NotDeadlockedProperty.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/NotDeadlockedProperty.java,v
retrieving revision 1.1.1.1
retrieving revision 1.2
diff -u -d -r1.1.1.1 -r1.2
--- NotDeadlockedProperty.java	26 Apr 2005 19:44:04 -0000	1.1.1.1
+++ NotDeadlockedProperty.java	7 Oct 2005 21:27:34 -0000	1.2
@@ -20,6 +20,7 @@
 
 import gov.nasa.jpf.Config;
 import gov.nasa.jpf.GenericProperty;
+import gov.nasa.jpf.Search;
 import gov.nasa.jpf.VM;
 
 /**
@@ -33,7 +34,7 @@
     return "Deadlock";
   }
 
-  public boolean check (VM vm, Object arg) {
+  public boolean check (Search search, VM vm) {
     return !((JVM) vm).isDeadlocked();
   }
 }
\ No newline at end of file

Index: Step.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/Step.java,v
retrieving revision 1.3
retrieving revision 1.4
diff -u -d -r1.3 -r1.4
--- Step.java	6 Oct 2005 21:05:53 -0000	1.3
+++ Step.java	7 Oct 2005 21:27:34 -0000	1.4
@@ -90,6 +90,14 @@
   public String getComment () {
     return comment;
   }
+
+  void printMissingPlaceholderOn (PrintWriter pw, String prefix) {
+    pw.print( (prefix != null) ? prefix : "  ");
+    for (; nMissing > 0; nMissing--) {
+      pw.print('.');
+    }
+    pw.println();    
+  }
   
   public void printStepOn (PrintWriter pw, SourceRef lastPrinted, String prefix) {
     Source source = Source.getSource(fileName);
@@ -104,14 +112,13 @@
           pw.println(']');          
         } else {
           nMissing++;
+          if (next == null) {
+            printMissingPlaceholderOn(pw,prefix);
+          }
         }
       } else {
         if (nMissing > 0) {
-          pw.print( (prefix != null) ? prefix : "  ");
-          for (; nMissing > 0; nMissing--) {
-            pw.print('.');
-          }
-          pw.println();
+          printMissingPlaceholderOn(pw,prefix);
         }
         
         pw.print( (prefix != null) ? prefix : "  ");

Index: NoUncaughtExceptionsProperty.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/NoUncaughtExceptionsProperty.java,v
retrieving revision 1.1.1.1
retrieving revision 1.2
diff -u -d -r1.1.1.1 -r1.2
--- NoUncaughtExceptionsProperty.java	26 Apr 2005 19:44:04 -0000	1.1.1.1
+++ NoUncaughtExceptionsProperty.java	7 Oct 2005 21:27:34 -0000	1.2
@@ -20,6 +20,7 @@
 
 import gov.nasa.jpf.Config;
 import gov.nasa.jpf.GenericProperty;
+import gov.nasa.jpf.Search;
 import gov.nasa.jpf.VM;
 
 import java.io.PrintWriter;
@@ -45,7 +46,7 @@
     return "uncaught exception";
   }
 
-  public boolean check (VM vm, Object arg) {
+  public boolean check (Search search, VM vm) {
     return (uncaughtXi == null);
   }
 

Index: JVM.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/JVM.java,v
retrieving revision 1.11
retrieving revision 1.12
diff -u -d -r1.11 -r1.12
--- JVM.java	6 Oct 2005 21:05:53 -0000	1.11
+++ JVM.java	7 Oct 2005 21:27:34 -0000	1.12
@@ -329,57 +329,153 @@
   }
   
   void notifyInstructionExecuted (ThreadInfo ti, Instruction insn, Instruction nextInsn) {
-    lastThreadInfo = ti;
-    lastInstruction = insn;
-    nextInstruction = nextInsn;
     if (listener != null) {
+      lastThreadInfo = ti;
+      lastInstruction = insn;
+      nextInstruction = nextInsn;
+
       listener.instructionExecuted(this);
+
+      nextInstruction = null;
+      lastInstruction = null;
+      lastThreadInfo = null;
     }
-    nextInstruction = null;
-    lastInstruction = null;
-    lastThreadInfo = null;
   }
   
   void notifyThreadStarted (ThreadInfo ti) {
-    lastThreadInfo = ti;
     if (listener != null) {
+      lastThreadInfo = ti;
       listener.threadStarted(this);
+      lastThreadInfo = null;
     }
-    lastThreadInfo = null;
   }
-  
+
+  void notifyThreadWaiting (ThreadInfo ti) {
+    if (listener != null) {
+      lastThreadInfo = ti;
+      listener.threadWaiting(this);
+      lastThreadInfo = null;
+    }
+  }
+
+  void notifyThreadNotified (ThreadInfo ti) {
+    if (listener != null) {
+      lastThreadInfo = ti;
+      listener.threadNotified(this);
+      lastThreadInfo = null;
+    }
+  }
+
+  void notifyThreadInterrupted (ThreadInfo ti) {
+    if (listener != null) {
+      lastThreadInfo = ti;
+      listener.threadInterrupted(this);
+      lastThreadInfo = null;
+    }
+  }
+
   void notifyThreadTerminated (ThreadInfo ti) {
-    lastThreadInfo = ti;
     if (listener != null) {
+      lastThreadInfo = ti;
       listener.threadTerminated(this);
+      lastThreadInfo = null;
+    }
+  }
+
+  void notifyThreadScheduled (ThreadInfo ti) {
+    if (listener != null) {
+      lastThreadInfo = ti;
+      listener.threadScheduled(this);
+      lastThreadInfo = null;
     }
-    lastThreadInfo = null;
   }
   
   void notifyClassLoaded (ClassInfo ci) {
-    lastClassInfo = ci;
     if (listener != null) {
+      lastClassInfo = ci;
       listener.classLoaded(this);
+      lastClassInfo = null;
     }
-    lastClassInfo = null;
   }
   
   void notifyObjectCreated (ThreadInfo ti, ElementInfo ei) {
-    lastThreadInfo = ti;
-    lastElementInfo = ei;
     if (listener != null) {
+      lastThreadInfo = ti;
+      lastElementInfo = ei;
+
       listener.objectCreated(this);
+
+      lastElementInfo = null;
+      lastThreadInfo = null;
     }
-    lastElementInfo = null;
-    lastThreadInfo = null;
   }
   
   void notifyObjectReleased (ElementInfo ei) {
-    lastElementInfo = ei;
     if (listener != null) {
+      lastElementInfo = ei;
       listener.objectReleased(this);
+      lastElementInfo = null;
+    }
+  }
+  
+  void notifyObjectLocked (ThreadInfo ti, ElementInfo ei){
+    if (listener != null) {
+      lastThreadInfo = ti;
+      lastElementInfo = ei;
+      
+      listener.objectLocked(this);
+
+      lastElementInfo = null;
+      lastThreadInfo = null;
+    }
+  }
+  
+  void notifyObjectUnlocked (ThreadInfo ti, ElementInfo ei) {
+    if (listener != null) {
+      lastThreadInfo = ti;
+      lastElementInfo = ei;
+      
+      listener.objectUnlocked(this);
+
+      lastElementInfo = null;
+      lastThreadInfo = null;
+    }
+  }
+  
+  void notifyObjectWait (ThreadInfo ti, ElementInfo ei) {
+    if (listener != null) {
+      lastThreadInfo = ti;
+      lastElementInfo = ei;
+      
+      listener.objectWait(this);
+
+      lastElementInfo = null;
+      lastThreadInfo = null;
+    }
+  }
+  
+  void notifyObjectNotifies (ThreadInfo ti, ElementInfo ei) {
+    if (listener != null) {
+      lastThreadInfo = ti;
+      lastElementInfo = ei;
+      
+      listener.objectNotify(this);
+
+      lastElementInfo = null;
+      lastThreadInfo = null;
+    }
+  }
+
+  void notifyObjectNotifiesAll (ThreadInfo ti, ElementInfo ei) {
+    if (listener != null) {
+      lastThreadInfo = ti;
+      lastElementInfo = ei;
+      
+      listener.objectNotifyAll(this);
+
+      lastElementInfo = null;
+      lastThreadInfo = null;
     }
-    lastElementInfo = null;
   }
   
   void notifyGCBegin () {
@@ -395,13 +491,15 @@
   }
   
   void notifyExceptionThrown (ThreadInfo ti, ElementInfo ei) {
-    lastThreadInfo = ti;
-    lastElementInfo = ei;
     if (listener != null) {
+      lastThreadInfo = ti;
+      lastElementInfo = ei;
+
       listener.exceptionThrown(this);
+      
+      lastElementInfo = null;
+      lastThreadInfo = null;
     }
-    lastElementInfo = null;
-    lastThreadInfo = null;
   }
   
   // VMListener acquisition

Index: NoAssertionViolatedProperty.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/NoAssertionViolatedProperty.java,v
retrieving revision 1.1.1.1
retrieving revision 1.2
diff -u -d -r1.1.1.1 -r1.2
--- NoAssertionViolatedProperty.java	26 Apr 2005 19:44:04 -0000	1.1.1.1
+++ NoAssertionViolatedProperty.java	7 Oct 2005 21:27:34 -0000	1.2
@@ -20,6 +20,7 @@
 
 import gov.nasa.jpf.Config;
 import gov.nasa.jpf.GenericProperty;
+import gov.nasa.jpf.Search;
 import gov.nasa.jpf.VM;
 
 /**
@@ -33,7 +34,7 @@
     return "Assertion Violated";
   }
 
-  public boolean check (VM vm, Object arg) {
+  public boolean check (Search search, VM vm) {
     return !((JVM) vm).ss.violatedAssertion;
   }
 }
\ No newline at end of file

[Javapathfinder-devel] javapathfinder/src/gov/nasa/jpf/tools ExecTracker.java,1.1.1.1,1.2 HeapTracker.java,1.2,1.3 InsnCounter.java,1.1.1.1,1.2 RaceDetector.java,1.4,1.5 VarTracker.java,1.1.1.1,1.2

[pcm <pcm...@us...>]

Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/tools
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv31984/src/gov/nasa/jpf/tools

Modified Files:
	ExecTracker.java HeapTracker.java InsnCounter.java 
	RaceDetector.java VarTracker.java 
Log Message:
(1) extended the VMListener interface to include (almost) everything that's
required to observe locks,signals and thread status changes. While it would have
been possibel to do this with instructionExecuted, this requires a lot more
internal JPF knowledge (and code duplication among listeners)

(2) moved the remaining tools from being explicit VMListeners to
extending ListenerAdapter / PropertyListenerAdapter so that future
listener interface changes are less pain

(3) fixed a little annoyance with reporting transitions that only contain
missing sources

(4) changed the Property interface to check(search,vm), the confusing
Object arg is gone (it was null anyways)


Index: RaceDetector.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/tools/RaceDetector.java,v
retrieving revision 1.4
retrieving revision 1.5
diff -u -d -r1.4 -r1.5
--- RaceDetector.java	5 Oct 2005 06:17:07 -0000	1.4
+++ RaceDetector.java	7 Oct 2005 21:27:34 -0000	1.5
@@ -208,7 +208,7 @@
   
   /*** GenericProperty **************************************************/
   
-  public boolean check(VM vm, Object arg) {
+  public boolean check(Search search, VM vm) {
     return (raceField == null);
   }
   

Index: InsnCounter.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/tools/InsnCounter.java,v
retrieving revision 1.1.1.1
retrieving revision 1.2
diff -u -d -r1.1.1.1 -r1.2
--- InsnCounter.java	26 Apr 2005 19:44:22 -0000	1.1.1.1
+++ InsnCounter.java	7 Oct 2005 21:27:34 -0000	1.2
@@ -18,6 +18,7 @@
 //
 package gov.nasa.jpf.tools;
 
+import gov.nasa.jpf.ListenerAdapter;
 import gov.nasa.jpf.VMListener;
 import gov.nasa.jpf.VM;
 import gov.nasa.jpf.SearchListener;
@@ -31,7 +32,7 @@
  * simple tools to gather statistics about instructions executed by JPF.
  * InsnCounter is mostly a VMListener that observes 'instructionExecuted'
  */
-public class InsnCounter implements VMListener, SearchListener {
+public class InsnCounter extends ListenerAdapter {
 
   String[] opCodes = new String[256];
   int[] counts = new int[256];
@@ -41,30 +42,7 @@
   public void searchFinished(Search search) {
     reportStatistics();
   }
-  
-  public void stateBacktracked(Search search) {
-    // not interested
-  }
-  public void propertyViolated(Search search) {
-    // not interested
-  }
-  public void searchConstraintHit(Search search) {
-    // not interested
-  }
-  public void stateAdvanced(Search search) {
-    // not interested
-  }
-  public void stateProcessed(Search search) {
-    // not interested
-  }
-  public void searchStarted(Search search) {
-    // not interested
-  }
-  public void stateRestored(Search search) {
-    // not interested
-  }
-  
-  
+    
   //----------------------------------------------------- VMListener interface
   public void instructionExecuted(VM vm) {
     JVM jvm = (JVM)vm;
@@ -77,32 +55,7 @@
     counts[bc]++;
     total++;
   }
-  
-  public void threadStarted(VM vm) {
-    // not interested
-  }
-  public void threadTerminated(VM vm) {
-    // not interested
-  }
-  public void objectCreated(VM vm) {
-    // not interested
-  }
-  public void objectReleased(VM vm) {
-    // not interested
-  }
-  public void gcBegin (VM vm) {
-    // not interested
-  }
-  public void gcEnd (VM vm) {
-    // not interested
-  }
-  public void classLoaded(VM vm) {
-    // not interested
-  }
-  public void exceptionThrown(VM vm) {
-    // not interested
-  }
-  
+
   
   //----------------------------------------------------- internal stuff
   void reportStatistics () {

Index: HeapTracker.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/tools/HeapTracker.java,v
retrieving revision 1.2
retrieving revision 1.3
diff -u -d -r1.2 -r1.3
--- HeapTracker.java	25 Aug 2005 17:06:00 -0000	1.2
+++ HeapTracker.java	7 Oct 2005 21:27:34 -0000	1.3
@@ -141,7 +141,7 @@
   /**
    * return 'false' if property is violated
    */
-  public boolean check (VM vm, Object arg) {
+  public boolean check (Search search, VM vm) {
     if (throwOutOfMemory) {
       // in this case we don't want to stop the program, but see if it
       // behaves gracefully - don't report a property violation

Index: VarTracker.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/tools/VarTracker.java,v
retrieving revision 1.1.1.1
retrieving revision 1.2
diff -u -d -r1.1.1.1 -r1.2
--- VarTracker.java	26 Apr 2005 19:44:22 -0000	1.1.1.1
+++ VarTracker.java	7 Oct 2005 21:27:34 -0000	1.2
@@ -19,6 +19,7 @@
 package gov.nasa.jpf.tools;
 
 import gov.nasa.jpf.Config;
+import gov.nasa.jpf.ListenerAdapter;
 import gov.nasa.jpf.VMListener;
 import gov.nasa.jpf.SearchListener;
 import gov.nasa.jpf.VM;
@@ -50,7 +51,7 @@
  * space blows up because of some counter/timer vars, and where to apply the
  * necessary abstractions to close/shrink it
  */
-public class VarTracker implements VMListener, SearchListener {
+public class VarTracker extends ListenerAdapter {
   
   int changeThreshold = 1;
   boolean filterSystemVars = false;
@@ -139,26 +140,11 @@
     queue.clear();
   }
   
-  public void stateBacktracked(Search search) {
-    // nothing to do
-  }
-  
-  public void stateProcessed (Search search) {
-    // nothing to do
-  }
-  
-  public void stateRestored(Search search) {
-    // TODO
-  }
   
   public void propertyViolated(Search search) {
     report("property violated");
   }
-  
-  public void searchStarted(Search search) {
-    // nothing to do
-  }
-  
+    
   public void searchConstraintHit(Search search) {
     report("search constraint hit");
     
@@ -245,37 +231,6 @@
     return true;
   }
   
-  public void threadStarted(VM vm) {
-    // TODO
-  }
-  
-  public void threadTerminated(VM vm) {
-    // TODO
-  }
-  
-  public void classLoaded(VM vm) {
-    // TODO
-  }
-  
-  public void objectCreated(VM vm) {
-    // TODO
-  }
-  
-  public void objectReleased(VM vm) {
-    // TODO
-  }
-  
-  public void gcBegin(VM vm) {
-    // TODO
-  }
-  
-  public void gcEnd(VM vm) {
-    // TODO
-  }
-  
-  public void exceptionThrown(VM vm) {
-    // TODO
-  }
   
   void filterArgs (String[] args) {
     for (int i=0; i<args.length; i++) {

Index: ExecTracker.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/tools/ExecTracker.java,v
retrieving revision 1.1.1.1
retrieving revision 1.2
diff -u -d -r1.1.1.1 -r1.2
--- ExecTracker.java	26 Apr 2005 19:44:20 -0000	1.1.1.1
+++ ExecTracker.java	7 Oct 2005 21:27:34 -0000	1.2
@@ -19,6 +19,7 @@
 package gov.nasa.jpf.tools;
 
 import gov.nasa.jpf.Config;
+import gov.nasa.jpf.ListenerAdapter;
 import gov.nasa.jpf.SearchListener;
 import gov.nasa.jpf.VMListener;
 import gov.nasa.jpf.JPF;
@@ -37,25 +38,19 @@
  * ExecTracker is mostly a VMListener of 'instructionExecuted' and
  * a SearchListener of 'stateAdvanced' and 'statehBacktracked'
  */
-public class ExecTracker implements SearchListener, VMListener {
+public class ExecTracker extends ListenerAdapter {
   /******************************************* SearchListener interface *****/
     
   boolean printLines = false;
   PrintWriter pw;
   SourceRef   lastLine;
   String      linePrefix;
-  
-  public void searchConstraintHit(Search search) {
-  }
-  
+    
   public void stateRestored(Search search) {
     int id = search.getStateNumber();
     System.out.println("--- restored: " + id);
   }
     
-  public void propertyViolated(Search search) {
-  }
-
   //--- the ones we are interested in
   public void searchStarted(Search search) {
     System.out.println("--- search started");
@@ -97,25 +92,11 @@
   }
 
   /******************************************* VMListener interface *********/
-  public void exceptionThrown(VM vm) {
-  }
-    
-  public void classLoaded(VM vm) {
-  }
-
-  public void gcBegin(VM vm) {
-  }
 
   public void gcEnd(VM vm) {
     System.out.println("\t\t\t\t # GC");
   }
 
-  public void objectCreated(VM vm) {
-  }
-
-  public void objectReleased(VM vm) {
-  }
-
   //--- the ones we are interested in
   public void instructionExecuted(VM vm) {
     JVM jvm = (JVM)vm;
@@ -155,7 +136,7 @@
     
     System.out.println( "\t\t\t\t # thread terminated: " + ti.getIndex());
   }
-
+  
   /****************************************** private stuff ******/
 
   void filterArgs (String[] args) {

[Javapathfinder-devel] javapathfinder/src/gov/nasa/jpf GenericProperty.java,1.1.1.1,1.2 ListenerAdapter.java,1.2,1.3 Property.java,1.1.1.1,1.2 PropertyListenerAdapter.java,1.1,1.2 VMListener.java,1.1.1.1,1.2 VMListenerMulticaster.java,1.1.1.1,1.2

[pcm <pcm...@us...>]

Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv31984/src/gov/nasa/jpf

Modified Files:
	GenericProperty.java ListenerAdapter.java Property.java 
	PropertyListenerAdapter.java VMListener.java 
	VMListenerMulticaster.java 
Log Message:
(1) extended the VMListener interface to include (almost) everything that's
required to observe locks,signals and thread status changes. While it would have
been possibel to do this with instructionExecuted, this requires a lot more
internal JPF knowledge (and code duplication among listeners)

(2) moved the remaining tools from being explicit VMListeners to
extending ListenerAdapter / PropertyListenerAdapter so that future
listener interface changes are less pain

(3) fixed a little annoyance with reporting transitions that only contain
missing sources

(4) changed the Property interface to check(search,vm), the confusing
Object arg is gone (it was null anyways)


Index: PropertyListenerAdapter.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/PropertyListenerAdapter.java,v
retrieving revision 1.1
retrieving revision 1.2
diff -u -d -r1.1 -r1.2
--- PropertyListenerAdapter.java	25 Aug 2005 16:59:17 -0000	1.1
+++ PropertyListenerAdapter.java	7 Oct 2005 21:27:34 -0000	1.2
@@ -31,7 +31,7 @@
 public class PropertyListenerAdapter extends GenericProperty implements
     SearchListener, VMListener {
 
-  public boolean check(VM vm, Object arg) {
+  public boolean check(Search search, VM vm) {
     return true;
   }
 
@@ -87,4 +87,31 @@
   public void exceptionThrown(VM vm) {
   }
 
+  public void threadWaiting (VM vm) {
+  }
+
+  public void threadNotified (VM vm) {
+  }
+
+  public void threadInterrupted (VM vm) {
+  }
+
+  public void threadScheduled (VM vm) {
+  }
+  
+  public void objectLocked (VM vm) {
+  }
+
+  public void objectUnlocked (VM vm) {
+  }
+
+  public void objectWait (VM vm) {
+  }
+
+  public void objectNotify (VM vm) {
+  }
+
+  public void objectNotifyAll (VM vm) {
+  }
+
 }

Index: GenericProperty.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/GenericProperty.java,v
retrieving revision 1.1.1.1
retrieving revision 1.2
diff -u -d -r1.1.1.1 -r1.2
--- GenericProperty.java	26 Apr 2005 19:43:55 -0000	1.1.1.1
+++ GenericProperty.java	7 Oct 2005 21:27:34 -0000	1.2
@@ -26,7 +26,7 @@
  * the check itself has to be provided
  */
 public abstract class GenericProperty implements Property {
-  public abstract boolean check (VM vm, Object arg);
+  public abstract boolean check (Search search, VM vm);
 
   protected GenericProperty () {
     // nothing yet

Index: ListenerAdapter.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/ListenerAdapter.java,v
retrieving revision 1.2
retrieving revision 1.3
diff -u -d -r1.2 -r1.3
--- ListenerAdapter.java	6 Sep 2005 21:21:08 -0000	1.2
+++ ListenerAdapter.java	7 Oct 2005 21:27:34 -0000	1.3
@@ -37,6 +37,18 @@
   public void threadStarted(VM vm) {
   }
 
+  public void threadWaiting (VM vm) {
+  }
+
+  public void threadNotified (VM vm) {
+  }
+
+  public void threadInterrupted (VM vm) {
+  }
+
+  public void threadScheduled (VM vm) {
+  }
+
   /* (non-Javadoc)
    * @see gov.nasa.jpf.VMListener#threadTerminated(gov.nasa.jpf.VM)
    */
@@ -61,6 +73,21 @@
   public void objectReleased(VM vm) {
   }
 
+  public void objectLocked (VM vm) {
+  }
+
+  public void objectUnlocked (VM vm) {
+  }
+
+  public void objectWait (VM vm) {
+  }
+
+  public void objectNotify (VM vm) {
+  }
+
+  public void objectNotifyAll (VM vm) {
+  }
+
   /* (non-Javadoc)
    * @see gov.nasa.jpf.VMListener#gcBegin(gov.nasa.jpf.VM)
    */

Index: VMListenerMulticaster.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/VMListenerMulticaster.java,v
retrieving revision 1.1.1.1
retrieving revision 1.2
diff -u -d -r1.1.1.1 -r1.2
--- VMListenerMulticaster.java	26 Apr 2005 19:43:56 -0000	1.1.1.1
+++ VMListenerMulticaster.java	7 Oct 2005 21:27:34 -0000	1.2
@@ -92,10 +92,30 @@
     tail.threadStarted(vm);
   }
 
+  public void threadWaiting (VM vm) {
+    head.threadWaiting(vm);
+    tail.threadWaiting(vm);    
+  }
+
+  public void threadNotified (VM vm) {
+    head.threadNotified(vm);
+    tail.threadNotified(vm);    
+  }
+
+  public void threadInterrupted (VM vm) {
+    head.threadInterrupted(vm);
+    tail.threadInterrupted(vm);    
+  }
+
   public void threadTerminated (VM vm) {
     head.threadTerminated(vm);
     tail.threadTerminated(vm);
   }
+
+  public void threadScheduled (VM vm) {
+    head.threadScheduled(vm);
+    tail.threadScheduled(vm);
+  }
   
   public void classLoaded (VM vm) {
     head.classLoaded(vm);
@@ -126,6 +146,31 @@
     head.exceptionThrown(vm);
     tail.exceptionThrown(vm);
   }
-  
+
+  public void objectLocked (VM vm) {
+    head.objectLocked(vm);
+    tail.objectLocked(vm); 
+  }
+
+  public void objectUnlocked (VM vm) {
+    head.objectUnlocked(vm);
+    tail.objectUnlocked(vm);    
+  }
+
+  public void objectWait (VM vm) {
+    head.objectWait(vm);
+    tail.objectWait(vm);
+  }
+
+  public void objectNotify (VM vm) {
+    head.objectNotify(vm);
+    tail.objectNotify(vm);    
+  }
+
+  public void objectNotifyAll (VM vm) {
+    head.objectNotifyAll(vm);
+    tail.objectNotifyAll(vm);    
+  }
+
 }
 

Index: VMListener.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/VMListener.java,v
retrieving revision 1.1.1.1
retrieving revision 1.2
diff -u -d -r1.1.1.1 -r1.2
--- VMListener.java	26 Apr 2005 19:43:56 -0000	1.1.1.1
+++ VMListener.java	7 Oct 2005 21:27:34 -0000	1.2
@@ -34,12 +34,32 @@
    * new Thread entered run() method
    */
   void threadStarted (VM vm);
+    
+  /**
+   * thread is waiting for signal
+   */
+  void threadWaiting (VM vm);
+
+  /**
+   * thread got notified
+   */
+  void threadNotified (VM vm);
+    
+  /**
+   * thread got interrupted
+   */
+  void threadInterrupted (VM vm);
   
   /**
    * Thread exited run() method
    */
   void threadTerminated (VM vm);
-  
+
+  /**
+   * new thread was scheduled by VM
+   */
+  void threadScheduled (VM vm); // this might go into the choice generator notifications
+
   /**
    * new class was loaded
    */
@@ -55,6 +75,33 @@
    */
   void objectReleased (VM vm);
   
+  /**
+   * notify if an object lock was taken (this includes automatic
+   * surrender during a wait())
+   */
+  void objectLocked (VM vm);
+  
+  /**
+   * notify if an object lock was released (this includes automatic
+   * reacquisition after a notify())
+   */
+  void objectUnlocked (VM vm);
+  
+  /**
+   * notify if a wait() is executed
+   */
+  void objectWait (VM vm);
+  
+  /**
+   * notify if an object notifies a single waiter
+   */
+  void objectNotify (VM vm);
+
+  /**
+   * notify if an object notifies all waiters
+   */
+  void objectNotifyAll (VM vm);
+  
   void gcBegin (VM vm);
   
   void gcEnd (VM vm);

Index: Property.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/Property.java,v
retrieving revision 1.1.1.1
retrieving revision 1.2
diff -u -d -r1.1.1.1 -r1.2
--- Property.java	26 Apr 2005 19:43:56 -0000	1.1.1.1
+++ Property.java	7 Oct 2005 21:27:34 -0000	1.2
@@ -26,7 +26,7 @@
  * properties have been violated (e.g. NoUncaughtExceptions)
  */
 public interface Property extends Printable {
-  boolean check (VM vm, Object arg);
+  boolean check (Search search, VM vm);
 
   String getErrorMessage ();
 }
\ No newline at end of file

[Javapathfinder-devel] javapathfinder/src/gov/nasa/jpf/search AbstractSearch.java,1.1.1.1,1.2 PropertyMulticaster.java,1.1.1.1,1.2

[pcm <pcm...@us...>]

Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/search
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv31984/src/gov/nasa/jpf/search

Modified Files:
	AbstractSearch.java PropertyMulticaster.java 
Log Message:
(1) extended the VMListener interface to include (almost) everything that's
required to observe locks,signals and thread status changes. While it would have
been possibel to do this with instructionExecuted, this requires a lot more
internal JPF knowledge (and code duplication among listeners)

(2) moved the remaining tools from being explicit VMListeners to
extending ListenerAdapter / PropertyListenerAdapter so that future
listener interface changes are less pain

(3) fixed a little annoyance with reporting transitions that only contain
missing sources

(4) changed the Property interface to check(search,vm), the confusing
Object arg is gone (it was null anyways)


Index: PropertyMulticaster.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/search/PropertyMulticaster.java,v
retrieving revision 1.1.1.1
retrieving revision 1.2
diff -u -d -r1.1.1.1 -r1.2
--- PropertyMulticaster.java	26 Apr 2005 19:44:19 -0000	1.1.1.1
+++ PropertyMulticaster.java	7 Oct 2005 21:27:34 -0000	1.2
@@ -19,6 +19,7 @@
 package gov.nasa.jpf.search;
 
 import gov.nasa.jpf.Property;
+import gov.nasa.jpf.Search;
 import gov.nasa.jpf.VM;
 
 import java.io.PrintWriter;
@@ -82,12 +83,12 @@
     tail = t;
   }
   
-  public boolean check (VM vm, Object arg) {
-    if (!head.check(vm,arg)){
+  public boolean check (Search search, VM vm) {
+    if (!head.check(search, vm)){
       headFailed = true;
       return false;
     }
-    if (!tail.check(vm,arg)){
+    if (!tail.check(search, vm)){
       tailFailed = true;
       return false;
     }

Index: AbstractSearch.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/search/AbstractSearch.java,v
retrieving revision 1.1.1.1
retrieving revision 1.2
diff -u -d -r1.1.1.1 -r1.2
--- AbstractSearch.java	26 Apr 2005 19:44:16 -0000	1.1.1.1
+++ AbstractSearch.java	7 Oct 2005 21:27:34 -0000	1.2
@@ -133,7 +133,7 @@
   }
   
   boolean isPropertyViolated () {
-    if ((property != null) && !property.check(vm, null)) {
+    if ((property != null) && !property.check(this, vm)) {
       error(property, vm.getPath());
       return true;
     }

[Javapathfinder-devel] javapathfinder/bin jpf.bat,1.4,1.5

[Masoud Mansouri-S. <mas...@us...>]

Update of /cvsroot/javapathfinder/javapathfinder/bin
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv8981/bin

Modified Files:
	jpf.bat 
Log Message:
* Minor change. No longer displaying the following at the begining of
   every run:

  REM
  REM overly simplified batch file to start JPF from a command prompt
  REM
  ...

Index: jpf.bat
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/bin/jpf.bat,v
retrieving revision 1.4
retrieving revision 1.5
diff -u -d -r1.4 -r1.5
--- jpf.bat	16 May 2005 18:15:47 -0000	1.4
+++ jpf.bat	7 Oct 2005 18:51:52 -0000	1.5
@@ -1,9 +1,8 @@
+@echo off
 REM
 REM overly simplified batch file to start JPF from a command prompt
 REM
 
-@echo off
-
 REM Set the JPF_HOME directory
 set JPF_HOME=%~dp0..
 

[Javapathfinder-devel] /javapathfinder/src/gov/nasa/jpf/jvm/choice IntChoiceFromSet.java,1.4,1.5

[John P. <joh...@us...>]

Update of /cvsroot/javapathfinder//javapathfinder/src/gov/nasa/jpf/jvm/choice
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv21038/src/gov/nasa/jpf/jvm/choice

Modified Files:
	IntChoiceFromSet.java 
Log Message:
*added comments
*beginning to generalize to specify literals or variable names for values - still works for literals

Index: IntChoiceFromSet.java
===================================================================
RCS file: /cvsroot/javapathfinder//javapathfinder/src/gov/nasa/jpf/jvm/choice/IntChoiceFromSet.java,v
retrieving revision 1.4
retrieving revision 1.5
diff -u -d -r1.4 -r1.5
--- IntChoiceFromSet.java	12 Sep 2005 16:23:20 -0000	1.4
+++ IntChoiceFromSet.java	6 Oct 2005 23:27:51 -0000	1.5
@@ -17,17 +17,16 @@
 //DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
 //
 
-/*
- * Created on Sep 8, 2005
- *
- * TODO To change the template for this generated file go to
- * Window - Preferences - Java - Code Style - Code Templates
- */
 package gov.nasa.jpf.jvm.choice;
 
 import gov.nasa.jpf.Config;
+import gov.nasa.jpf.jvm.ClassInfo;
+import gov.nasa.jpf.jvm.DynamicArea;
+import gov.nasa.jpf.jvm.ElementInfo;
 import gov.nasa.jpf.jvm.IntChoiceGenerator;
 import gov.nasa.jpf.jvm.JVM;
+import gov.nasa.jpf.jvm.StaticElementInfo;
+import gov.nasa.jpf.jvm.ThreadInfo;
 import gov.nasa.jpf.JPFException;
 /**
  * @author jpenix
@@ -47,7 +46,8 @@
 	int count = -1;
 	
 	/**
-	 * @param id
+	 * @param config - JPF configuration object
+	 * @param id - String label used in choice config 
 	 */
 	public IntChoiceFromSet(Config conf, String id) {
 		super(id);
@@ -57,24 +57,50 @@
 		}
 	}
 
-	/* (non-Javadoc)
+	/** 
 	 * @see gov.nasa.jpf.jvm.IntChoiceGenerator#getNextChoice()
-	 */
+	 **/
 	public int getNextChoice(JVM vm) {
 		
+		int ret;
 		try {
-		// watch out this returns 0 if it parses wrong
-		int ret = Integer.parseInt(values[count]); 
-			vm.println(id + ": " + ret);
-	        return ret;
-	      } catch (NumberFormatException nfx) {
-	        throw new JPFException("Number format error for <" + id +">: parsing \"" + values[count] +"\"");
-	      }
+			ret = Integer.parseInt(values[count]); 
+		} 
+		catch (NumberFormatException nfx) {
+	      	
+	      	// split out class name and variable name
+			String[] varId = values[count].split("[.]+");
+			
+			switch (values.length){
+			case 1: { // variable name
+				ThreadInfo ti = vm.getSystemState().getRunningThread();
+				try {
+					ret = ti.getIntLocal(varId[0]);
+					// that throws an exception (a few calls down) if  
+					// the name is not found...
+				}
+				catch (JPFException e){ //not local? try a field!
+					ElementInfo ei = DynamicArea.getHeap().get(ti.getThis());
+					ret = ei.getIntField(varId[0],null);
+				}
+			}
+			case 2: { // static variable name TODO other cases here...
+				ClassInfo ci = ClassInfo.getClassInfo(varId[0]);
+				StaticElementInfo ei = vm.getKernelState().sa.get(ci.getName());
+				ret = ei.getIntField(varId[1], null);
+			}
+			default: 
+		        throw new JPFException("Choice value format error for <" + id +">: parsing \"" + values[count] +"\"");
+			}
+		}
+		// print "Choice: bob = MyClass.ONE(1)"
+		vm.println("Choice: "+id + " = " + values[count] + "("+ret+")");
+		return ret;
 	}
 
-	/* (non-Javadoc)
+	/**
 	 * @see gov.nasa.jpf.jvm.ChoiceGenerator#hasMoreChoices()
-	 */
+	 **/
 	public boolean hasMoreChoices(JVM vm) {
 		if (count < values.length-1)  
 			return true;
@@ -82,11 +108,18 @@
 			return false;
 	}
 
-	/* (non-Javadoc)
+	/**
 	 * @see gov.nasa.jpf.jvm.ChoiceGenerator#advance(gov.nasa.jpf.jvm.JVM)
-	 */
+	 **/
 	public void advance(JVM vm) {
 		count++;
 	}
 
+	/**
+	 * get String label of current value, as specified in config file
+	 **/
+	public String getValueLabel(){
+		return values[count];
+	}
+
 }

[Javapathfinder-devel] javapathfinder jpf.properties,1.4,1.5

[pcm <pcm...@us...>]

Update of /cvsroot/javapathfinder/javapathfinder
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv29129

Modified Files:
	jpf.properties 
Log Message:
de-personalized jpf.properties

Index: jpf.properties
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/jpf.properties,v
retrieving revision 1.4
retrieving revision 1.5
diff -u -d -r1.4 -r1.5
--- jpf.properties	6 Oct 2005 21:56:15 -0000	1.4
+++ jpf.properties	6 Oct 2005 21:59:59 -0000	1.5
@@ -1,9 +1,12 @@
 # jpf.properties - the standard mode property file that is
 # loaded on top of default.properties, and normally contains
-# special Search and Heuristic settings
+# special Search and Heuristic settings.
 
-vm.classpath = /Users/pcmehlitz/tmp
-vm.sourcepath = ${vm.classpath}
+
+# where are your apps? You can set this here to include your standard dirs
+# (don't forget to set sourcepath accordingly if you want error traces)
+#vm.classpath = /Users/pcmehlitz/tmp
+#vm.sourcepath = ${vm.classpath}
 
 
 # search.class = gov.nasa.jpf.search.heuristic.HeuristicSearch
@@ -21,7 +24,7 @@
 log.level=warning
 
 # a simple DoubleThresholdGenerator example
-d0threshold.class = gov.nasa.jpf.jvm.choice.DoubleThresholdGenerator
-d0threshold.threshold = 0.0
-d0threshold.low = -1.0
-d0threshold.high = 1.0
+#d0threshold.class = gov.nasa.jpf.jvm.choice.DoubleThresholdGenerator
+#d0threshold.threshold = 0.0
+#d0threshold.low = -1.0
+#d0threshold.high = 1.0

[Javapathfinder-devel] javapathfinder/src/gov/nasa/jpf Config.java,1.8,1.9

[pcm <pcm...@us...>]

Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv28038/src/gov/nasa/jpf

Modified Files:
	Config.java 
Log Message:
command line args were not trimmed, causing

 bin/jpf "+key = value" ..
 
not to override 'key', but adding a new property entry. To make things worse, I
notoriously forget to quote arguments in shell scripts (bin/jpf)



Index: Config.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/Config.java,v
retrieving revision 1.8
retrieving revision 1.9
diff -u -d -r1.8 -r1.9
--- Config.java	9 Sep 2005 04:55:38 -0000	1.8
+++ Config.java	6 Oct 2005 21:56:15 -0000	1.9
@@ -240,7 +240,6 @@
    */
   void processArgs(String[] args) {
     int i;
-    String arg;
     ArrayList list = new ArrayList();
 
     for (i = 0; i < args.length; i++) {
@@ -249,7 +248,9 @@
         if (a.charAt(0) == '+') {
           int idx = a.indexOf("=");
           if (idx > 0) {
-            setProperty(a.substring(1, idx), a.substring(idx + 1));
+            String key = a.substring(1, idx).trim();
+            String val = a.substring(idx+1).trim();
+            setProperty(key, val);
           } else {
             setProperty(a.substring(1), "");
           }

[Javapathfinder-devel] javapathfinder build.xml,1.4,1.5 jpf.properties,1.3,1.4

[pcm <pcm...@us...>]

Update of /cvsroot/javapathfinder/javapathfinder
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv28038

Modified Files:
	build.xml jpf.properties 
Log Message:
command line args were not trimmed, causing

 bin/jpf "+key = value" ..
 
not to override 'key', but adding a new property entry. To make things worse, I
notoriously forget to quote arguments in shell scripts (bin/jpf)



Index: build.xml
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/build.xml,v
retrieving revision 1.4
retrieving revision 1.5
diff -u -d -r1.4 -r1.5
--- build.xml	11 May 2005 21:42:35 -0000	1.4
+++ build.xml	6 Oct 2005 21:56:15 -0000	1.5
@@ -34,7 +34,7 @@
   <property file="default.properties"/>
 	
   <!-- our required global properties -->
-  <property name="app.name"             value="open-jpf" />
+  <property name="app.name"             value="jpf" />
 		
   <!-- Project directories -->
   <property name="bin.dir"              value="bin" />

Index: jpf.properties
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/jpf.properties,v
retrieving revision 1.3
retrieving revision 1.4
diff -u -d -r1.3 -r1.4
--- jpf.properties	7 Sep 2005 22:08:20 -0000	1.3
+++ jpf.properties	6 Oct 2005 21:56:15 -0000	1.4
@@ -2,6 +2,8 @@
 # loaded on top of default.properties, and normally contains
 # special Search and Heuristic settings
 
+vm.classpath = /Users/pcmehlitz/tmp
+vm.sourcepath = ${vm.classpath}
 
 
 # search.class = gov.nasa.jpf.search.heuristic.HeuristicSearch
@@ -19,7 +21,7 @@
 log.level=warning
 
 # a simple DoubleThresholdGenerator example
-d0threshold.class = gov.nasa.jpf.jvm.DoubleThresholdGenerator
+d0threshold.class = gov.nasa.jpf.jvm.choice.DoubleThresholdGenerator
 d0threshold.threshold = 0.0
 d0threshold.low = -1.0
 d0threshold.high = 1.0

[Javapathfinder-devel] javapathfinder/bin jpf,1.7,1.8

[pcm <pcm...@us...>]

Update of /cvsroot/javapathfinder/javapathfinder/bin
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv28038/bin

Modified Files:
	jpf 
Log Message:
command line args were not trimmed, causing

 bin/jpf "+key = value" ..
 
not to override 'key', but adding a new property entry. To make things worse, I
notoriously forget to quote arguments in shell scripts (bin/jpf)



Index: jpf
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/bin/jpf,v
retrieving revision 1.7
retrieving revision 1.8
diff -u -d -r1.7 -r1.8
--- jpf	12 May 2005 06:25:31 -0000	1.7
+++ jpf	6 Oct 2005 21:56:15 -0000	1.8
@@ -55,4 +55,4 @@
   JVM_FLAGS="-Xmx1024m"
 fi
 
-java $JVM_FLAGS -classpath "$CP" gov.nasa.jpf.JPF +jpf.basedir="$JPF_HOME" $@
+java $JVM_FLAGS -classpath "$CP" gov.nasa.jpf.JPF +jpf.basedir="$JPF_HOME" "$@"

[Javapathfinder-devel] javapathfinder/src/gov/nasa/jpf/jvm JenkinsStateSet.java,NONE,1.1 JVM.java,1.10,1.11 StackFrame.java,1.3,1.4 Step.java,1.2,1.3 SystemState.java,1.4,1.5 ThreadInfo.java,1.10,1.11 ThreadList.java,1.1.1.1,1.2

[pcm <pcm...@us...>]

Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv15306/src/gov/nasa/jpf/jvm

Modified Files:
	JVM.java StackFrame.java Step.java SystemState.java 
	ThreadInfo.java ThreadList.java 
Added Files:
	JenkinsStateSet.java 
Log Message:
(1) added Peter Dillinger's JenkinsStateSet as a faster replacement for
MD5StateSet (20-30% speed improvement on large examples), the latter one
(with it's fast-MD5.jar) probably getting dropped from the distrib soon
(after some more testing)

(2) minor reporting changes (vm.report.show_missing_lines, format)

(3) another simple DoubleChoiceFromSet generator. Time to start with some
serious generators

(4) report thread stacks only if there was an error (i.e. system doesn't
terminate in init state)


Index: SystemState.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/SystemState.java,v
retrieving revision 1.4
retrieving revision 1.5
diff -u -d -r1.4 -r1.5
--- SystemState.java	9 Sep 2005 23:31:43 -0000	1.4
+++ SystemState.java	6 Oct 2005 21:05:53 -0000	1.5
@@ -147,6 +147,10 @@
     return ignored;
   }
 
+  public boolean isInitState () {
+    return (id == StateSet.UNKNOWN_ID);
+  }
+  
   public boolean getInteresting () {
     return interesting;
   }
@@ -191,7 +195,11 @@
   public int getRunnableThreadCount () {
     return ks.tl.getRunnableThreadCount();
   }
-  
+
+  public int getLiveThreadCount () {
+    return ks.tl.getLiveThreadCount();
+  }
+
   public ThreadInfo getThreadInfo (int idx) {
     return ks.tl.get(idx);
   }

Index: ThreadInfo.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/ThreadInfo.java,v
retrieving revision 1.10
retrieving revision 1.11
diff -u -d -r1.10 -r1.11
--- ThreadInfo.java	12 May 2005 06:25:32 -0000	1.10
+++ ThreadInfo.java	6 Oct 2005 21:05:53 -0000	1.11
@@ -1792,27 +1792,6 @@
     return (last > 0);
   }
   
-  public void printInternalErrorTrace (Throwable e) {
-    String msg = e.getMessage();
-    
-    if (msg != null) {
-      Debug.println(Debug.ERROR,
-                    "exception " + e.getClass().getName() + ": " + msg);
-    } else {
-      Debug.println(Debug.ERROR, "exception " + e.getClass().getName());
-    }
-    
-    printStackTrace();
-    
-    if (msg != null) {
-      Debug.println(Debug.ERROR,
-                    "exception " + e.getClass().getName() + ": " + msg);
-    } else {
-      Debug.println(Debug.ERROR, "exception " + e.getClass().getName());
-    }
-    
-    printStackContent();
-  }
   
   /**
    * Prints the content of the stack.

Index: Step.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/Step.java,v
retrieving revision 1.2
retrieving revision 1.3
diff -u -d -r1.2 -r1.3
--- Step.java	9 Jun 2005 19:54:54 -0000	1.2
+++ Step.java	6 Oct 2005 21:05:53 -0000	1.3
@@ -39,6 +39,8 @@
   String        comment;
   Step          next;
 
+  static int nMissing; // number of missing lines since last printed source line
+
   // report options - statics are suboptimal, but we don't have a good path
   // to the VM here
   static boolean showBytecode;
@@ -88,30 +90,40 @@
   public String getComment () {
     return comment;
   }
-
+  
   public void printStepOn (PrintWriter pw, SourceRef lastPrinted, String prefix) {
     Source source = Source.getSource(fileName);
     boolean isLineMissing = source.isLineMissing(line);
 
     if (!this.equals(lastPrinted)) {
-      if (!isLineMissing) {
-        pw.print( (prefix != null) ? prefix : "  ");
-        pw.print(Left.format(fileName + ":" + line, 20));
-        pw.print(' ');
-        pw.println(source.getLine(line));        
-      } else {
-        if (!fileName.equals(lastPrinted.getFileName()) && !showMissingLines) {
+      if (isLineMissing) {
+        if (showMissingLines) {
           pw.print( (prefix != null) ? prefix : "  ");
           pw.print("[no source for: ");
           pw.print(fileName);
-          pw.println(']');
+          pw.println(']');          
+        } else {
+          nMissing++;
+        }
+      } else {
+        if (nMissing > 0) {
+          pw.print( (prefix != null) ? prefix : "  ");
+          for (; nMissing > 0; nMissing--) {
+            pw.print('.');
+          }
+          pw.println();
         }
+        
+        pw.print( (prefix != null) ? prefix : "  ");
+        pw.print(Left.format(fileName + ":" + line, 20));
+        pw.print(' ');
+        pw.println(source.getLine(line));        
       }
       
       lastPrinted.set(this);
     }
 
-    if (showBytecode || (showMissingLines && isLineMissing) ) {
+    if (showBytecode) {
       if (insn != null) {
         MethodInfo mi = insn.getMethod();
         pw.print('\t');

Index: JVM.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/JVM.java,v
retrieving revision 1.10
retrieving revision 1.11
diff -u -d -r1.10 -r1.11
--- JVM.java	9 Sep 2005 04:55:38 -0000	1.10
+++ JVM.java	6 Oct 2005 21:05:53 -0000	1.11
@@ -871,21 +871,27 @@
    * JVM specific results
    */
   public void printResults (PrintWriter pw) {
-    if (config.getBoolean("vm.report.printStacks")) {
-      pw.println("------------------------------------ thread stacks");
-      printStackTraces(pw);
-      pw.println("------------------------------------ end thread stacks");
+    if (config.getBoolean("vm.report.print_stacks")) {      
+      if (!ss.isInitState()) { // otherwise there is not much to report
+        pw.println("------------------------------------ thread stacks");
+        printStackTraces(pw);
+      }
     }
   }
   
+  /**
+   * print call stacks of all live threads
+   */
   public void printStackTraces (PrintWriter pw) {
     int imax = ss.getThreadCount();
+    int n=0;
     
     for (int i = 0; i < imax; i++) {
       ThreadInfo ti = ss.getThreadInfo(i);
       String[] cs = ti.getCallStack();
       
       if (cs.length > 0) {
+        n++;
         pw.print("Thread: ");
         pw.println(ti.getName());
         for (int j=cs.length-1; j >= 0; j--) {
@@ -894,6 +900,10 @@
         pw.println();
       }
     }
+    
+    if (n==0) {
+      pw.println("no live threads");
+    }
   }
   
   void backtrackKernelState () {

--- NEW FILE: JenkinsStateSet.java ---
// contributed by Peter C. Dillinger and the Georgia Tech
// Research Corporation.
//
// Portions drawn from public domain work by Bob Jenkins, Dec. 1996
//
// Copyright (C) 2005 United States Government as represented by the
// Administrator of the National Aeronautics and Space Administration
// (NASA).  All Rights Reserved.
// 
// This software is distributed under the NASA Open Source Agreement
// (NOSA), version 1.3.  The NOSA has been approved by the Open Source
// Initiative.  See the file NOSA-1.3-JPF at the top of the distribution
// directory tree for the complete NOSA document.
// 
// THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY
// KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
// LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
// SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR
// A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT
// THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
// DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
//
package gov.nasa.jpf.jvm;

import gov.nasa.jpf.util.DynamicIntArray;

/**
 * Implements StateSet based on Jenkins hashes.
 */
public class JenkinsStateSet implements StateSet {
  static final double MAX_LOAD = 0.9;

  static final int INIT_SIZE = 65536;

  int lastStateId = -1;

  boolean isNewState;

  DynamicIntArray fingerprints = new DynamicIntArray();

  int[] hashtable = new int[INIT_SIZE];

  int nextRehash = (int) (MAX_LOAD * INIT_SIZE);

  // ugly, but unchanged
  public boolean isNewState (int stateId) {
    if (lastStateId == stateId) {
      return isNewState;
    } else {
      return false; // otherwise we've had a subsequent forward() or
      // backtrack
    }
  }

  public int size () {
    return lastStateId + 1;
  }

  public int add (SystemState ss) {
    int[] val = ss.getStoringData();

    // Jenkins' LOOKUP2 hash
    int a = 0x510fb60d;
    int b = 0xa4cb30d9;
    int c = 0x9e3779b9;

    int i;
    for (i = 0; i < val.length - 2; i += 3) {
      a += val[i];
      b += val[i + 1];
      c += val[i + 2];
      a -= b; a -= c; a ^= (c >>> 13);
      b -= c; b -= a; b ^= (a << 8);
      c -= a; c -= b; c ^= (b >>> 13);
      a -= b; a -= c; a ^= (c >>> 12);
      b -= c; b -= a; b ^= (a << 16);
      c -= a; c -= b; c ^= (b >>> 5);
      a -= b; a -= c; a ^= (c >>> 3);
      b -= c; b -= a; b ^= (a << 10);
      c -= a; c -= b; c ^= (b >>> 15);
    }
    switch (val.length - i) {
    case 2:
      c += val[val.length - 2];
    case 1:
      b += val[val.length - 1];
    }
    a += val.length;
    a -= b; a -= c; a ^= (c >>> 13);
    b -= c; b -= a; b ^= (a << 8);
    c -= a; c -= b; c ^= (b >>> 13);
    a -= b; a -= c; a ^= (c >>> 12);
    b -= c; b -= a; b ^= (a << 16);
    c -= a; c -= b; c ^= (b >>> 5);
    a -= b; a -= c; a ^= (c >>> 3);
    b -= c; b -= a; b ^= (a << 10);
    c -= a; c -= b; c ^= (b >>> 15);

    // hash table lookup & add; open-addressed, double hashing
    int mask = hashtable.length - 1;
    int idx = a & mask;
    int delta = (b & mask) | 1; // must be odd!
    int oidx = idx;

    while (hashtable[idx] != 0) {
      int id = hashtable[idx] - 1; // in table, 1 higher
      if (fingerprints.get(id * 3) == a && fingerprints.get(id * 3 + 1) == b
          && fingerprints.get(id * 3 + 2) == c) {
        isNewState = false;
        return id;
      }
      idx = (idx + delta) & mask;
      assert (idx != oidx); // should never wrap around
    }
    isNewState = true; // not found

    assert (hashtable[idx] == 0); // should never fill up

    if (lastStateId >= nextRehash) { // too full
      hashtable = null;
      // run GC here?
      hashtable = new int[(mask + 1) << 1];
      mask = hashtable.length - 1;
      nextRehash = (int) (MAX_LOAD * mask);

      for (i = 0; i <= lastStateId; i++) {
        idx = fingerprints.get(i * 3) & mask;
        delta = (fingerprints.get(i * 3 + 1) & mask) | 1;
        while (hashtable[idx] != 0) { // we know enough slots exist
          idx = (idx + delta) & mask;
        }
        hashtable[idx] = i + 1; // in table, add 1
      }
      // done with rehash; now get idx to empty slot
      idx = a & mask;
      delta = (b & mask) | 1;
      while (hashtable[idx] != 0) { // we know enough slots exist and state is
                                    // new
        idx = (idx + delta) & mask;
      }
    } else {
      // idx already pointing to empty slot
    }

    lastStateId++;
    hashtable[idx] = lastStateId + 1; // in table, add 1

    fingerprints.set(lastStateId * 3, a);
    fingerprints.set(lastStateId * 3 + 1, b);
    fingerprints.set(lastStateId * 3 + 2, c);

    // only reached if state is new
    return lastStateId;
  }
}
Index: ThreadList.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/ThreadList.java,v
retrieving revision 1.1.1.1
retrieving revision 1.2
diff -u -d -r1.1.1.1 -r1.2
--- ThreadList.java	26 Apr 2005 19:44:08 -0000	1.1.1.1
+++ ThreadList.java	6 Oct 2005 21:05:53 -0000	1.2
@@ -235,6 +235,18 @@
     return n;
   }
   
+  public int getLiveThreadCount () {
+    int n = 0;
+
+    for (int i = 0; i < threads.length; i++) {
+      if (threads[i].isAlive()) {
+        n++;
+      }
+    }
+
+    return n;
+  }  
+  
   boolean hasOtherRunnablesThan (int idx) {
     int i;
     int n = threads.length;

Index: StackFrame.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/StackFrame.java,v
retrieving revision 1.3
retrieving revision 1.4
diff -u -d -r1.3 -r1.4
--- StackFrame.java	5 May 2005 17:33:19 -0000	1.3
+++ StackFrame.java	6 Oct 2005 21:05:53 -0000	1.4
@@ -685,7 +685,9 @@
     }
   }
   
-  
+  /**
+   * this includes locals and pc
+   */
   public void printStackContent () {
     Debug.print(Debug.ERROR, "\tat ");
     Debug.print(Debug.ERROR, mi.getCompleteName());

[Javapathfinder-devel] javapathfinder/src/gov/nasa/jpf/tools SearchMonitor.java,1.2,1.3

[pcm <pcm...@us...>]

Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/tools
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv15306/src/gov/nasa/jpf/tools

Modified Files:
	SearchMonitor.java 
Log Message:
(1) added Peter Dillinger's JenkinsStateSet as a faster replacement for
MD5StateSet (20-30% speed improvement on large examples), the latter one
(with it's fast-MD5.jar) probably getting dropped from the distrib soon
(after some more testing)

(2) minor reporting changes (vm.report.show_missing_lines, format)

(3) another simple DoubleChoiceFromSet generator. Time to start with some
serious generators

(4) report thread stacks only if there was an error (i.e. system doesn't
terminate in init state)


Index: SearchMonitor.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/tools/SearchMonitor.java,v
retrieving revision 1.2
retrieving revision 1.3
diff -u -d -r1.2 -r1.3
--- SearchMonitor.java	18 May 2005 06:41:45 -0000	1.2
+++ SearchMonitor.java	6 Oct 2005 21:05:53 -0000	1.3
@@ -43,7 +43,7 @@
 
   static final String DEF_HOSTNAME = "localhost";
   static final int DEF_PORT = 20000;
-  static final int DEF_INTERVAL = 1000;   // min duration in ms between reports
+  static final int DEF_INTERVAL = Integer.MAX_VALUE;   // min duration in ms between reports
   
   String hostName = DEF_HOSTNAME;
   int port = DEF_PORT;
@@ -125,8 +125,9 @@
   public void searchStarted(Search search) {
     connect();
     
-    if (search instanceof HeuristicSearch)
-    	isHeuristic = true;
+    if (search instanceof HeuristicSearch) {
+      isHeuristic = true;
+    }
     
     startTime = lastTime = System.currentTimeMillis();
     

[Javapathfinder-devel] javapathfinder/src/gov/nasa/jpf Error.java,1.2,1.3

[pcm <pcm...@us...>]

Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv15306/src/gov/nasa/jpf

Modified Files:
	Error.java 
Log Message:
(1) added Peter Dillinger's JenkinsStateSet as a faster replacement for
MD5StateSet (20-30% speed improvement on large examples), the latter one
(with it's fast-MD5.jar) probably getting dropped from the distrib soon
(after some more testing)

(2) minor reporting changes (vm.report.show_missing_lines, format)

(3) another simple DoubleChoiceFromSet generator. Time to start with some
serious generators

(4) report thread stacks only if there was an error (i.e. system doesn't
terminate in init state)


Index: Error.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/Error.java,v
retrieving revision 1.2
retrieving revision 1.3
diff -u -d -r1.2 -r1.3
--- Error.java	9 Jun 2005 19:54:54 -0000	1.2
+++ Error.java	6 Oct 2005 21:05:53 -0000	1.3
@@ -62,12 +62,10 @@
     ps.print(path.length());
     ps.println(')');
     path.printOn(ps);
-    ps.println("------------------------------------ end error path");
     
     if (path.hasOutput()) {    
       ps.println("------------------------------------ path output");
       path.printOutputOn( ps);
-      ps.println("------------------------------------ end path output");
     }
   }
 }

[Javapathfinder-devel] javapathfinder/src/gov/nasa/jpf/jvm/choice DoubleChoiceFromSet.java,NONE,1.1

[pcm <pcm...@us...>]

Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/choice
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv15306/src/gov/nasa/jpf/jvm/choice

Added Files:
	DoubleChoiceFromSet.java 
Log Message:
(1) added Peter Dillinger's JenkinsStateSet as a faster replacement for
MD5StateSet (20-30% speed improvement on large examples), the latter one
(with it's fast-MD5.jar) probably getting dropped from the distrib soon
(after some more testing)

(2) minor reporting changes (vm.report.show_missing_lines, format)

(3) another simple DoubleChoiceFromSet generator. Time to start with some
serious generators

(4) report thread stacks only if there was an error (i.e. system doesn't
terminate in init state)


--- NEW FILE: DoubleChoiceFromSet.java ---
//
//Copyright (C) 2005 United States Government as represented by the
//Administrator of the National Aeronautics and Space Administration
//(NASA).  All Rights Reserved.
//
//This software is distributed under the NASA Open Source Agreement
//(NOSA), version 1.3.  The NOSA has been approved by the Open Source
//Initiative.  See the file NOSA-1.3-JPF at the top of the distribution
//directory tree for the complete NOSA document.
//
//THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY
//KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
//LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
//SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR
//A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT
//THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
//DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
//
package gov.nasa.jpf.jvm.choice;

import java.util.logging.Logger;

import gov.nasa.jpf.jvm.DoubleChoiceGenerator;
import gov.nasa.jpf.jvm.JVM;
import gov.nasa.jpf.Config;
import gov.nasa.jpf.JPF;

/**
 * simple DoubleChoiceGenerator that takes it's values from a single
 * property "values" (comma or blank separated list)
 */
public class DoubleChoiceFromSet extends DoubleChoiceGenerator {
  
  static Logger log = JPF.getLogger("gov.nasa.jpf.jvm.choice");
  
  double[] values;
  int count;
  
  public DoubleChoiceFromSet (Config conf, String id) {
    super(id);
    
    try {
      values = conf.getDoubleArray(id + ".values");
    } catch (Config.Exception cx) {
      log.warning("DoubleChoiceFromSet configuration error: " + cx);
      values = new double[0];
    }
      
    count = -1;
  }
  
  public double getNextChoice (JVM vm) {
    if (count < values.length) {
      return values[count];
    }
    
    return Double.NaN;  // Hmm, maybe we should return the last value
  }
  
  public boolean hasMoreChoices (JVM vm) {
    return (count < values.length-1);
  }
  
  public void advance (JVM vm) {
    count++;
  }
}

[Javapathfinder-devel] javapathfinder default.properties,1.3,1.4

[pcm <pcm...@us...>]

Update of /cvsroot/javapathfinder/javapathfinder
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv15306

Modified Files:
	default.properties 
Log Message:
(1) added Peter Dillinger's JenkinsStateSet as a faster replacement for
MD5StateSet (20-30% speed improvement on large examples), the latter one
(with it's fast-MD5.jar) probably getting dropped from the distrib soon
(after some more testing)

(2) minor reporting changes (vm.report.show_missing_lines, format)

(3) another simple DoubleChoiceFromSet generator. Time to start with some
serious generators

(4) report thread stacks only if there was an error (i.e. system doesn't
terminate in init state)


Index: default.properties
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/default.properties,v
retrieving revision 1.3
retrieving revision 1.4
diff -u -d -r1.3 -r1.4
--- default.properties	12 May 2005 06:25:31 -0000	1.3
+++ default.properties	6 Oct 2005 21:05:53 -0000	1.4
@@ -84,7 +84,7 @@
 vm.class = gov.nasa.jpf.jvm.JVM
 
 # class used to hash/store states (if not set, state data is not stored)
-vm.storage.class = gov.nasa.jpf.jvm.Md5StateSet
+vm.storage.class = gov.nasa.jpf.jvm.JenkinsStateSet
 
 # class used to set method and field attributes at load time
 vm.attributor.class = gov.nasa.jpf.jvm.DefaultAttributor
@@ -159,7 +159,7 @@
 vm.check_fp_compare = true
 
 # print all live thread stacks upon error
-vm.report.printStacks = true
+vm.report.print_stacks = true
 
 # do we want to report each step (insn) for a Transition
 vm.report.show_steps = true
@@ -167,7 +167,7 @@
 # do we want to print bytecodes instead of source lines?
 vm.report.show_bytecode = false
 
-# do we want to print insns without sources as bytecodes?
+# do we want to print placeholders for missing source lines
 vm.report.show_missing_lines = false