---

Instruction.java

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

import gov.nasa.arc.ase.jpf.InternalErrorException;
import de.fub.bytecode.classfile.ConstantPool;
import de.fub.bytecode.generic.InstructionHandle;
import gov.nasa.arc.ase.jpf.jvm.MethodInfo;
import gov.nasa.arc.ase.jpf.jvm.ThreadInfo;
import gov.nasa.arc.ase.jpf.jvm.SystemState;
import gov.nasa.arc.ase.jpf.jvm.KernelState;
import gov.nasa.arc.ase.util.Debug;
//#ifdef JDK11


//#else JDK11
import java.util.List;
import java.util.ArrayList;
//#endif JDK11
//#ifdef BUCHI
import gov.nasa.arc.ase.jpf.jvm.VirtualMachine;
//#endif BUCHI

public abstract class Instruction {
  protected static List Unimplemented = new ArrayList();
  protected int position;
  protected int offset;
  protected MethodInfo mi;
  protected String asString;
//#ifdef BUCHI
  protected boolean isObservable;
//#endif BUCHI
  public static Instruction create(InstructionHandle h, int o, MethodInfo m, ConstantPool cp) {
    Instruction i = null;
    String name = null;
    try {
      name = h.getInstruction().getClass().getName();
      if(!name.startsWith("de.fub.bytecode.generic.")) {
    Debug.println(Debug.ERROR, "panic: instruction not in the right package");
    Debug.println(Debug.ERROR, "Quitting...");
        throw new InternalErrorException(""); //System.exit(0);
      }
      name = "gov.nasa.arc.ase.jpf.jvm.bytecode." + name.substring(24);
      Class clazz = Class.forName(name);
      
      i = (gov.nasa.arc.ase.jpf.jvm.bytecode.Instruction)clazz.newInstance();
      i.init(h, o, m, cp);
    } catch(ClassNotFoundException e) {
      if(!Unimplemented.contains(name)) {
    Unimplemented.add(name);
    Debug.println(Debug.WARNING,"warning: unimplemented bytecode instruction: " +
             name.substring(34));
      }
    } catch(Exception e) {
      throw new InternalErrorException("creation of instruction " +
      name.substring(34) + " failed");
    }

    return i;
  }  
  public boolean examine(SystemState ss, KernelState ks, ThreadInfo th) {
    return false;
  }  
  public abstract Instruction execute(SystemState ss, KernelState ks, ThreadInfo th);  
  public Instruction getNext() {
    return mi.getInstruction(offset+1);
  }  
  public int getOffset() {
    return offset;
  }  
  public int getPosition() {
    return position;
  }  
  protected void init(InstructionHandle h, int o, MethodInfo m, ConstantPool cp) {
    position = h.getPosition();
    offset = o;
    mi = m;
    asString = h.getInstruction().toString(cp);
    setPeer(h.getInstruction(), cp);
//#ifdef BUCHI
    isObservable = VirtualMachine.observablePositions.contains(mi.getCompleteName() + ":" + position);
//#endif BUCHI
  }  
  public boolean isExecutable(SystemState ss, KernelState ks, ThreadInfo th) {
    return true;
  }  
//#ifdef COVERAGE















//#endif COVERAGE

//#ifdef BUCHI

  public boolean isObservable() {
    return isObservable;
  }  
  public void setObservable() {
    isObservable = true;
  }  
//#endif BUCHI

  protected abstract void setPeer(de.fub.bytecode.generic.Instruction i, ConstantPool cp);  
  public String toString() {
    return asString;
  }  
}

---