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

Class FieldSSAVisitor

java.lang.Object

gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprMapVisitor

gov.nasa.jpf.symbc.veritesting.ast.visitors.AstMapVisitor

gov.nasa.jpf.symbc.veritesting.ast.visitors.FixedPointAstMapVisitor

gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess.FieldSSAVisitor

All Implemented Interfaces:

AstVisitor<Stmt>, ExprVisitor<za.ac.sun.cs.green.expr.Expression>

public class FieldSSAVisitor
extends FixedPointAstMapVisitor

Field Summary

Fields

Modifier and Type	Field and Description
private DynamicRegion	dynRegion
(package private) static int	FIELD_SUBSCRIPT_BASE
private static int	fieldExceptionNumber
private GlobalSubscriptMap	gsm
FieldSubscriptMap	psm
private gov.nasa.jpf.vm.ThreadInfo	ti

Fields inherited from class gov.nasa.jpf.symbc.veritesting.ast.visitors.FixedPointAstMapVisitor

firstException, instantiatedRegion, somethingChanged

Fields inherited from class gov.nasa.jpf.symbc.veritesting.ast.visitors.AstMapVisitor

eva, exprVisitor

Constructor Summary

Constructors

Constructor and Description
FieldSSAVisitor(gov.nasa.jpf.vm.ThreadInfo ti, DynamicRegion dynRegion)

Method Summary

Modifier and Type	Method and Description
Stmt	bad(java.lang.Object obj)
private Stmt	createGammaStmt(za.ac.sun.cs.green.expr.Expression condition, FieldRef fieldRef, SubscriptPair thenSubscript, SubscriptPair elseSubscript)
private SubscriptPair	createSubscript(FieldRef fieldRef)
DynamicRegion	execute()
static Stmt	getThrowInstruction()
private Stmt	mergePSM(za.ac.sun.cs.green.expr.Expression condition, FieldSubscriptMap thenMap, FieldSubscriptMap elseMap)
static int	nextFieldExceptionNumber()
private void	populateException(java.lang.IllegalArgumentException e)
private SubstituteGetOutput	substituteGet(GetInstruction getIns, FieldRef fieldRef)
Stmt	visit(GetInstruction c)
Stmt	visit(IfThenElseStmt stmt)
Stmt	visit(PutInstruction putIns)
Stmt	visit(ReturnInstruction ret)

Methods inherited from class gov.nasa.jpf.symbc.veritesting.ast.visitors.FixedPointAstMapVisitor

getChange, getFirstException

Methods inherited from class gov.nasa.jpf.symbc.veritesting.ast.visitors.AstMapVisitor

visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit

Methods inherited from class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprMapVisitor

visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit

Methods inherited from class java.lang.Object

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

Field Detail

fieldExceptionNumber

private static int fieldExceptionNumber

dynRegion

private DynamicRegion dynRegion

psm

public FieldSubscriptMap psm

ti

private gov.nasa.jpf.vm.ThreadInfo ti

FIELD_SUBSCRIPT_BASE

static final int FIELD_SUBSCRIPT_BASE

See Also:

Constant Field Values

gsm

private GlobalSubscriptMap gsm

Constructor Detail

FieldSSAVisitor

public FieldSSAVisitor(gov.nasa.jpf.vm.ThreadInfo ti,
                       DynamicRegion dynRegion)

Method Detail

populateException

private void populateException(java.lang.IllegalArgumentException e)

bad

public Stmt bad(java.lang.Object obj)

visit

public Stmt visit(ReturnInstruction ret)

Specified by:

visit in interface AstVisitor<Stmt>

Overrides:

visit in class AstMapVisitor

visit

public Stmt visit(PutInstruction putIns)

Specified by:

visit in interface AstVisitor<Stmt>

Overrides:

visit in class AstMapVisitor

getThrowInstruction

public static Stmt getThrowInstruction()

nextFieldExceptionNumber

public static int nextFieldExceptionNumber()

createSubscript

private SubscriptPair createSubscript(FieldRef fieldRef)

visit

public Stmt visit(IfThenElseStmt stmt)

Specified by:

visit in interface AstVisitor<Stmt>

Overrides:

visit in class AstMapVisitor

mergePSM

private Stmt mergePSM(za.ac.sun.cs.green.expr.Expression condition,
                      FieldSubscriptMap thenMap,
                      FieldSubscriptMap elseMap)

createGammaStmt

private Stmt createGammaStmt(za.ac.sun.cs.green.expr.Expression condition,
                             FieldRef fieldRef,
                             SubscriptPair thenSubscript,
                             SubscriptPair elseSubscript)

visit

public Stmt visit(GetInstruction c)

Specified by:

visit in interface AstVisitor<Stmt>

Overrides:

visit in class AstMapVisitor

substituteGet

private SubstituteGetOutput substituteGet(GetInstruction getIns,
                                          FieldRef fieldRef)
                                   throws StaticRegionException

Throws:

StaticRegionException

execute

public DynamicRegion execute()

Specified by:

execute in class FixedPointAstMapVisitor