00001 package gov.nasa.arc.ase.jpf.jvm.bytecode; 00002 00003 //#ifdef BUCHI 00004 import gov.nasa.arc.ase.jpf.jvm.VirtualMachine; 00005 import gov.nasa.arc.ase.jpf.jvm.MethodInfo; 00006 import de.fub.bytecode.generic.InstructionHandle; 00007 import de.fub.bytecode.classfile.ConstantPool; 00008 //#endif BUCHI 00009 00010 public abstract class ReturnInstruction extends Instruction { 00011 //#endif BUCHI 00012 //#ifdef BUCHI 00013 00014 protected void init(InstructionHandle h, int o, MethodInfo m, ConstantPool cp) { 00015 super.init(h, o, m, cp); 00016 isObservable |= VirtualMachine.observableReturns.contains(mi.getCompleteName()); 00017 } 00018 }