---

TrailInfo.java

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

import de.fub.bytecode.generic.*;
import gov.nasa.arc.ase.jpf.*;
import gov.nasa.arc.ase.util.Debug;
import java.io.*;
import java.util.*;

class TrailInfo implements iTrailInfo {
  private int thread;
  private int random;
  private int line;
  private String classname;
  private List pcs = new ArrayList();

// ifdef BUCHI





//#endif BUCHI
  public TrailInfo(int thread, 
                   int random, 
                   int line,
                   String cname) {
    this.thread = thread;
    this.random = random;
    this.line = line;
    this.classname = cname;
  }  
  public void addPC(InstructionHandle pc) {
    pcs.add(pc);
  }  
  public void dump2file(BufferedWriter out) {
    Source source = Source.getSource(classname);
    if (source != null)
      try {
    source.dump2file(out,thread,line);
      } catch (IOException e) {}
  }  
  public String getClassname() {
    return this.classname;
  }  
  public int getLine() {
    return this.line;
  }  
  public int getRandom() {
    return this.random;
  }  
  public int getThread() {
    return this.thread;
  }  
  private void indent() {
    for (int i = 0;i < thread;i++) {
      Debug.print(Debug.WARNING, "           |");
    };
  }  
  public void print() {
    Source source = Source.getSource(classname);
    indent();
    if (source != null)
      source.print(thread, line); 
// ifdef BUCHI


//#endif BUCHI
    if (VirtualMachine.options.bytecode_dump) {
      for (int i = 0; i < pcs.size();i++) {
        indent();
        Debug.print(Debug.WARNING, "         ");
        Debug.println(Debug.WARNING, pcs.get(i).toString()); 
      }
      Debug.println(Debug.WARNING, "-------------------------------------------------------------------------------");
    }
  }  
  public String toString() {
    Source source = Source.getSource(classname);
    if (source == null)
      return "";
    StringBuffer sb = new StringBuffer();
// ifdef BUCHI


//#endif BUCHI
    for (int j = 0; j < thread; j++)
      sb.append(" |  ");
    sb.append(source.getLine(thread, line));
    if (VirtualMachine.options.bytecode_dump) {
      for (int i = 0; i < pcs.size();i++) {
    sb.append("\n");
    sb.append(pcs.get(i).toString());
      }
      sb.append("\n-------------------------------------------------------------------------------");
    }

    return sb.toString();
  }  
}

---