[Javapathfinder-devel] javapathfinder/env/jvm/gov/nasa/jpf/jvm JPF_java_io_RandomAccessFile.java,1.1.1.1,1.2

[Willem V. <wv...@us...>]

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

Modified Files:
	JPF_java_io_RandomAccessFile.java 
Log Message:
* fixed problem with RandomAccessFile not working for multiple 
* accesses to the same file

Index: JPF_java_io_RandomAccessFile.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/env/jvm/gov/nasa/jpf/jvm/JPF_java_io_RandomAccessFile.java,v
retrieving revision 1.1.1.1
retrieving revision 1.2
diff -u -d -r1.1.1.1 -r1.2
--- JPF_java_io_RandomAccessFile.java	26 Apr 2005 19:43:26 -0000	1.1.1.1
+++ JPF_java_io_RandomAccessFile.java	23 Jun 2005 20:50:06 -0000	1.2
@@ -19,6 +19,8 @@
 
 package gov.nasa.jpf.jvm;
 
+import java.util.HashMap;
+
 /**
  * MJI NativePeer class for java.io.RandomAccessFile library abstraction
  *
@@ -26,6 +28,28 @@
  */
 public class JPF_java_io_RandomAccessFile {
 
+	// need to see whether the file is already in use
+	// if so, then we'll update the file data and length in the original file
+	// we do update the length in the local object, but not the data
+		
+	static HashMap File2DataMap = new HashMap();
+	
+	// get the mapped object if one exists
+	private static int getMapping(MJIEnv env, int this_ptr) {
+		int fn_ptr = env.getReferenceField(this_ptr,"filename");
+		Object o = File2DataMap.get(new Integer(fn_ptr));
+		if (o == null)
+			return this_ptr;
+		return ((Integer)o).intValue();
+	}
+	
+	// set the mapping during the constructor call
+	public static void setDataMap(MJIEnv env, int this_ptr) {
+		int fn_ptr = env.getReferenceField(this_ptr,"filename");
+		if (!File2DataMap.containsKey(new Integer(fn_ptr))) 
+			File2DataMap.put(new Integer(fn_ptr),new Integer(this_ptr));
+	}
+	
   public static void writeByte(MJIEnv env, int this_ptr, int data) {
     long current_posn = env.getLongField(this_ptr, current_position);
     long current_len = env.getLongField(this_ptr, current_length);
@@ -37,6 +61,8 @@
     env.setLongField(this_ptr, current_position, current_posn);
     if (current_posn >= current_len) {
       env.setLongField(this_ptr, current_length, current_posn + 1);
+      // update length in the mapped object if it exists
+      env.setLongField(getMapping(env,this_ptr), current_length, current_posn + 1);
     }
   }
 
@@ -58,6 +84,8 @@
       env.setLongField(this_ptr, current_position, len);
     }
     env.setLongField(this_ptr, current_length, len);
+    // update length in the mapped object if it exists
+    env.setLongField(getMapping(env,this_ptr), current_length, current_posn + 1);
   }
 
   public static int read(MJIEnv env, int this_ptr, int data_array,
@@ -105,6 +133,9 @@
 
   private static int findDataChunk(MJIEnv env, int this_ptr, long position,
                                    int chunk_size) {
+  	
+  	//check if the file data is mapped, use mapped this_ptr if it exists
+  	this_ptr = getMapping(env,this_ptr);  	
     int prev_obj = MJIEnv.NULL;
     int cur_obj = env.getReferenceField(this_ptr, data_root);
     long chunk_idx = position/chunk_size;