Fix get/setShort for field and array reflection
authorJohn Toman <jtoman@cs.washington.edu>
Thu, 30 Aug 2018 22:40:28 +0000 (15:40 -0700)
committerJohn Toman <jtoman@cs.washington.edu>
Fri, 31 Aug 2018 19:24:25 +0000 (12:24 -0700)
src/main/gov/nasa/jpf/vm/MJIEnv.java
src/peers/gov/nasa/jpf/vm/JPF_java_lang_reflect_Array.java
src/tests/gov/nasa/jpf/test/java/lang/reflect/FieldTest.java

index 2bac12a..a37a941 100644 (file)
@@ -562,11 +562,13 @@ public class MJIEnv {
   }
 
   public void setShortField (int objref, String fname, short val) {
-    setIntField(objref, fname, /*(int)*/ val);
+    ElementInfo ei = heap.getModifiable(objref);
+    ei.setShortField(fname, val);
   }
 
   public short getShortField (int objref, String fname) {
-    return (short) getIntField(objref, fname);
+    ElementInfo ei = heap.get(objref);
+    return ei.getShortField(fname);
   }
 
   /**
index 8dfa035..325dcb7 100644 (file)
@@ -111,7 +111,7 @@ public class JPF_java_lang_reflect_Array extends NativePeer {
   @MJI
   public int get__Ljava_lang_Object_2I__Ljava_lang_Object_2 (MJIEnv env, int clsRef,
                                                                     int aref, int index){
-    String at = env.getArrayType(aref);
+    String at = Types.getTypeName(env.getArrayType(aref));
     if (at.equals("int")){
       int vref = env.newObject("java.lang.Integer");
       env.setIntField(vref, "value", env.getIntArrayElement(aref,index));
index ed29c71..48e863d 100644 (file)
@@ -22,6 +22,7 @@ import gov.nasa.jpf.util.test.TestJPF;
 import java.lang.annotation.Inherited;
 import java.lang.annotation.Retention;
 import java.lang.annotation.RetentionPolicy;
+import java.lang.reflect.Array;
 import java.lang.reflect.Field;
 
 import org.junit.Test;
@@ -96,6 +97,10 @@ public class FieldTest extends TestJPF {
   public class Sub {
     public int f;
   }
+  
+  public static class ShortField {
+    short f;
+  }
 
   @Test
   public void getDeclaredAnnotationsTest () throws SecurityException, NoSuchFieldException{
@@ -106,4 +111,18 @@ public class FieldTest extends TestJPF {
       assertEquals(f2.getDeclaredAnnotations().length, 1);
     }
   }
+  
+  @Test
+  public void getSetShortFieldTest() throws NoSuchFieldException, SecurityException, IllegalArgumentException, IllegalAccessException {
+    if(verifyNoPropertyViolation()) {
+      ShortField sf = new ShortField();
+      Field f = sf.getClass().getField("f");
+      f.set(sf, (short)3);
+      assertEquals((short)f.get(sf), (short)3);
+      
+      short[] x = new short[] {1,2,3};
+      Array.setShort(x, 0, (short) 3);
+      assertEquals(Array.getShort(x, 0), (short)3);
+    }
+  }
 }