---

Area.java

package gov.nasa.arc.ase.jpf.jvm;

import gov.nasa.arc.ase.util.HashData;
import java.util.BitSet;

/**
 * This class defines an area. An area can be used for objects
 * in the DynamicArea or classes in the StaticArea.
 */
public abstract class Area implements Storable {
  /**
   * Contains the information for each element.
   */
  protected ElementInfo[] elements;

  /**
   * The number of elements. It can differ from the
   * size of the elements array.
   */
  private int nElements;

  /**
   * Last used element.
   */
  private int lastElement;

  /**
   * Reference of the kernel state this dynamic area is in.
   */
  public KernelState ks;

  /**
   * True if it's the static area.
   */
  public boolean isStatic;

  /**
   * Set of bits used to see which elements has changed.
   */
  public BitSet hasChanged;

  /**
   * Set if any element is changed (includes has been added or removed)
   */
  public boolean anyChanged;

  /**
   * Contains the data from the last call to get storing data.
   */
  public int[] data;
  
  /**
   * The number of entries per element.
   */

//#ifdef REFERENCE_COUNT

//#else REFERENCE_COUNT
  private static final int delta = 2;
  protected Area(Area a) {
    int l = a.elements.length;
    elements = new ElementInfo[l];
    for(int i = 0; i < l; i++)
      if(a.elements[i] != null) {
    elements[i] = (ElementInfo)a.elements[i].clone();
    elements[i].area = this;
    elements[i].index = i;
      } else
    elements[i] = null;

    nElements = a.nElements;
    lastElement = a.lastElement;
    ks = null;
    isStatic = a.isStatic;
    hasChanged = (BitSet)a.hasChanged.clone();
    anyChanged = a.anyChanged;
    l = a.data.length;
    data = new int[l];
    System.arraycopy(a.data, 0, data, 0, l);
  }  
//#endif REFERENCE_COUNT

  public Area(KernelState ks, boolean s) {
    this.ks = ks;
    elements = new ElementInfo[0];
    nElements = 0;
    lastElement = -1;
    isStatic = s;
    hasChanged = new BitSet();
    anyChanged = false;
    data = new int[0];
  }  
  protected void add(int index, ElementInfo e) {
    e.area = this;
    e.index = index;

    if(index >= elements.length) {
      ElementInfo[] n = new ElementInfo[index+10];
      System.arraycopy(elements, 0, n, 0, elements.length);
      elements = n;
    }

    if(index > lastElement) lastElement = index;

    elements[index] = e;
    nElements++;
    hasChanged.set(index);
    anyChanged = true;
    ks.data = null;
  }  
  public void backtrackTo(ArrayOffset storing, Object backtrack) {
    Object[] b = (Object[])backtrack;

    int length = storing.get();
    int l = elements.length;

    int s = length * delta;

    if(data.length != s+1) data = new int[s+1];

    if(s > 0)
      System.arraycopy(storing.data, storing.offset, data, 1, s);

    anyChanged = false;
    hasChanged = new BitSet();
    data[0] = length;

    lastElement = length-1;

    if(length != l) {
      if(l > length) l =  length;

      ElementInfo[] n = new ElementInfo[length];
      System.arraycopy(elements, 0, n, 0, l);

      elements = n;
    }

    for(int i = 0; i < length; i++) {
      ElementInfo e = elements[i];

      if(storing.peek() != 0) {
    if(e == null) {
      e = elements[i] = new ElementInfo();
      e.area = this;
      e.index = i;
    }

    e.backtrackTo(storing, b[i]);
      } else {
    elements[i] = null;

    storing.get();
    storing.get();
//#ifdef REFERENCE_COUNT

//#endif REFERENCE_COUNT
      }
    }
  }  
  public int count() {
    return nElements;
  }  
  public ElementInfo get(int index) {
    return elements[index];
  }  
  public Object getBacktrackData() {
    int length = elements.length;
    Object[] data = new Object[length];

//#ifdef RACE




//#endif RACE

    return data;
  }  
  public int[] getStoringData() {
    if(!anyChanged) return data;

    int length = lastElement+1;
    int size = length * delta;
    int s = data.length-1;

    if(s != size) {
      if(s > size) s = size;

      int[] n = new int[size+1];
      if(s > 0)
    System.arraycopy(data, 1, n, 1, s);
      data = n;
    }
    data[0] = length;

    for(int i = 0, j = 1; i < length; i++, j += delta) {
      if(hasChanged.get(i)) {
    if(elements[i] != null) {
      int[] eData = elements[i].getStoringData();
      System.arraycopy(eData, 0, data, j, delta);
    } else {
      data[j] = 0;
      data[j+1] = 0;
//#ifdef REFERENCE_COUNT

//#endif REFERENCE_COUNT
    }
      } else {
    if(elements[i] == null) {
      data[j] = 0;
      data[j+1] = 0;
//#ifdef REFERENCE_COUNT

//#endif REFERENCE_COUNT
    }
      }
    }

    anyChanged = false;
    hasChanged = new BitSet();

    return data;
  }  
  public void hash(HashData hd) {
    int length = elements.length;

    for(int i = 0; i < length; i++)
      if(elements[i] != null)
    elements[i].hash(hd);
  }  
  public int hashCode() {
    HashData hd = new HashData();

    hash(hd);

    return hd.getValue();
  }  
  protected void remove(int index) {
    elements[index].area = null;
    elements[index].index = -1;
    elements[index] = null;
    nElements--;

    hasChanged.set(index);
    anyChanged = true;

    if(lastElement == index)
      while(lastElement >= 0 && elements[lastElement] == null)
    lastElement--;
    ks.data = null;
  }  
  public void removeAll() {
    int l = elements.length;

    for(int i = 0; i < l; i++)
      if(elements[i] != null)
    remove(i);
  }  
}

---