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

Class LocalOutputInvariantVisitor

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.Invariants.LocalOutputInvariantVisitor

All Implemented Interfaces:

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

public class LocalOutputInvariantVisitor
extends AstMapVisitor

Field Summary

Fields

Modifier and Type	Field and Description
(package private) ExprVisitorAdapter<za.ac.sun.cs.green.expr.Expression>	eva
java.util.List<AssignmentStmt>	gammaStmts
java.util.List<java.lang.Integer>	gammaWalaVarDefs

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

exprVisitor

Constructor Summary

Constructors

Modifier	Constructor and Description
private	LocalOutputInvariantVisitor(StaticRegion staticRegion)

Method Summary

Modifier and Type	Method and Description
static boolean	execute(StaticRegion staticRegion)
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

eva

ExprVisitorAdapter<za.ac.sun.cs.green.expr.Expression> eva

gammaStmts

public java.util.List<AssignmentStmt> gammaStmts

gammaWalaVarDefs

public java.util.List<java.lang.Integer> gammaWalaVarDefs

Constructor Detail

LocalOutputInvariantVisitor

private LocalOutputInvariantVisitor(StaticRegion staticRegion)

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

execute

public static boolean execute(StaticRegion staticRegion)
                       throws StaticRegionException

Throws:

StaticRegionException