2 * Copyright (C) 2014, United States Government, as represented by the
3 * Administrator of the National Aeronautics and Space Administration.
6 * The Java Pathfinder core (jpf-core) platform is licensed under the
7 * Apache License, Version 2.0 (the "License"); you may not use this file except
8 * in compliance with the License. You may obtain a copy of the License at
10 * http://www.apache.org/licenses/LICENSE-2.0.
12 * Unless required by applicable law or agreed to in writing, software
13 * distributed under the License is distributed on an "AS IS" BASIS,
14 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
15 * See the License for the specific language governing permissions and
16 * limitations under the License.
18 package gov.nasa.jpf.vm;
20 import gov.nasa.jpf.annotation.MJI;
21 import gov.nasa.jpf.vm.MJIEnv;
22 import gov.nasa.jpf.vm.NativePeer;
24 public class JPF_java_lang_StringBuilder extends NativePeer {
26 int appendString (MJIEnv env, int objref, String s) {
27 int slen = s.length();
28 int aref = env.getReferenceField(objref, "value");
29 int alen = env.getArrayLength(aref);
30 int count = env.getIntField(objref, "count");
35 for (i=count, j=0; i<n; i++, j++) {
36 env.setCharArrayElement(aref, i, s.charAt(j));
43 int arefNew = env.newCharArray(m);
44 for (i=0; i<count; i++) {
45 env.setCharArrayElement(arefNew, i, env.getCharArrayElement(aref, i));
47 for (j=0; i<n; i++, j++) {
48 env.setCharArrayElement(arefNew, i, s.charAt(j));
50 env.setReferenceField(objref, "value", arefNew);
53 env.setIntField(objref, "count", n);
58 // we skip the AbstractStringBuilder ctor here, which is a bit dangerous
59 // This is only justified because StringBuilders are used everywhere (implicitly)
61 public void $init____V (MJIEnv env, int objref){
62 int aref = env.newCharArray(16);
63 env.setReferenceField(objref, "value", aref);
66 public void $init__I__V (MJIEnv env, int objref, int len){
67 int aref = env.newCharArray(len);
68 env.setReferenceField(objref, "value", aref);
71 public void $init__Ljava_lang_String_2__V (MJIEnv env, int objref, int sRef){
72 if (sRef == MJIEnv.NULL){
73 env.throwException("java.lang.NullPointerException");
77 char[] src = env.getStringChars(sRef);
78 int aref = env.newCharArray(src.length + 16);
79 char[] dst = env.getCharArrayObject(aref);
80 System.arraycopy(src,0,dst,0,src.length);
82 env.setReferenceField(objref, "value", aref);
83 env.setIntField(objref, "count", src.length);
88 public int append__Ljava_lang_String_2__Ljava_lang_StringBuilder_2 (MJIEnv env, int objref, int sref) {
89 String s = env.getStringObject(sref);
91 if (s == null) s = "null";
93 return appendString(env, objref, s);
97 public int append__I__Ljava_lang_StringBuilder_2 (MJIEnv env, int objref, int i) {
98 String s = Integer.toString(i);
100 return appendString(env, objref, s);
104 public int append__F__Ljava_lang_StringBuilder_2 (MJIEnv env, int objref, float f) {
105 String s = Float.toString(f);
107 return appendString(env, objref, s);
111 public int append__D__Ljava_lang_StringBuilder_2 (MJIEnv env, int objref, double d) {
112 String s = Double.toString(d);
114 return appendString(env, objref, s);
118 public int append__J__Ljava_lang_StringBuilder_2 (MJIEnv env, int objref, long l) {
119 String s = Long.toString(l);
121 return appendString(env, objref, s);
125 public int append__Z__Ljava_lang_StringBuilder_2 (MJIEnv env, int objref, boolean b) {
126 String s = b ? "true" : "false";
128 return appendString(env, objref, s);
132 public int append__C__Ljava_lang_StringBuilder_2 (MJIEnv env, int objref, char c) {
133 int aref = env.getReferenceField(objref, "value");
134 int alen = env.getArrayLength(aref);
135 int count = env.getIntField(objref, "count");
140 env.setCharArrayElement(aref, count, c);
142 int m = 3 * alen / 2;
143 int arefNew = env.newCharArray(m);
144 for (i=0; i<count; i++) {
145 env.setCharArrayElement(arefNew, i, env.getCharArrayElement(aref, i));
147 env.setCharArrayElement(arefNew, count, c);
148 env.setReferenceField(objref, "value", arefNew);
151 env.setIntField(objref, "count", n);
158 public int toString____Ljava_lang_String_2 (MJIEnv env, int objref) {
159 int aref = env.getReferenceField(objref, "value");
160 int count = env.getIntField(objref, "count");
162 char[] buf = env.getCharArrayObject(aref);
163 String s = new String(buf, 0, count);
164 return env.newString(s);