---

Step.java

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

import gov.nasa.arc.ase.jpf.jvm.bytecode.Instruction;
import gov.nasa.arc.ase.util.Left;

public class Step {
  public String classname;
  public int line;
  public Instruction[] bytecodes;
  public String[] comments;
  public int[] commentLocations;

  public Step(String cname, int l) {
    classname = cname;
    line = l;
    bytecodes = new Instruction[0];
    comments = new String[0];
    commentLocations = new int[0];
  }  
  public void addBytecode(Instruction i) {
    int l = bytecodes.length;
    Instruction[] n = new Instruction[l+1];

    System.arraycopy(bytecodes, 0, n, 0, l);
    bytecodes = n;
    bytecodes[l] = i;
  }  
  public void addComment(String c) {
    int l = comments.length;
    
    String[] nc = new String[l+1];
    System.arraycopy(comments, 0, nc, 0, l);
    comments = nc;

    int[] nl = new int[l+1];
    System.arraycopy(commentLocations, 0, nl, 0, l);
    commentLocations = nl;

    comments[l] = c;
    commentLocations[l] = bytecodes.length;
  }  
  public String toString() {
    StringBuffer sb = new StringBuffer();
    ClassInfo ci = ClassInfo.getClassInfo(classname);

    sb.append('\t');
    sb.append(Left.format(ci.getSourceFileName() + ":" + line, 20));
    sb.append(' ');
    sb.append(ci.getSource().get(line));
    sb.append('\n');

    if(VirtualMachine.options.bytecode_dump) {
      int j = 0, cl = comments.length;

      for(int i = 0, l = bytecodes.length; i < l; i++) {
    while(j < cl && i >= commentLocations[j]) {
      sb.append("\t\t// ");
      sb.append(comments[j++]);
      sb.append('\n');
    }
    sb.append("\t\t");
    sb.append(bytecodes[i].getPosition());
    sb.append(": ");
    sb.append(bytecodes[i].toString());
    sb.append('\n');
      }
      while(j < cl) {
    sb.append("\t\t// ");
    sb.append(comments[j++]);
    sb.append('\n');
      }
    } else {
      for(int j = 0, l = comments.length; j < l; j++) {
    sb.append("\t\t// ");
    sb.append(comments[j]);
    sb.append('\n');
      }
    }

    return sb.toString();
  }  
}

---