---

Expression.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.*;
import java.lang.reflect.*;

class Expression extends DepthFirstAdapter {
  private Translation translation;
  private Class currentType;

  public Expression(Translation t) {
    translation = t;
  }  
  public void caseAColonExp(AColonExp node) {
    inAColonExp(node);
    node.getExp().apply(this);
    outAColonExp(node);
  }  
  public void caseAQualifiedName(AQualifiedName node) {
    node.getName().apply(this);
    String id = node.getId().getText();

    if(currentType.isPrimitive())
      throw new JPFErrorException("Can't get field in primitive type");

    try {
      currentType = getField(currentType, id).getType();
      printGetField(id, currentType);
    } catch(NoSuchFieldException e) {
      throw new JPFErrorException("No field " + id + " in " + currentType.getName());
    }
  }  
  public void caseASimpleName(ASimpleName node) {
    String id = node.getId().getText();

    try {
      currentType = Class.forName(id);
      translation.out.print("s.getClass(\"" + id + "\")");
    } catch(ClassNotFoundException e) {
      try {
    currentType = Class.forName("java.lang." + id);
    translation.out.print("s.getClass(\"" + id + "\")");
      } catch(ClassNotFoundException ee) {
    if((currentType = (Class)translation.params.get(id)) != null) {
      translation.out.print(id);
    } else {
      translation.out.print(classNameOf(translation.thisType.getName()) + "$this");

      try {
        currentType = getField(translation.thisType, id).getType();
      } catch(NoSuchFieldException eee) {
        throw new JPFErrorException("No field " + id + " in " + translation.thisType.getName());
      }

      printGetField(id, currentType);
    }
      }
    }
  }  
  public void caseTRetVal(TRetVal node) {
    translation.out.print("t");

    printGetReturnValue(translation.thisMethod.getReturnType());
  }  
  private static String classNameOf(String name) {
    if(name.indexOf('.') == -1) return name;

    return name.substring(name.lastIndexOf('.')+1);
  }  
  public void defaultCase(Node node) {
    translation.out.print(node);
  }  
  private static Field getField(Class c, String f) throws NoSuchFieldException {
    while(c != null) {
      try {
    return c.getDeclaredField(f);
      } catch(NoSuchFieldException e) {
    c = c.getSuperclass();
      }
    }

    throw new NoSuchFieldException(f);
  }  
  private void printGetField(String id, Class type) {
    translation.out.print(".get");
    if(type.isPrimitive()) {
      if(type == Boolean.TYPE) {
    translation.out.print("Boolean");
      } else if(type == Character.TYPE) {
    translation.out.print("Character");
      } else if(type == Byte.TYPE) {
    translation.out.print("Byte");
      } else if(type == Short.TYPE) {
    translation.out.print("Short");
      } else if(type == Integer.TYPE) {
    translation.out.print("Int");
      } else if(type == Long.TYPE) {
    translation.out.print("Long");
      } else if(type == Float.TYPE) {
    translation.out.print("Float");
      } else if(type == Double.TYPE) {
    translation.out.print("Double");
      }
    } else
      translation.out.print("Object");
    translation.out.print("Field(\"" + id + "\")");
  }  
  private void printGetReturnValue(Class type) {
    translation.out.print(".get");
    if(type.isPrimitive()) {
      if(type == Boolean.TYPE) {
    translation.out.print("Boolean");
      } else if(type == Character.TYPE) {
    translation.out.print("Character");
      } else if(type == Byte.TYPE) {
    translation.out.print("Byte");
      } else if(type == Short.TYPE) {
    translation.out.print("Short");
      } else if(type == Integer.TYPE) {
    translation.out.print("Int");
      } else if(type == Long.TYPE) {
    translation.out.print("Long");
      } else if(type == Float.TYPE) {
    translation.out.print("Float");
      } else if(type == Double.TYPE) {
    translation.out.print("Double");
      }
    } else
      translation.out.print("Object");
    translation.out.print("ReturnValue()");
  }  
}

---