fix for String (getBytes()) (#449)

javapathfinder · May 3, 2024 · e3a56c1 · e3a56c1
1 parent 505f0a2
commit e3a56c1
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 8 deletions.
diff --git a/src/classes/modules/java.base/java/lang/String.java b/src/classes/modules/java.base/java/lang/String.java
@@ -600,6 +600,10 @@ public char charAt(int index) {
 
 	@Deprecated
 	native public void getBytes(int srcBegin, int srcEnd, byte dst[], int dstBegin);
+	public void getBytes(byte[] dst, int srcPos, int dstBegin, byte coder, int length){
+		getBytes(srcPos,(srcPos+length),dst,dstBegin);
+	}
+
 	native public byte[] getBytes(String charsetName)
 			throws UnsupportedEncodingException;
 

diff --git a/src/peers/gov/nasa/jpf/vm/JPF_java_lang_String.java b/src/peers/gov/nasa/jpf/vm/JPF_java_lang_String.java
@@ -18,12 +18,6 @@
 package gov.nasa.jpf.vm;
 
 import gov.nasa.jpf.annotation.MJI;
-import gov.nasa.jpf.vm.CharArrayFields;
-import gov.nasa.jpf.vm.ElementInfo;
-import gov.nasa.jpf.vm.Fields;
-import gov.nasa.jpf.vm.Heap;
-import gov.nasa.jpf.vm.MJIEnv;
-import gov.nasa.jpf.vm.NativePeer;
 
 import java.io.UnsupportedEncodingException;
 import java.util.Locale;
@@ -33,7 +27,7 @@
  */
 public class JPF_java_lang_String extends NativePeer {
 
-  
+
   @MJI
   public int init___3CII__Ljava_lang_String_2 (MJIEnv env, int objRef, int valueRef, int offset, int count) {
     char[] value = env.getCharArrayObject(valueRef);
@@ -108,7 +102,7 @@ public void getChars___3CI__V(MJIEnv env, int objRef, int dstRef, int dstBegin)
     char[] dst = env.getCharArrayObject(dstRef);
     obj.getChars(0, obj.length(), dst, dstBegin);
   }
-  
+
   @SuppressWarnings("deprecation")
   @MJI
   public void getBytes__II_3BI__V (MJIEnv env, int objRef, int srcBegin, int srcEnd, int dstRef, int dstBegin) {