---

INVOKESTATIC.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.ConstantPoolGen;
import de.fub.bytecode.generic.InstructionHandle;
import gov.nasa.arc.ase.util.Debug;

public class INVOKESTATIC extends AbstractInstruction {
  private de.fub.bytecode.generic.INVOKESTATIC peer;

  /*********************************************************************/
  /* looks for nondeterminism */
  public boolean examine(SystemState ss, KernelState ks, ThreadInfo th) {
    ConstantPoolGen cpg = th.getCPG();

    String className  = peer.getClassName(cpg);
    String sig        = peer.getSignature(cpg);
    String methodName = peer.getMethodName(cpg);

    ClassInfo ci = JPFVM.getJPFVM().getClass(className);
    return !ci.isStaticMethodDeterministic(ss, ks, th, methodName+sig);
  }  
  /*********************************************************************/


  public InstructionHandle execute(SystemState ss, KernelState ks, ThreadInfo th) {
    DynamicArea da = ks.dynamic_area;
    StaticArea sa = ks.static_area;

    ConstantPoolGen cpg = th.getCPG();

    String className  = peer.getClassName(cpg);
    String sig        = peer.getSignature(cpg);
    String methodName = peer.getMethodName(cpg);

    ClassInfo ci = JPFVM.getJPFVM().getClass(className);
    if (!ks.static_area.hasClass(className)) {
      ks.static_area.addClass(ci);
      return ci.initialize(ss, ks, th);
    }

    return ci.executeStaticMethod(ss, ks, th, methodName+sig);
  }  
 public boolean isExecutable(SystemState ss, KernelState ks, ThreadInfo th) {
    ConstantPoolGen cpg = th.getCPG();

    String className  = peer.getClassName(cpg);
    String sig        = peer.getSignature(cpg);
    String methodName = peer.getMethodName(cpg);

    ClassInfo ci = JPFVM.getJPFVM().getClass(className);
    return ci.isStaticMethodExecutable(ss, ks, th, methodName+sig);
  }  
  public void setPeer(de.fub.bytecode.generic.Instruction i) {
    peer = (de.fub.bytecode.generic.INVOKESTATIC)i;
  }  
}

---