FIX: "java.lang.Char" should be "java.lang.Character". However, new unit test fails...
authorCyrille Artho <artho@kth.se>
Fri, 23 Nov 2018 14:39:40 +0000 (15:39 +0100)
committerCyrille Artho <artho@kth.se>
Fri, 23 Nov 2018 14:39:40 +0000 (15:39 +0100)
new file:   src/tests/gov/nasa/jpf/test/java/io/PrintStreamTest.java: New test, failing part commented out.

src/main/gov/nasa/jpf/vm/MJIEnv.java
src/peers/gov/nasa/jpf/vm/JPF_java_lang_reflect_Field.java
src/tests/gov/nasa/jpf/test/java/io/PrintStreamTest.java [new file with mode: 0644]

index 1558f27..1ce57a3 100644 (file)
@@ -1135,7 +1135,7 @@ public class MJIEnv {
           arg[i] = getBooleanObject(ref);
         } else if (clsName.equals("java.lang.Byte")) {
           arg[i] = getByteObject(ref);
-        } else if (clsName.equals("java.lang.Char")) {
+        } else if (clsName.equals("java.lang.Character")) {
           arg[i] = getCharObject(ref);
         } else if (clsName.equals("java.lang.Short")) {
           arg[i] = getShortObject(ref);
@@ -1169,7 +1169,7 @@ public class MJIEnv {
                  arg[i] = getStringObject(ref);
                } else if (clsName.equals("java.lang.Byte")) {
                  arg[i] = getByteObject(ref);
-               } else if (clsName.equals("java.lang.Char")) {
+               } else if (clsName.equals("java.lang.Character")) {
                  arg[i] = getCharObject(ref);
                } else if (clsName.equals("java.lang.Short")) {
                  arg[i] = getShortObject(ref);
index 758a0c7..8880f46 100644 (file)
@@ -716,7 +716,7 @@ public class JPF_java_lang_reflect_Field extends NativePeer {
       
       if (fi.isBooleanField() && valClsName.equals("java.lang.Boolean")) return true;
       else if (fi.isByteField() && valClsName.equals("java.lang.Byte")) return true;
-      else if (fi.isCharField() && valClsName.equals("java.lang.Char")) return true;
+      else if (fi.isCharField() && valClsName.equals("java.lang.Character")) return true;
       else if (fi.isShortField() && valClsName.equals("java.lang.Short")) return true;
       else if (fi.isIntField() && valClsName.equals("java.lang.Integer")) return true;
       else if (fi.isLongField() && valClsName.equals("java.lang.Long")) return true;
diff --git a/src/tests/gov/nasa/jpf/test/java/io/PrintStreamTest.java b/src/tests/gov/nasa/jpf/test/java/io/PrintStreamTest.java
new file mode 100644 (file)
index 0000000..47556f2
--- /dev/null
@@ -0,0 +1,42 @@
+/*
+ * Copyright (C) 2014, United States Government, as represented by the
+ * Administrator of the National Aeronautics and Space Administration.
+ * All rights reserved.
+ *
+ * The Java Pathfinder core (jpf-core) platform is licensed under the
+ * Apache License, Version 2.0 (the "License"); you may not use this file except
+ * in compliance with the License. You may obtain a copy of the License at
+ * 
+ *        http://www.apache.org/licenses/LICENSE-2.0. 
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and 
+ * limitations under the License.
+ */
+
+package gov.nasa.jpf.test.java.io;
+
+import gov.nasa.jpf.util.test.TestJPF;
+
+import java.io.ByteArrayOutputStream;
+import java.io.PrintStream;
+
+import org.junit.Test;
+
+/**
+ * regression test for object streams
+ */
+public class PrintStreamTest extends TestJPF {
+
+  @Test // currently fails with: java.lang.NoSuchMethodError: java.util.regex.Matcher.find(I)Z
+  public void testPrintCharFormat () {
+    if (verifyNoPropertyViolation()){
+       ByteArrayOutputStream baos = new ByteArrayOutputStream(1);
+       PrintStream baps = new PrintStream(baos, true);
+//     baps.printf("%c", 'a'); // fails
+//     assert (baos.toByteArray()[0] == 97);
+    }
+  }
+}