---

IASTORE.java

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

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

public class IASTORE extends AbstractInstruction {
  private de.fub.bytecode.generic.IASTORE 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), "IASTORE", 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;

    int value = th.pop();
    int index = th.pop();
    int arrayref = th.pop();

    da.setValue(arrayref, index, value);

// 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.IASTORE)i;
  }  
}

---