import gov.nasa.jpf.vm.MJIEnv;
import gov.nasa.jpf.vm.NativePeer;
import gov.nasa.jpf.annotation.MJI;

import my.util.TeleTYpewriter;

/**
 * Native peer class for TeleTYpewriter class.
 *
 * @author Franck van Breugel
 */
public class JPF_my_util_TeleTYpewriter extends NativePeer {
    /**
     * Prints "Invoking isTTY" and executes the native method isTTY in the host JVM, and returns its result.
     *
     * @param env MJI environment.
     * @param clsObjRef JPF's index of object on which the method isTTY is invoked.
     * @return result of the native method call isTTY.
    */
    @MJI
    public boolean isTTY____Z(MJIEnv env, int clsObjRef) {
	System.out.println("Invoking isTTY");
        return TeleTYpewriter.isTTY();
    }

    /**
     * Prints "Invoking getTTYName", executes the native method getTTYName in the host JVM, and returns its result as an int representing the String in JPF.
     *
     * @param env MJI environment.
     * @param clsObjRef JPF's index of object on which the method getTTYName is invoked.
     * @return result of the native method getTTYName as an int.
    */
    @MJI
    public int getTTYName____Ljava_lang_String_2(MJIEnv env, int clsObjRef) {
	System.out.println("Invoking getTTYName");
        String name = TeleTYpewriter.getTTYName();
        int ref = env.newString(name);
        return ref;
    }
}