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.
19 package gov.nasa.jpf.vm;
21 import gov.nasa.jpf.annotation.MJI;
22 import gov.nasa.jpf.vm.MJIEnv;
23 import gov.nasa.jpf.vm.NativePeer;
25 import java.text.DecimalFormat;
26 import java.text.Format;
27 import java.text.NumberFormat;
28 import java.text.ParsePosition;
30 // NOTE - this only works because DecimalFormat is a Format subclass, i.e.
31 // the java.text.Format native peer will be initialized first
32 // (otherwise we shouldn't depend on static data of other native peers)
34 public class JPF_java_text_DecimalFormat extends NativePeer {
36 static final int INTEGER_STYLE=0;
37 static final int NUMBER_STYLE=1;
39 NumberFormat getInstance (MJIEnv env, int objref) {
40 Format fmt = JPF_java_text_Format.getInstance(env,objref);
41 assert fmt instanceof NumberFormat;
43 return (NumberFormat)fmt;
47 * NOTE: if we would directly intercept the ctors, we would have to
48 * explicitly call the superclass ctors here (the 'id' handle gets
49 * initialized in the java.text.Format ctor)
52 public void init0____V (MJIEnv env, int objref) {
53 DecimalFormat fmt = new DecimalFormat();
54 JPF_java_text_Format.putInstance(env,objref,fmt);
58 public void init0__Ljava_lang_String_2__V (MJIEnv env, int objref, int patternref) {
59 String pattern = env.getStringObject(patternref);
61 DecimalFormat fmt = new DecimalFormat(pattern);
62 JPF_java_text_Format.putInstance(env,objref,fmt);
66 public void init0__I__V (MJIEnv env, int objref, int style) {
67 NumberFormat fmt = null;
68 if (style == INTEGER_STYLE) {
69 fmt = NumberFormat.getIntegerInstance();
70 } else if (style == NUMBER_STYLE) {
71 fmt = NumberFormat.getNumberInstance();
74 fmt = new DecimalFormat();
77 JPF_java_text_Format.putInstance(env,objref,fmt);
81 public void setMaximumFractionDigits__I__V (MJIEnv env, int objref, int newValue){
82 NumberFormat fmt = getInstance(env,objref);
84 fmt.setMaximumFractionDigits(newValue);
89 public void setMaximumIntegerDigits__I__V (MJIEnv env, int objref, int newValue){
90 NumberFormat fmt = getInstance(env,objref);
92 fmt.setMaximumIntegerDigits(newValue);
97 public void setMinimumFractionDigits__I__V (MJIEnv env, int objref, int newValue){
98 NumberFormat fmt = getInstance(env,objref);
100 fmt.setMinimumFractionDigits(newValue);
105 public void setMinimumIntegerDigits__I__V (MJIEnv env, int objref, int newValue){
106 NumberFormat fmt = getInstance(env,objref);
108 fmt.setMinimumIntegerDigits(newValue);
113 public int format__J__Ljava_lang_String_2 (MJIEnv env, int objref, long number) {
114 NumberFormat fmt = getInstance(env,objref);
116 String s = fmt.format(number);
117 int sref = env.newString(s);
125 public int format__D__Ljava_lang_String_2 (MJIEnv env, int objref, double number) {
126 NumberFormat fmt = getInstance(env,objref);
128 String s = fmt.format(number);
129 int sref = env.newString(s);
137 public void setParseIntegerOnly__Z__V(MJIEnv env, int objref, boolean value) {
138 NumberFormat fmt = getInstance(env,objref);
140 fmt.setParseIntegerOnly(value);
145 public boolean isParseIntegerOnly____Z(MJIEnv env, int objref) {
146 NumberFormat fmt = getInstance(env,objref);
148 return fmt.isParseIntegerOnly();
154 public void setGroupingUsed__Z__V(MJIEnv env, int objref, boolean newValue) {
155 NumberFormat fmt = getInstance(env,objref);
157 fmt.setGroupingUsed(newValue);
162 public boolean isGroupingUsed____Z(MJIEnv env, int objref) {
163 NumberFormat fmt = getInstance(env,objref);
165 return fmt.isGroupingUsed();
171 public int parse__Ljava_lang_String_2Ljava_text_ParsePosition_2__Ljava_lang_Number_2(MJIEnv env, int objref,int sourceRef,int parsePositionRef) {
172 String source = env.getStringObject(sourceRef);
173 ParsePosition parsePosition = createParsePositionFromRef(env,parsePositionRef);
174 NumberFormat fmt = getInstance(env,objref);
175 Number number = null;
177 number = fmt.parse(source,parsePosition);
179 updateParsePositionRef(env,parsePositionRef, parsePosition);
180 return createNumberRefFromNumber(env,number);
183 private static ParsePosition createParsePositionFromRef(MJIEnv env,int parsePositionRef) {
184 int index = env.getIntField(parsePositionRef, "index");
185 int errorIndex = env.getIntField(parsePositionRef, "errorIndex");
186 ParsePosition ps = new ParsePosition(index);
187 ps.setErrorIndex(errorIndex);
191 private static void updateParsePositionRef(MJIEnv env,int parsePositionRef, ParsePosition parsePosition) {
192 env.setIntField(parsePositionRef, "index", parsePosition.getIndex());
193 env.setIntField(parsePositionRef, "errorIndex", parsePosition.getErrorIndex());
196 private static int createNumberRefFromNumber(MJIEnv env,Number number) {
197 int numberRef = MJIEnv.NULL;
198 if(number instanceof Double) {
199 numberRef = env.newObject("java.lang.Double");
200 env.setDoubleField(numberRef, "value", number.doubleValue());
201 } else if(number instanceof Long) {
202 numberRef = env.newObject("java.lang.Long");
203 env.setLongField(numberRef, "value", number.longValue());