---

BanderaReflection.java

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

import gov.nasa.arc.ase.jpf.InternalErrorException;
import gov.nasa.arc.ase.jpf.jvm.Types;
import gov.nasa.arc.ase.jpf.jvm.MethodInfo;
import gov.nasa.arc.ase.jpf.jvm.bytecode.Instruction;

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

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

      return exit();
    }

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

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

    if(name.equals("choose()Z")) {
      return false;
    }

    return super.isStaticMethodDeterministic(mi);
  }  
}

---