---

AASTORE.java

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

import de.fub.bytecode.generic.InstructionHandle;
import gov.nasa.arc.ase.jpf.*;
import gov.nasa.arc.ase.jpf.jvm.*;
import gov.nasa.arc.ase.util.Debug;
// ifdef RACE
import gov.nasa.arc.ase.jpf.jvm.runtime.*;
//#endif RACE

public class AASTORE extends AbstractInstruction {
  private de.fub.bytecode.generic.AASTORE peer;

//#endif RACE
// ifdef RACE
  private void ANALYZE_execute(ThreadInfo th, int arrayref,
      DynamicArea da, int index, long value){
    if (Analyze.on()) {
      LockStatus lock_status = da.getLockStatus(arrayref);
      Analyze.debugPreAccess(th, "Object[]", Integer.toString(index),
      new ObjRef(arrayref), "AASTORE", value, lock_status);      
      lock_status.checkWriteArray(th, index);
      Analyze.debugPostAccess(lock_status);
    }
  }  
  public InstructionHandle execute(SystemState ss, KernelState ks, ThreadInfo th) {
    DynamicArea da = ks.dynamic_area;

// ifdef MARK_N_SWEEP
    int value = th.peek();
    int index = th.peek(1);
    int arrayref = th.peek(2);

    // sets the value into the array
    da.setValue(arrayref, index, value);
    th.pop(3);
//#else MARK_N_SWEEP






//#endif MARK_N_SWEEP

// ifdef RACE
    ANALYZE_execute(th, arrayref, da, index, value);
//#endif RACE

    return th.getPC().getNext();
  }  
  public void setPeer(de.fub.bytecode.generic.Instruction i) {
    peer = (de.fub.bytecode.generic.AASTORE)i;
  }  
}

---