---

AASTORE.java

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

import gov.nasa.arc.ase.jpf.jvm.ElementInfo;
import gov.nasa.arc.ase.jpf.jvm.SystemState;
import gov.nasa.arc.ase.jpf.jvm.KernelState;
import gov.nasa.arc.ase.jpf.jvm.ThreadInfo;
import de.fub.bytecode.classfile.ConstantPool;
import gov.nasa.arc.ase.util.Debug;
//#ifdef RACE

//#endif RACE

public class AASTORE extends Instruction {
  public Instruction execute(SystemState ss, KernelState ks, ThreadInfo th) {
    int value = th.pop();
    int index = th.pop();
    int arrayRef = th.pop();

    if(arrayRef == -1)
      return th.createAndThrowException("java.lang.NullPointerException");

    ElementInfo e = ks.da.get(arrayRef);

    if(e.outOfBounds(index))
      return th.createAndThrowException("java.lang.ArrayIndexOutOfBoundsException");

    e.setField(index, value);

//#ifdef RACE


//#endif RACE

    return th.getPC().getNext();
  }  
  public void setPeer(de.fub.bytecode.generic.Instruction i, ConstantPool cp) {
  }  
}

---