Description
The JPF model class for java.util.regex.Matcher is missing two standard Java methods that are marked as TODO in the source code. These methods are essential for common regex find-and-replace workflows.
Missing Methods
| Method |
Signature |
appendTail |
StringBuffer appendTail(StringBuffer sb) |
appendReplacement |
Matcher appendReplacement(StringBuffer sb, String replacement) |
Current State
// File: src/classes/modules/java.base/java/util/regex/Matcher.java (lines 164-165)
// TODO public native StringBuffer appendTail(StringBuffer sb);
// TODO public native Matcher appendReplacement(StringBuffer sb, String replacement);
Use Case
These methods enable the standard pattern for regex-based string transformation:
Pattern p = Pattern.compile("cat");
Matcher m = p.matcher("one cat two cats");
StringBuffer sb = new StringBuffer();
while (m.find()) {
m.appendReplacement(sb, "dog"); // ← Currently missing
}
m.appendTail(sb); // ← Currently missing
// Result: "one dog two dogs"Implementation Approach
┌─────────────────────────────────────────────────────────────────┐
│ Model Class │
│ src/classes/modules/java.base/java/util/regex/Matcher.java │
├─────────────────────────────────────────────────────────────────┤
│ + public native StringBuffer appendTail(StringBuffer sb); │
│ + public native Matcher appendReplacement(StringBuffer sb, │
│ String replacement); │
└────────────────────────────┬────────────────────────────────────┘
│ delegates via MJI
▼
┌─────────────────────────────────────────────────────────────────┐
│ Native Peer │
│ src/peers/gov/nasa/jpf/vm/JPF_java_util_regex_Matcher.java│
├─────────────────────────────────────────────────────────────────┤
│ + appendTail__Ljava_lang_StringBuffer_2(...) │
│ + appendReplacement__Ljava_lang_StringBuffer_2...(...) │
│ │
│ Implementation: Delegate to real java.util.regex.Matcher │
└─────────────────────────────────────────────────────────────────┘
Files to Modify
src/classes/modules/java.base/java/util/regex/Matcher.java — Add native method declarationssrc/peers/gov/nasa/jpf/vm/JPF_java_util_regex_Matcher.java — Implement native peer methods
Description
The JPF model class for
java.util.regex.Matcheris missing two standard Java methods that are marked as TODO in the source code. These methods are essential for common regex find-and-replace workflows.Missing Methods
appendTailStringBuffer appendTail(StringBuffer sb)appendReplacementMatcher appendReplacement(StringBuffer sb, String replacement)Current State
Use Case
These methods enable the standard pattern for regex-based string transformation:
Implementation Approach
Files to Modify
src/classes/modules/java.base/java/util/regex/Matcher.java— Add native method declarationssrc/peers/gov/nasa/jpf/vm/JPF_java_util_regex_Matcher.java— Implement native peer methods