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.JPFException;
22 import java.io.PrintStream;
27 *a Field (data value) store for array objects
29 public abstract class ArrayFields extends Fields {
31 int getNumberOfFieldsOrElements () {
32 return arrayLength(); // we have no fields
35 public abstract int arrayLength ();
38 public abstract int getHeapSize ();
41 public boolean isReferenceArray(){
45 public int getNumberOfFields() {
50 public abstract void copyElements (ArrayFields src, int srcPos, int dstPos, int len);
52 public void printElements( PrintStream ps, int max){
53 int len = arrayLength();
54 if (max < 0) max = len;
56 for (i=0; i<max; i++){
67 protected abstract void printValue (PrintStream ps, int idx);
69 public abstract Object getValues();
72 public boolean getBooleanValue (int pos) {
73 // overridden by subclass
74 throw new JPFException( "not a boolean[]");
77 public byte getByteValue (int pos) {
78 // overridden by subclass
79 throw new JPFException( "not a byte[]");
82 public char getCharValue (int pos) {
83 // overridden by subclass
84 throw new JPFException( "not a char[]");
87 public short getShortValue (int pos) {
88 // overridden by subclass
89 throw new JPFException( "not a short[]");
92 public int getIntValue (int pos) {
93 // overridden by subclass
94 throw new JPFException( "not an int[]");
97 public long getLongValue (int pos) {
98 // overridden by subclass
99 throw new JPFException( "not a long[]");
102 public float getFloatValue (int pos) {
103 // overridden by subclass
104 throw new JPFException( "not a float[]");
107 public double getDoubleValue (int pos) {
108 // overridden by subclass
109 throw new JPFException( "not a double[]");
112 public int getReferenceValue (int pos) {
113 // overridden by subclass
114 throw new JPFException( "not a reference array");
118 public void setBooleanValue (int pos, boolean newValue) {
119 // overridden by subclass
120 throw new JPFException( "not a boolean[]");
123 public void setByteValue (int pos, byte newValue) {
124 // overridden by subclass
125 throw new JPFException( "not a byte[]");
128 public void setCharValue (int pos, char newValue) {
129 // overridden by subclass
130 throw new JPFException( "not a char[]");
133 public void setShortValue (int pos, short newValue) {
134 // overridden by subclass
135 throw new JPFException( "not a short[]");
138 public void setIntValue (int pos, int newValue) {
139 // overridden by subclass
140 throw new JPFException( "not an int[]");
143 public void setFloatValue (int pos, float newValue){
144 // overridden by subclass
145 throw new JPFException( "not a float[]");
148 public void setLongValue (int pos, long newValue) {
149 // overridden by subclass
150 throw new JPFException( "not a long[]");
153 public void setDoubleValue (int pos, double newValue){
154 // overridden by subclass
155 throw new JPFException( "not a double[]");
158 public void setReferenceValue (int pos, int newValue){
159 // overridden by subclass
160 throw new JPFException( "not a reference array");
164 public boolean[] asBooleanArray () {
165 // overridden by subclass
166 throw new JPFException("not a boolean[]");
168 public byte[] asByteArray () {
169 // overridden by subclass
170 throw new JPFException("not a byte[]");
172 public char[] asCharArray () {
173 // overridden by subclass
174 throw new JPFException("not a char[]");
176 public char[] asCharArray (int offset, int length) {
177 // overridden by subclass
178 throw new JPFException("not a char[]");
180 public short[] asShortArray () {
181 // overridden by subclass
182 throw new JPFException("not a short[]");
184 public int[] asIntArray () {
185 // overridden by subclass
186 throw new JPFException("not a int[]");
188 public int[] asReferenceArray () {
189 // overridden by subclass
190 throw new JPFException("not a reference array");
192 public long[] asLongArray () {
193 // overridden by subclass
194 throw new JPFException("not a long[]");
196 public float[] asFloatArray () {
197 // overridden by subclass
198 throw new JPFException("not a float[]");
200 public double[] asDoubleArray () {
201 // overridden by subclass
202 throw new JPFException("not a double[]");
206 public int[] asFieldSlots() {
207 throw new JPFException("array has no field slots");