package java.nio;
public abstract class Buffer {
+
protected int position;
protected int capacity;
protected int limit;
+ protected int mark = -1;
+
+
+ // Todo: There exists other missing methods in this class
+ // which may throw NoSuchMethodException errors to users
+ // For example checkBounds has yet to be implemented
+ Buffer(int mark, int pos, int lim, int cap) {
+ if (cap < 0)
+ throw new IllegalArgumentException("Negative capacity: " + cap);
+ this.capacity = cap;
+ limit(lim);
+ position(pos);
+ if (mark >= 0 && mark <= pos){
+ this.mark = mark;
+ }
+ }
public final int capacity() {
return capacity;
public final Buffer clear(){
position = 0;
limit = capacity;
+ mark = -1;
return this;
}
public class ByteBuffer extends Buffer {
byte[] array;
+ int offset;
public static ByteBuffer allocate(int i) {
if (i < 0) {
throw new IllegalArgumentException();
}
- ByteBuffer newBuffer = new ByteBuffer(i);
+ ByteBuffer newBuffer = new ByteBuffer(-1, 0, i, i, new byte[i], 0);
return newBuffer;
}
return allocate(capacity);
}
- protected ByteBuffer(int i) {
- capacity = i;
- this.clear();
- array = new byte[i];
+ ByteBuffer(int mark, int pos, int lim, int cap, byte[] hb, int offset) {
+ super(mark, pos, lim, cap);
+ this.array = hb;
+ this.offset = offset;
+ }
+
+ ByteBuffer(int mark, int pos, int lim, int cap) {
+ this(mark, pos, lim, cap, null, 0);
}
public ByteBuffer duplicate() {
- ByteBuffer copy = new ByteBuffer(capacity);
+ ByteBuffer copy = new ByteBuffer(-1, 0, capacity, capacity, new byte[capacity], 0);
copy.array = array;
return copy;
}
public ByteBuffer slice() {
int remaining = limit - position;
- ByteBuffer copy = new ByteBuffer(remaining);
+ ByteBuffer copy = new ByteBuffer(-1, 0, remaining, remaining, new byte[remaining], 0);
copy.array = array;
return copy;
}
}
public static ByteBuffer wrap(byte[] outMess) {
- ByteBuffer byteBuffer = new ByteBuffer(outMess.length);
+ ByteBuffer byteBuffer = new ByteBuffer(-1, 0, outMess.length, outMess.length, new byte[outMess.length], 0);
byteBuffer.clear();
System.arraycopy(outMess, 0 , byteBuffer.array, 0, outMess.length);
return byteBuffer;
package java.text;
+import java.util.Locale;
+
public abstract class NumberFormat extends Format {
static final int INTEGER_STYLE=0;
return new DecimalFormat(NUMBER_STYLE);
}
+ public static NumberFormat getNumberInstance(Locale locale) {
+ return new DecimalFormat(NUMBER_STYLE);
+ }
+
public static NumberFormat getInstance() {
return new DecimalFormat(NUMBER_STYLE);
}
public native Matcher useAnchoringBounds(boolean b);
+ public Matcher usePattern(Pattern newPattern){
+ this.pattern = newPattern;
+ return updatePattern();
+ }
+
+ public native Matcher updatePattern();
+
public native int regionStart();
public native int regionEnd();
matchers = new HashMap<Integer,Matcher>();
}
+ Pattern getPatternFromMatcher(MJIEnv env, int objref) {
+ int patRef = env.getReferenceField(objref, "pattern");
+
+ int regexRef = env.getReferenceField(patRef, "regex");
+ String regex = env.getStringObject(regexRef);
+ int flags = env.getIntField(patRef, "flags");
+
+ return Pattern.compile(regex, flags);
+ }
+
void putInstance (MJIEnv env, int objref, Matcher matcher) {
int id = env.getIntField(objref, "id");
matchers.put(id, matcher);
@MJI
public void register____V (MJIEnv env, int objref) {
- int patRef = env.getReferenceField(objref, "pattern");
-
- int regexRef = env.getReferenceField(patRef, "regex");
- String regex = env.getStringObject(regexRef);
- int flags = env.getIntField(patRef, "flags");
-
- Pattern pat = Pattern.compile(regex, flags);
+ Pattern pat = getPatternFromMatcher(env, objref);
int inputRef = env.getReferenceField(objref, "input");
String input = env.getStringObject(inputRef);
return objref;
}
+ @MJI
+ public int updatePattern____Ljava_util_regex_Matcher_2(MJIEnv env, int objref) {
+ //We get the newly updated pattern
+ Pattern pat = getPatternFromMatcher(env, objref);
+
+ //We update the matcher with the new pattern
+ Matcher matcher = getInstance(env, objref);
+ matcher = matcher.usePattern(pat);
+ putInstance(env, objref, matcher);
+
+ return objref;
+ }
+
@MJI
public int toString____Ljava_lang_String_2 (MJIEnv env, int objref) {
Matcher matcher = getInstance(env, objref);
--- /dev/null
+/*
+ * 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.nio;
+
+import gov.nasa.jpf.util.test.TestJPF;
+import org.junit.Test;
+
+import java.util.Random;
+import java.util.Scanner;
+
+public class ByteBufferTest extends TestJPF {
+
+ /**
+ * This test case checks to see if the missing
+ * class java.nio.Buffer.<init>(IIII)V issue
+ * is resolved and fails otherwise
+ */
+ @Test
+ public void testBufferConstructor() {
+ if (verifyNoPropertyViolation()) {
+ Random random = new Random();
+ byte[] bytes = new byte[8];
+ random.nextBytes(bytes);
+ new Scanner(new String(bytes));
+ }
+ }
+
+}
import java.text.FieldPosition;
import java.text.NumberFormat;
import java.text.ParsePosition;
+import java.util.Locale;
import org.junit.Test;
assertTrue(format.isParseIntegerOnly());
format = NumberFormat.getNumberInstance();
assertFalse(format.isParseIntegerOnly());
+ format = NumberFormat.getNumberInstance(Locale.ENGLISH);
+ assertFalse(format.isParseIntegerOnly());
}
}
projects / jpf-core.git / commitdiff