src/main/gov/nasa/jpf/vm/ArrayFields.java

   1 /*
   2  * Copyright (C) 2014, United States Government, as represented by the
   3  * Administrator of the National Aeronautics and Space Administration.
   4  * All rights reserved.
   5  *
   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
   9  *
  10  *        http://www.apache.org/licenses/LICENSE-2.0.
  11  *
  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.
  17  */
  18 package gov.nasa.jpf.vm;
  19
  20 import gov.nasa.jpf.JPFException;
  21
  22 import java.io.PrintStream;
  23
  24
  25
  26 /**
  27  *a Field (data value) store for array objects
  28  */
  29 public abstract class ArrayFields extends Fields {
  30
  31   int getNumberOfFieldsOrElements () {
  32     return arrayLength(); // we have no fields
  33   }
  34
  35   public abstract int arrayLength ();
  36
  37   @Override
  38   public abstract int getHeapSize ();
  39
  40   @Override
  41   public boolean isReferenceArray(){
  42     return false;
  43   }
  44
  45   public int getNumberOfFields() {
  46     // has none
  47     return 0;
  48   }
  49
  50   public abstract void copyElements (ArrayFields src, int srcPos, int dstPos, int len);
  51
  52   public void printElements( PrintStream ps, int max){
  53     int len = arrayLength();
  54     if (max < 0) max = len;
  55     int i;
  56     for (i=0; i<max; i++){
  57       if (i>0){
  58         ps.print(',');
  59       }
  60       printValue(ps, i);
  61     }
  62     if (i < len){
  63       ps.print("...");
  64     }
  65   }
  66
  67   protected abstract void printValue (PrintStream ps, int idx);
  68
  69   public abstract Object getValues();
  70
  71   @Override
  72   public boolean getBooleanValue (int pos) {
  73   // overridden by subclass
  74       throw new JPFException( "not a boolean[]");
  75   }
  76   @Override
  77   public byte getByteValue (int pos) {
  78     // overridden by subclass
  79     throw new JPFException( "not a byte[]");
  80   }
  81   @Override
  82   public char getCharValue (int pos) {
  83     // overridden by subclass
  84     throw new JPFException( "not a char[]");
  85   }
  86   @Override
  87   public short getShortValue (int pos) {
  88     // overridden by subclass
  89     throw new JPFException( "not a short[]");
  90   }
  91   @Override
  92   public int getIntValue (int pos) {
  93     // overridden by subclass
  94     throw new JPFException( "not an int[]");
  95   }
  96   @Override
  97   public long getLongValue (int pos) {
  98     // overridden by subclass
  99     throw new JPFException( "not a long[]");
 100   }
 101   @Override
 102   public float getFloatValue (int pos) {
 103     // overridden by subclass
 104     throw new JPFException( "not a float[]");
 105   }
 106   @Override
 107   public double getDoubleValue (int pos) {
 108     // overridden by subclass
 109     throw new JPFException( "not a double[]");
 110   }
 111   @Override
 112   public int getReferenceValue (int pos) {
 113     // overridden by subclass
 114     throw new JPFException( "not a reference array");
 115   }
 116
 117   @Override
 118   public void setBooleanValue (int pos, boolean newValue) {
 119     // overridden by subclass
 120     throw new JPFException( "not a boolean[]");
 121   }
 122   @Override
 123   public void setByteValue (int pos, byte newValue) {
 124     // overridden by subclass
 125     throw new JPFException( "not a byte[]");
 126   }
 127   @Override
 128   public void setCharValue (int pos, char newValue) {
 129     // overridden by subclass
 130     throw new JPFException( "not a char[]");
 131   }
 132   @Override
 133   public void setShortValue (int pos, short newValue) {
 134     // overridden by subclass
 135     throw new JPFException( "not a short[]");
 136   }
 137   @Override
 138   public void setIntValue (int pos, int newValue) {
 139     // overridden by subclass
 140     throw new JPFException( "not an int[]");
 141   }
 142   @Override
 143   public void setFloatValue (int pos, float newValue){
 144     // overridden by subclass
 145     throw new JPFException( "not a float[]");
 146   }
 147   @Override
 148   public void setLongValue (int pos, long newValue) {
 149     // overridden by subclass
 150     throw new JPFException( "not a long[]");
 151   }
 152   @Override
 153   public void setDoubleValue (int pos, double newValue){
 154     // overridden by subclass
 155     throw new JPFException( "not a double[]");
 156   }
 157   @Override
 158   public void setReferenceValue (int pos, int newValue){
 159     // overridden by subclass
 160     throw new JPFException( "not a reference array");
 161   }
 162
 163
 164   public boolean[] asBooleanArray () {
 165     // overridden by subclass
 166     throw new JPFException("not a boolean[]");
 167   }
 168   public byte[] asByteArray () {
 169     // overridden by subclass
 170     throw new JPFException("not a byte[]");
 171   }
 172   public char[] asCharArray () {
 173     // overridden by subclass
 174     throw new JPFException("not a char[]");
 175   }
 176   public char[] asCharArray (int offset, int length) {
 177     // overridden by subclass
 178     throw new JPFException("not a char[]");
 179   }
 180   public short[] asShortArray () {
 181     // overridden by subclass
 182     throw new JPFException("not a short[]");
 183   }
 184   public int[] asIntArray () {
 185     // overridden by subclass
 186     throw new JPFException("not a int[]");
 187   }
 188   public int[] asReferenceArray () {
 189     // overridden by subclass
 190     throw new JPFException("not a reference array");
 191   }
 192   public long[] asLongArray () {
 193     // overridden by subclass
 194     throw new JPFException("not a long[]");
 195   }
 196   public float[] asFloatArray () {
 197     // overridden by subclass
 198     throw new JPFException("not a float[]");
 199   }
 200   public double[] asDoubleArray () {
 201     // overridden by subclass
 202     throw new JPFException("not a double[]");
 203   }
 204
 205   @Override
 206   public int[] asFieldSlots() {
 207     throw new JPFException("array has no field slots");
 208   }
 209
 210 }