From 0a84e8efb3a8509bbb8564ef9fe4abf2bdcb62b3 Mon Sep 17 00:00:00 2001 From: Manish Kumar Thakur Date: Tue, 29 Jan 2019 19:14:19 +0530 Subject: [PATCH] Rectifies the java.lang.NoSuchMethodError when usinf printf (#172) * Rectifies the java.lang.NoSuchMethodError: java.util.regex.Matcher.find(I)Z error by overloading the find() method in native peer classes * adds unit test --- src/classes/java/util/regex/Matcher.java | 2 ++ .../gov/nasa/jpf/vm/JPF_java_util_regex_Matcher.java | 6 ++++++ src/tests/gov/nasa/jpf/test/java/io/PrintStreamTest.java | 8 ++++---- 3 files changed, 12 insertions(+), 4 deletions(-) diff --git a/src/classes/java/util/regex/Matcher.java b/src/classes/java/util/regex/Matcher.java index 8b1aac4..515318e 100644 --- a/src/classes/java/util/regex/Matcher.java +++ b/src/classes/java/util/regex/Matcher.java @@ -67,6 +67,8 @@ public class Matcher { public native boolean matches(); public native boolean find(); + + public native boolean find(int start); public native boolean lookingAt(); diff --git a/src/peers/gov/nasa/jpf/vm/JPF_java_util_regex_Matcher.java b/src/peers/gov/nasa/jpf/vm/JPF_java_util_regex_Matcher.java index b514846..ebf9a21 100644 --- a/src/peers/gov/nasa/jpf/vm/JPF_java_util_regex_Matcher.java +++ b/src/peers/gov/nasa/jpf/vm/JPF_java_util_regex_Matcher.java @@ -73,6 +73,12 @@ public class JPF_java_util_regex_Matcher extends NativePeer { return matcher.matches(); } + @MJI + public boolean find__I__Z (MJIEnv env, int objref, int i) { + Matcher matcher = getInstance( env, objref); + return matcher.find(i); + } + @MJI public boolean find____Z (MJIEnv env, int objref) { Matcher matcher = getInstance( env, objref); diff --git a/src/tests/gov/nasa/jpf/test/java/io/PrintStreamTest.java b/src/tests/gov/nasa/jpf/test/java/io/PrintStreamTest.java index 47556f2..6cadb32 100644 --- a/src/tests/gov/nasa/jpf/test/java/io/PrintStreamTest.java +++ b/src/tests/gov/nasa/jpf/test/java/io/PrintStreamTest.java @@ -30,13 +30,13 @@ import org.junit.Test; */ public class PrintStreamTest extends TestJPF { - @Test // currently fails with: java.lang.NoSuchMethodError: java.util.regex.Matcher.find(I)Z + @Test 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); + baps.printf("%c", 'a'); + assert (baos.toByteArray()[0] == 97); } } -} +} \ No newline at end of file -- 2.34.1