---

FRETURN.java

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

import de.fub.bytecode.classfile.ConstantPool;
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 gov.nasa.arc.ase.jpf.jvm.MethodInfo;
import gov.nasa.arc.ase.util.Debug;

public class FRETURN extends ReturnInstruction {
  public Instruction execute(SystemState ss, KernelState ks, ThreadInfo th) {
    MethodInfo mi = th.getMethod();

    mi.leave(th);

    int value = th.pop();

    // removes the top frame
    th.popFrame();
    th.removeArguments(mi);

    // push the return value in the caller's stack frame
    th.push(value, false);

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

---