---

PredicateCompiler.java

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

//#ifdef BUCHI && BANDERA
import edu.ksu.cis.bandera.specification.predicate.lexer.*;
import edu.ksu.cis.bandera.specification.predicate.node.*;
import edu.ksu.cis.bandera.specification.predicate.parser.*;
import gov.nasa.arc.ase.jpf.JPFErrorException;
import java.io.*;
import java.lang.reflect.*;

public class PredicateCompiler {
  public static void compile(String fname, String cname, String mname) {
    Reader in = null;
    if(fname.equals("-"))
      in = new InputStreamReader(System.in);
    else if(fname.endsWith(".p")) {
      try {
    in = new FileReader(fname);
      } catch(FileNotFoundException e) {
    throw new JPFErrorException("Can't open file: " + fname);
      }
    } else
      in = new StringReader(fname);

    Parser p =
      new Parser(
      new Lexer(
        new PushbackReader(in, 1024)));

    Start tree;
    try {
      tree = p.parse();
    } catch(IOException e) {
      throw new JPFErrorException("io error: " + e.getMessage());
    } catch(LexerException e) {
      throw new JPFErrorException("lexer error: " + e.getMessage());
    } catch(ParserException e) {
      throw new JPFErrorException("parse error: " + e.getMessage());
    }

    try {
      Class c = cname == null ? null : Class.forName(cname);
      Method m = mname == null ? null : getMethod(c, mname);
      tree.apply(
      new Translation(c, m));
    } catch(ClassNotFoundException e) {
      throw new JPFErrorException("class not found: " + cname);
    } catch(NoSuchMethodException e) {
      throw new JPFErrorException("method not found: " + mname);
    }
  }  
  private static Method getMethod(Class c, String m) throws NoSuchMethodException {
    while(c != null) {
      Method[] ms = c.getDeclaredMethods();

      for(int i = 0, l = ms.length; i < l; i++)
    if(Signature.getSignature(ms[i]).equals(m))
      return ms[i];

      c = c.getSuperclass();
    }

    throw new NoSuchMethodException(m);
  }  
  public static void main(String[] args) {
    switch(args.length) {
      case 1: compile(args[0], null, null); break;
      case 2: compile(args[0], args[1], null); break;
      case 3: compile(args[0], args[1], args[2]); break;

      default:
    usage();
    }
  }  
  public static void usage() {
    System.err.println("usage:");
    System.err.println("\t java gov.nasa.arc.ase.jpf.jvm.tool.PredicateCompiler <filename> [<classname> [<methodname>]]");
    System.exit(1);
  }  
}

---