---

JavaLangMathReflection.java

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

import gov.nasa.arc.ase.jpf.jvm.*;
import gov.nasa.arc.ase.jpf.jvm.bytecode.Instruction;

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

    if(name.equals("<clinit>()V")) {
      return exit();
    }

    if(name.equals("pow(DD)D")) {
      // doubles take 2 slots on the stack each, hence 0 and 2
      return exit(java.lang.Math.pow(getDoubleArgument(0),
                                     getDoubleArgument(2)));        
    }

    if(name.equals("max(DD)D")) {
      // doubles take 2 slots on the stack each, hence 0 and 2
      return exit(java.lang.Math.max(getDoubleArgument(0),
                                     getDoubleArgument(2)));        
    }

    if(name.equals("max(FF)F")) {
      return exit(java.lang.Math.max(getFloatArgument(0),
                                     getFloatArgument(1)));     
    }

    if(name.equals("max(II)I")) {
      return exit(java.lang.Math.max(getIntArgument(0),
                                     getIntArgument(1)));       
    }

    if(name.equals("max(JJ)J")) {
      // longs take 2 slots on the stack each, hence 0 and 2
      return exit(java.lang.Math.max(getLongArgument(0),
                                     getLongArgument(2)));      
    }

    if(name.equals("min(DD)D")) {
      // doubles take 2 slots on the stack each, hence 0 and 2
      return exit(java.lang.Math.min(getDoubleArgument(0),
                                     getDoubleArgument(2)));        
    }

    if(name.equals("min(FF)F")) {
      return exit(java.lang.Math.min(getFloatArgument(0),
                                     getFloatArgument(1)));     
    }

    if(name.equals("min(II)I")) {
      return exit(java.lang.Math.min(getIntArgument(0),
                                     getIntArgument(1)));       
    }

    if(name.equals("min(JJ)J")) {
      // longs take 2 slots on the stack each, hence 0 and 2
      return exit(java.lang.Math.min(getLongArgument(0),
                                     getLongArgument(2)));      
    }

    return super.executeStaticMethod(mi);
  }  
}

---