---

AALOAD.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 AALOAD extends AbstractInstruction {
  private de.fub.bytecode.generic.AALOAD peer;

//#endif RACE
// ifdef RACE
  private void ANALYZE_execute(ThreadInfo th, int arrayref,
      DynamicArea da, int index){
    if (Analyze.on()) {
      LockStatus lock_status = da.getLockStatus(arrayref);
      Analyze.debugPreAccess(th, "Object[]", Integer.toString(index),
      new ObjRef(arrayref), "AALOAD", da.getValue(arrayref, index), lock_status);      
      lock_status.checkReadArray(th, index);
      Analyze.debugPostAccess(lock_status);
    }
  }  
  public InstructionHandle execute(SystemState ss, KernelState ks, ThreadInfo th) {
    DynamicArea da = ks.dynamic_area;           // this is the dynamic area

    // reads the arguments from the stack
    int index = th.pop();
    int arrayref = th.pop();

    // transforms an index in the array into a value
    int value = (int)da.getValue(arrayref, index);

    // and pushes the value onto the stack
    th.push(value);
// ifdef MARK_N_SWEEP
    th.setOperandRef();
//#endif MARK_N_SWEEP

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

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

---