---

VerifyReflection.java

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

import gov.nasa.arc.ase.jpf.jvm.reflection.Reflection;
import gov.nasa.arc.ase.jpf.TransitionResult;
import gov.nasa.arc.ase.jpf.jvm.bytecode.Instruction;

public class VerifyReflection extends Reflection {
  public Instruction executeStaticMethod(MethodInfo mi) {
    String name = mi.getFullName();

    if(name.equals("atLabel(Ljava/lang/String;)V")) {
//#ifdef BUCHI
      String label = getStringArgument(0);

      Labels.set(label, th.getPC(-1).getNext());
//#endif BUCHI
      
      return exit();
    }

    if(name.equals("atLabel(I)V")) {
//#ifdef BUCHI
      int label = getIntArgument(0);

      Labels.set(Integer.toString(label), th.getPC(-1).getNext());
//#endif BUCHI

      return exit();
    }

    if(name.equals("random(I)I"))
      return exit(ss.random(getIntArgument(0)+1));

    if(name.equals("randomBool()Z"))
      return exit(ss.random(2) != 0);

    if(name.equals("beginAtomic()V")) {
      th.list.ks.setAtomic();
      return exit();
    }

    if(name.equals("endAtomic()V")) {
      th.list.ks.clearAtomic();
      return exit();
    }

    if(name.equals("beginSoftAtomic()V")) {
      th.enterSoftAtomic();
      return exit();
    }

    if(name.equals("endSoftAtomic()V")) {
      th.leaveSoftAtomic();
      return exit();
    }

    if(name.equals("dumpState()V")) {
      System.out.println("dumping the state");
      ss.ks.log();
      return exit();
    }

    if(name.equals("assert(Z)V")) {
      th.list.ks.ss.violatedAssertion |= !Types.intToBoolean(th.getLocalVariable(0));

      return exit();
    }

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

    if(name.equals("random(I)I"))
      return false;

    if(name.equals("randomBool()Z"))
      return false;

    return super.isStaticMethodDeterministic(mi);
  }  
}

---