gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment

Class OutputTable

java.lang.Object

gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.Table<java.lang.Integer,V>

gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StaticTable<java.lang.Integer>

gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.OutputTable

public class OutputTable
extends StaticTable<java.lang.Integer>

An Environment table that holds all slots that needs to be populated after successful symmetrization of the region. Vars associated with the slot are the last instance discovered for the slots.

Field Summary

Fields inherited from class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.Table

label1, label2, table, tableName

Constructor Summary

Constructors

Constructor and Description
OutputTable(boolean isMethodRegion)
OutputTable(com.ibm.wala.ssa.IR ir, boolean isMethodRegion, SlotParamTable slotParamTable, InputTable inputTable, Stmt stmt)
OutputTable(com.ibm.wala.ssa.IR ir, boolean isMethodRegion, SlotParamTable slotParamTable, InputTable inputTable, Stmt stmt, Pair<java.lang.Integer,java.lang.Integer> firstDefLastDef)

Method Summary

Modifier and Type	Method and Description
private void	computeMethodOutput(com.ibm.wala.ssa.IR ir) All normal predecessors of an exit node must have a return as the last instruction.
private void	computeOutputVars(com.ibm.wala.ssa.IR ir, SlotParamTable slotParamTable, InputTable inputTable, Pair<java.lang.Integer,java.lang.Integer> firstDefLastDef) outputVars are computed by finding the maximum wala var for each stackSlot and those that are not input or constants.
private java.util.List<com.ibm.wala.ssa.SSAReturnInstruction>	findAllReturns(com.ibm.wala.ssa.IR ir)
boolean	isOutputVar(int var)
void	print() Basic print of the table.

Methods inherited from class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StaticTable

getKeys, mergeTable, updateKey

Methods inherited from class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.Table

add, lookup, mergeTable, remove

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

OutputTable

public OutputTable(com.ibm.wala.ssa.IR ir,
                   boolean isMethodRegion,
                   SlotParamTable slotParamTable,
                   InputTable inputTable,
                   Stmt stmt)

OutputTable

public OutputTable(com.ibm.wala.ssa.IR ir,
                   boolean isMethodRegion,
                   SlotParamTable slotParamTable,
                   InputTable inputTable,
                   Stmt stmt,
                   Pair<java.lang.Integer,java.lang.Integer> firstDefLastDef)

OutputTable

public OutputTable(boolean isMethodRegion)

Method Detail

computeMethodOutput

private void computeMethodOutput(com.ibm.wala.ssa.IR ir)

All normal predecessors of an exit node must have a return as the last instruction. If the first return has no use then the method is void.

Parameters:

ir -

findAllReturns

private java.util.List<com.ibm.wala.ssa.SSAReturnInstruction> findAllReturns(com.ibm.wala.ssa.IR ir)

computeOutputVars

private void computeOutputVars(com.ibm.wala.ssa.IR ir,
                               SlotParamTable slotParamTable,
                               InputTable inputTable,
                               Pair<java.lang.Integer,java.lang.Integer> firstDefLastDef)

outputVars are computed by finding the maximum wala var for each stackSlot and those that are not input or constants.

print

public void print()

Description copied from class: Table

Basic print of the table. inside the table.

Overrides:

print in class Table<java.lang.Integer,java.lang.Integer>

isOutputVar

public boolean isOutputVar(int var)