---

PUTFIELD.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.Constants;
import de.fub.bytecode.generic.ConstantPoolGen;
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 PUTFIELD extends AbstractInstruction {
  private de.fub.bytecode.generic.PUTFIELD peer;

//#endif RACE
// ifdef RACE
  private void ANALYZE_execute(ThreadInfo th, int objref,
      DynamicArea da, ConstantPoolGen cpg, long value){
    if (Analyze.on()){
      String className = peer.getClassName(cpg);
      String fieldName = peer.getFieldName(cpg);
      LockStatus lock_status = da.getLockStatus(objref, fieldName);
      Analyze.debugPreAccess(th, className, fieldName, new ObjRef(objref),
      "PUTFIELD", value, lock_status);      
      lock_status.checkWrite(th, className, fieldName);
      Analyze.debugPostAccess(lock_status);
    }
  }  
  private void DEPEND_execute(ThreadInfo th, int objref){
    if (Depend.on()){
      Depend.addWrite(th, new ObjRef(objref));
    }
  }  
  public InstructionHandle execute(SystemState ss, KernelState ks, ThreadInfo th) {
    DynamicArea da = ks.dynamic_area;

    ConstantPoolGen cpg = th.getCPG();

    // size of the local stack
    int size = peer.consumeStack(cpg);
    
    // value to be put into the field
    long value;
    int objref;

// ifdef MARK_N_SWEEP
    if (size == 3) { // object reference + value
      // dword value
      value = th.peek2();
      objref = th.peek(2);
    } else {
      // word value
      value = th.peek();
      objref = th.peek(1);
    }

    da.setValue(objref, peer.getFieldName(cpg), value);

    th.pop(size);
//#else MARK_N_SWEEP











//#endif MARK_N_SWEEP
// ifdef RACE
    ANALYZE_execute(th, objref, da, cpg, value);
    DEPEND_execute(th, objref);
//#endif RACE

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

---