---

Labels.java

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

//#ifdef BUCHI
import java.util.Hashtable;
import gov.nasa.arc.ase.jpf.jvm.bytecode.Instruction;
import gov.nasa.arc.ase.util.Debug;

public class Labels {
  private static Hashtable labels = new Hashtable();

  public static boolean isAt(String label, ThreadInfo th) {
    Instruction pc = (Instruction)labels.get(label);

    if(pc == null) return false;

    return th.getPC() == pc;
  }  
  public static void set(String label, Instruction pc) {
    if(!VirtualMachine.observableLabels.contains(label)) {
      Debug.println(Debug.MESSAGE, "Ignored label: " + label);
      return;
    }

    if(labels.containsKey(label)) return;

    labels.put(label, pc);
    pc.setObservable();
    Debug.println(Debug.MESSAGE, "New label: " + label);
  }  
}

---