JVMPathEntry.java Source File

00001 package gov.nasa.arc.ase.jpf.jvm;
00002 
00003 import gov.nasa.arc.ase.jpf.Engine;
00004 import gov.nasa.arc.ase.jpf.Path;
00005 import gov.nasa.arc.ase.util.Debug;
00006 import java.io.Serializable;
00007 
00008 public class JVMPathEntry {
00009   
00010   int line;
00011   String classname;
00012   String file;
00013   int thread;
00014   int random;
00015 
00016   public JVMPathEntry(int line, String cname, int thread, int random) {
00017     this.line = line;
00018     this.classname = cname;
00019     this.file = Source.getSourceFileName(cname);
00020     this.thread = thread;
00021     this.random = random;
00022   }  
00023 }