public class Source extends Object
Modifier and Type | Field and Description |
---|---|
protected String |
fname |
protected String[] |
lines |
protected gov.nasa.jpf.util.Source.SourceRoot |
root |
Modifier | Constructor and Description |
---|---|
protected |
Source(gov.nasa.jpf.util.Source.SourceRoot root,
String fname) |
Modifier and Type | Method and Description |
---|---|
String |
getLine(int i)
this is our sole purpose in life - answer line strings
line index is 1-based
|
int |
getLineCount() |
String |
getPath() |
static Source |
getSource(String relPathName) |
static void |
init(Config config) |
protected void |
loadLines(InputStream is) |
protected gov.nasa.jpf.util.Source.SourceRoot root
protected String fname
protected String[] lines
protected Source(gov.nasa.jpf.util.Source.SourceRoot root, String fname)
public static void init(Config config)
protected void loadLines(InputStream is) throws IOException
IOException
public String getLine(int i)
public int getLineCount()
public String getPath()