From f7336c4df1322b1d586c0ebc34c10fd57f340667 Mon Sep 17 00:00:00 2001
From: Cyrille Artho <artho@kth.se>
Date: Fri, 23 Nov 2018 15:39:40 +0100
Subject: [PATCH] FIX: "java.lang.Char" should be "java.lang.Character".
 However, new unit test fails due to other problem. 	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          |  4 +-
 .../jpf/vm/JPF_java_lang_reflect_Field.java   |  2 +-
 .../jpf/test/java/io/PrintStreamTest.java     | 42 +++++++++++++++++++
 3 files changed, 45 insertions(+), 3 deletions(-)
 create mode 100644 src/tests/gov/nasa/jpf/test/java/io/PrintStreamTest.java

diff --git a/src/main/gov/nasa/jpf/vm/MJIEnv.java b/src/main/gov/nasa/jpf/vm/MJIEnv.java
index 1558f27..1ce57a3 100644
--- a/src/main/gov/nasa/jpf/vm/MJIEnv.java
+++ b/src/main/gov/nasa/jpf/vm/MJIEnv.java
@@ -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);
diff --git a/src/peers/gov/nasa/jpf/vm/JPF_java_lang_reflect_Field.java b/src/peers/gov/nasa/jpf/vm/JPF_java_lang_reflect_Field.java
index 758a0c7..8880f46 100644
--- a/src/peers/gov/nasa/jpf/vm/JPF_java_lang_reflect_Field.java
+++ b/src/peers/gov/nasa/jpf/vm/JPF_java_lang_reflect_Field.java
@@ -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
index 0000000..47556f2
--- /dev/null
+++ b/src/tests/gov/nasa/jpf/test/java/io/PrintStreamTest.java
@@ -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);
+    }
+  }
+}
-- 
2.34.1