---

Parameters.java

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

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

class Parameters extends DepthFirstAdapter {
  private Translation translation;
  private StringBuffer sb;

  public Parameters(Translation t) {
    translation = t;
  }  
  public void caseAInstanceParams(AInstanceParams node) {
    translation.out.print(", Reference " + classNameOf(translation.thisType.getName()) + "$this");
    if(node.getCpl() != null) {
      node.getCpl().apply(this);
    }
  }  
  public void caseAParamParamList(AParamParamList node) {
    sb = new StringBuffer();
    node.getName().apply(this);
    String type = sb.toString();

    sb = new StringBuffer();
    node.getId().apply(this);
    String name = sb.toString();

    translation.out.print(", Reference " + name);

    try {
      translation.params.put(name, Class.forName(type));
    } catch(ClassNotFoundException e) {
      try {
    translation.params.put(name, Class.forName("java.lang." + type));
      } catch(ClassNotFoundException ee) {
    throw new JPFErrorException("class not found: " + type);
      }
    }
  }  
  public void caseAParamsParamList(AParamsParamList node) {
    sb = new StringBuffer();
    node.getName().apply(this);
    String type = sb.toString();

    sb = new StringBuffer();
    node.getId().apply(this);
    String name = sb.toString();

    translation.out.print(", " + type + " " + name);

    try {
      translation.params.put(name, Class.forName(type));
    } catch(ClassNotFoundException e) {
      try {
    translation.params.put(name, Class.forName("java.lang." + type));
      } catch(ClassNotFoundException ee) {
    throw new JPFErrorException("class not found: " + type);
      }
    }
  }  
  public void caseAQualifiedName(AQualifiedName node) {
    node.getName().apply(this);
    sb.append(".");
    sb.append(node.getId().getText());
  }  
  public void caseASimpleName(ASimpleName node) {
    sb.append(node.getId().getText());
  }  
  public void caseTId(TId node) {
    sb.append(node.getText());
  }  
  private static String classNameOf(String name) {
    if(name.indexOf('.') == -1) return name;

    return name.substring(name.lastIndexOf('.')+1);
  }  
}

---