---

VerifyReflection.java

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

import de.fub.bytecode.generic.InstructionHandle;
import gov.nasa.arc.ase.jpf.jvm.reflection.Reflection;
import gov.nasa.arc.ase.jpf.TransitionResult;

public class VerifyReflection extends Reflection {
  public InstructionHandle executeStaticMethod(MethodInfo mi, boolean atomic) {
    String name = mi.getFullName();

    if(name.equals("gov.nasa.arc.ase.jpf.jvm.Verify.atLabel(Ljava/lang/String;)V")) {
      String label = da.convert2String(th.getLocalVariable(0));

      Labels.set(label, th.getCurrentMethod().getFullName(), th.getPC().getNext().getPosition());
      
      return exit();
    }

    if(name.equals("gov.nasa.arc.ase.jpf.jvm.Verify.atLabel(I)V")) {
      int label = th.getLocalVariable(0);

      Labels.set(new Integer(label).toString(), th.getCurrentMethod().getFullName(), th.getPC().getNext().getPosition());
      
      return exit();
    }

    if(name.equals("gov.nasa.arc.ase.jpf.jvm.Verify.random(I)I"))
      return exit(th.doRandom(th.getLocalVariable(0)+1, ss.getScheduler()));

    if(name.equals("gov.nasa.arc.ase.jpf.jvm.Verify.randomBool()Z"))
      return exit(th.doRandom(2, ss.getScheduler()));

    if(name.equals("gov.nasa.arc.ase.jpf.jvm.Verify.beginAtomic()V")) {
      TransitionResult.setAtomic();
      return exit();
    }

    if(name.equals("gov.nasa.arc.ase.jpf.jvm.Verify.endAtomic()V")) {
      TransitionResult.clearAtomic();
      return exit();
    }

    if(name.equals("gov.nasa.arc.ase.jpf.jvm.Verify.atomicMethod()V")) {
      th.executeAtomicMethod(-1);
      return exit();
    }

    if(name.equals("gov.nasa.arc.ase.jpf.jvm.Verify.assert(Z)V")) {
      TransitionResult.assertionViolation(!Types.intToBoolean(th.getLocalVariable(0)));
      return exit();
    }

    return super.executeStaticMethod(mi, atomic);
  }  
  public boolean isStaticMethodDeterministic(MethodInfo mi) {
    String name = mi.getFullName();

    if(name.equals("gov.nasa.arc.ase.jpf.jvm.Verify.random(I)I"))
      return false;

    if(name.equals("gov.nasa.arc.ase.jpf.jvm.Verify.randomBool()Z"))
      return false;

    return super.isStaticMethodDeterministic(mi);
  }  
}

---