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

Class RegionBoundaryVisitor

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.transformations.Environment.RegionBoundaryVisitor

All Implemented Interfaces:

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

public class RegionBoundaryVisitor
extends AstMapVisitor

The visitor explores the boundaries of the region by identifying: first def, last def and first use vars. This information is later used to identify beginning and ending of vars for which the tables should be populated.

Field Summary

Fields

Modifier and Type	Field and Description
private java.util.ArrayList<java.lang.Integer>	allDefs

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

eva, exprVisitor

Constructor Summary

Constructors

Constructor and Description
RegionBoundaryVisitor(ExprBoundaryVisitor exprBoundaryVisitor)

Method Summary

Modifier and Type	Method and Description
RegionBoundaryOutput	getOutput()
Stmt	visit(ArrayLengthInstruction c)
Stmt	visit(ArrayLoadInstruction c)
Stmt	visit(ArrayStoreInstruction c)
Stmt	visit(AssignmentStmt a)
Stmt	visit(CheckCastInstruction c)
Stmt	visit(CompositionStmt a)
Stmt	visit(GetInstruction c)
Stmt	visit(IfThenElseStmt a)
Stmt	visit(InstanceOfInstruction c)
Stmt	visit(InvokeInstruction c)
Stmt	visit(NewInstruction c)
Stmt	visit(PhiInstruction c)
Stmt	visit(PutInstruction c)
Stmt	visit(ReturnInstruction c)
Stmt	visit(SkipStmt a)
Stmt	visit(SPFCaseStmt c)
Stmt	visit(SwitchInstruction c)
Stmt	visit(ThrowInstruction c)

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

allDefs

private java.util.ArrayList<java.lang.Integer> allDefs

Constructor Detail

RegionBoundaryVisitor

public RegionBoundaryVisitor(ExprBoundaryVisitor exprBoundaryVisitor)

Method Detail

visit

public Stmt visit(AssignmentStmt a)

Specified by:

visit in interface AstVisitor<Stmt>

Overrides:

visit in class AstMapVisitor

visit

public Stmt visit(CompositionStmt a)

Specified by:

visit in interface AstVisitor<Stmt>

Overrides:

visit in class AstMapVisitor

visit

public Stmt visit(IfThenElseStmt a)

Specified by:

visit in interface AstVisitor<Stmt>

Overrides:

visit in class AstMapVisitor

visit

public Stmt visit(SkipStmt a)

Specified by:

visit in interface AstVisitor<Stmt>

Overrides:

visit in class AstMapVisitor

visit

public Stmt visit(SPFCaseStmt c)

Specified by:

visit in interface AstVisitor<Stmt>

Overrides:

visit in class AstMapVisitor

visit

public Stmt visit(ArrayLoadInstruction c)

Specified by:

visit in interface AstVisitor<Stmt>

Overrides:

visit in class AstMapVisitor

visit

public Stmt visit(ArrayStoreInstruction c)

Specified by:

visit in interface AstVisitor<Stmt>

Overrides:

visit in class AstMapVisitor

visit

public Stmt visit(SwitchInstruction c)

Specified by:

visit in interface AstVisitor<Stmt>

Overrides:

visit in class AstMapVisitor

visit

public Stmt visit(ReturnInstruction c)

Specified by:

visit in interface AstVisitor<Stmt>

Overrides:

visit in class AstMapVisitor

visit

public Stmt visit(GetInstruction c)

Specified by:

visit in interface AstVisitor<Stmt>

Overrides:

visit in class AstMapVisitor

visit

public Stmt visit(PutInstruction c)

Specified by:

visit in interface AstVisitor<Stmt>

Overrides:

visit in class AstMapVisitor

visit

public Stmt visit(NewInstruction c)

Specified by:

visit in interface AstVisitor<Stmt>

Overrides:

visit in class AstMapVisitor

visit

public Stmt visit(InvokeInstruction c)

Specified by:

visit in interface AstVisitor<Stmt>

Overrides:

visit in class AstMapVisitor

visit

public Stmt visit(ArrayLengthInstruction c)

Specified by:

visit in interface AstVisitor<Stmt>

Overrides:

visit in class AstMapVisitor

visit

public Stmt visit(ThrowInstruction c)

Specified by:

visit in interface AstVisitor<Stmt>

Overrides:

visit in class AstMapVisitor

visit

public Stmt visit(CheckCastInstruction c)

Specified by:

visit in interface AstVisitor<Stmt>

Overrides:

visit in class AstMapVisitor

visit

public Stmt visit(InstanceOfInstruction c)

Specified by:

visit in interface AstVisitor<Stmt>

Overrides:

visit in class AstMapVisitor

visit

public Stmt visit(PhiInstruction c)

Specified by:

visit in interface AstVisitor<Stmt>

Overrides:

visit in class AstMapVisitor

getOutput

public RegionBoundaryOutput getOutput()