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

Class FixedPointAstMapVisitor

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

All Implemented Interfaces:

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

Direct Known Subclasses:

ArraySSAVisitor, FieldSSAVisitor, SimplifyStmtVisitor, SubstitutionVisitor

public abstract class FixedPointAstMapVisitor
extends AstMapVisitor

Field Summary

Fields

Modifier and Type	Field and Description
protected java.lang.Exception	firstException this is used when computing fixed point to carry the first exception that the visitor might have encountered.
protected DynamicRegion	instantiatedRegion
protected boolean	somethingChanged This is used to capture the fact that there is change happening in the transformation, this is used for the quick check for the fix point computation.

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

eva, exprVisitor

Constructor Summary

Constructors

Constructor and Description
FixedPointAstMapVisitor(ExprVisitor<za.ac.sun.cs.green.expr.Expression> exprVisitor)

Method Summary

Modifier and Type	Method and Description
abstract DynamicRegion	execute()
boolean	getChange()
java.lang.Exception	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, 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

somethingChanged

protected boolean somethingChanged

This is used to capture the fact that there is change happening in the transformation, this is used for the quick check for the fix point computation.

firstException

protected java.lang.Exception firstException

this is used when computing fixed point to carry the first exception that the visitor might have encountered.

instantiatedRegion

protected DynamicRegion instantiatedRegion

Constructor Detail

FixedPointAstMapVisitor

public FixedPointAstMapVisitor(ExprVisitor<za.ac.sun.cs.green.expr.Expression> exprVisitor)

Method Detail

getChange

public boolean getChange()

getFirstException

public java.lang.Exception getFirstException()

execute

public abstract DynamicRegion execute()