---

JimpleTrace Class Reference

List of all members.

Public Methods
	JimpleTrace (BirTrace birTrace)
JimpleStore	getLastStore ()
Stmt[]	getStatements ()
JimpleStore	getStore (int stmtIndex)
TransSystem	getTransSystem ()
String	getTrapName ()
Stmt	getTrapStmt ()
boolean	isComplete ()
boolean	isDepthExceeded ()
boolean	isLimitViolation ()
boolean	isOutOfMemory ()
boolean	isVectorExceeded ()
boolean	isVerified ()
void	print ()
void	print (PrintWriter out, boolean showVars)
Private Methods
String	evalExpr (Expr expr, int stmtIndex)
Static Private Methods
String	pad (Object o, int width)
Private Attributes
boolean	verified
boolean	completed
boolean	limitviolation
boolean	outofmemory
boolean	depthexceeded
boolean	vectorexceeded
Stmt[]	stmts
String	trapName
Stmt	trapStmt
TransSystem	system
BirTrace	birTrace
Hashtable	threadOfStmt = new Hashtable()
int[]	stateIndex

---

Detailed Description

A JimpleTrace is either a sequence of Jimple Stmt's, possibly followed by a Stmt causing a trap (and the name of the trap), an indication of an incomplete model check (e.g., due to insufficient memory), an indication of a model resource limit violation, or simply a token indicating the property was verified.

This class can be used to map the output of a verifier (once interpreted as a sequence of transformations) back to a sequence of actions in the Jimple.

Definition at line 62 of file JimpleTrace.java.

---

Constructor & Destructor Documentation

JimpleTrace::JimpleTrace (  BirTrace   birTrace )  [inline]

Build a JimpleTrace from a BIR trace. Definition at line 105 of file JimpleTrace.java.

---

Member Function Documentation

Stmt [] JimpleTrace::getStatements (    )  [inline]

Get Jimple Stmts executed in the trace. If a Stmt caused a trap, it will be included as the last element of this array. Definition at line 184 of file JimpleTrace.java.

JimpleStore JimpleTrace::getStore (  int   stmtIndex )  [inline]

Get the store at a particular statement. Parameters: stmtIndex   the index of the statement (between 0 and the number of statements in the trace) Returns: the JimpleStore representing the variable values just before that Stmt (if there are N statements, the store at statement index N represents the final state, after all Stmts). Definition at line 193 of file JimpleTrace.java. Referenced by print().

String JimpleTrace::getTrapName (    )  [inline]

Get the name of the trap (returns null if no trap occurred in trace). Definition at line 202 of file JimpleTrace.java.

Stmt JimpleTrace::getTrapStmt (    )  [inline]

Get the Stmt that caused the trap (returns null if no trap in trace). Definition at line 206 of file JimpleTrace.java.

boolean JimpleTrace::isComplete (    )  [inline]

Was the failure due to the checker (e.g., out of memory)? Definition at line 211 of file JimpleTrace.java.

boolean JimpleTrace::isDepthExceeded (    )  [inline]

Was the failure due to a checker exceeding its depth bound? Definition at line 215 of file JimpleTrace.java.

boolean JimpleTrace::isLimitViolation (    )  [inline]

Was the failure due to a model resource limit violation? Definition at line 220 of file JimpleTrace.java.

boolean JimpleTrace::isOutOfMemory (    )  [inline]

Was the failure due to checker running out of memory? Definition at line 224 of file JimpleTrace.java.

boolean JimpleTrace::isVectorExceeded (    )  [inline]

Was the failure due to a checker exceeding its state vector size? Definition at line 228 of file JimpleTrace.java.

boolean JimpleTrace::isVerified (    )  [inline]

Was the property verified (i.e., hold on the model)? Definition at line 233 of file JimpleTrace.java.

String JimpleTrace::pad (  Object   o, int   width )  [inline, static, private]

Format object in field of given width Definition at line 238 of file JimpleTrace.java. Referenced by print().

void JimpleTrace::print (  PrintWriter   out, boolean   showVars )  [inline]

Print a JimpleTrace. Parameters: out   PrintWriter to send output to showVars   show variable values (if false, only Stmts are displayed) Definition at line 252 of file JimpleTrace.java.

---

Member Data Documentation

int [] JimpleTrace::stateIndex [private]

Maps Stmt index to state index in trace. The BIR trace is a sequence of BIR transformations, each of which may contain several actions, and not all actions map back to Jimple Stmts. The BIR trace contains a BirState for each action index (i.e., a starting BirState, and the BirState after each action in the BirTrace). We must be able to retrieve the BirState for a given Jimple Stmt in the trace. The stateIndex array maintains this mapping. The element stateIndex[jimpleStmtNum] gives the index of the BirState of the system in the state just *before* the given Jimple Stmt is executed. For example, suppose the BIR trace contains actions A1,..,A4, but that only A2 and A4 had source statements (call them S1 and S2). Then stateIndex[] would be { 0, 2, 4 }. So stateIndex[1] = 2 since the state of the system after the first Stmt (S1) is the BirState after the second action (A2) is executed. Definition at line 98 of file JimpleTrace.java.

---

The documentation for this class was generated from the following file:

• JimpleTrace.java

---