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

Class ExprSubstitutionVisitor

java.lang.Object

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

gov.nasa.jpf.symbc.veritesting.ast.transformations.substitution.ExprSubstitutionVisitor

All Implemented Interfaces:

ExprVisitor<za.ac.sun.cs.green.expr.Expression>

public class ExprSubstitutionVisitor
extends ExprMapVisitor
implements ExprVisitor<za.ac.sun.cs.green.expr.Expression>

This is the expression visitor class used during substitution that either returns the value of a variable from a symbol table to returns the expression back if it doesn't make to any entry.

Field Summary

Fields

Modifier and Type	Field and Description
private DynamicRegion	dynRegion
ExprVisitorAdapter	eva
private gov.nasa.jpf.vm.StackFrame	sf
private boolean	somethingChanged
static StaticRegionException	sre
private gov.nasa.jpf.vm.ThreadInfo	ti
private DynamicTable	valueSymbolTable

Constructor Summary

Constructors

Constructor and Description
ExprSubstitutionVisitor(gov.nasa.jpf.vm.ThreadInfo ti, DynamicRegion dynRegion, DynamicTable valueSymbolTable)

Method Summary

Modifier and Type	Method and Description
DynamicTable	getValueSymbolTable()
boolean	isSomethingChanged()
void	setValueSymbolTable(DynamicTable valueSymbolTable)
za.ac.sun.cs.green.expr.Expression	visit(FieldRefVarExpr expr)
za.ac.sun.cs.green.expr.Expression	visit(WalaVarExpr expr)

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

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

Methods inherited from interface gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprVisitor

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

Field Detail

ti

private gov.nasa.jpf.vm.ThreadInfo ti

sf

private gov.nasa.jpf.vm.StackFrame sf

eva

public ExprVisitorAdapter eva

dynRegion

private DynamicRegion dynRegion

valueSymbolTable

private DynamicTable valueSymbolTable

somethingChanged

private boolean somethingChanged

sre

public static StaticRegionException sre

Constructor Detail

ExprSubstitutionVisitor

public ExprSubstitutionVisitor(gov.nasa.jpf.vm.ThreadInfo ti,
                               DynamicRegion dynRegion,
                               DynamicTable valueSymbolTable)

Method Detail

isSomethingChanged

public boolean isSomethingChanged()

setValueSymbolTable

public void setValueSymbolTable(DynamicTable valueSymbolTable)

getValueSymbolTable

public DynamicTable getValueSymbolTable()

visit

public za.ac.sun.cs.green.expr.Expression visit(WalaVarExpr expr)

Specified by:

visit in interface ExprVisitor<za.ac.sun.cs.green.expr.Expression>

Overrides:

visit in class ExprMapVisitor

visit

public za.ac.sun.cs.green.expr.Expression visit(FieldRefVarExpr expr)

Specified by:

visit in interface ExprVisitor<za.ac.sun.cs.green.expr.Expression>

Overrides:

visit in class ExprMapVisitor