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

Class ArraySSAVisitor

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.arrayaccess.ArraySSAVisitor

All Implemented Interfaces:

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

public class ArraySSAVisitor
extends FixedPointAstMapVisitor

Field Summary

Fields

Modifier and Type	Field and Description
(package private) static int	ARRAY_SUBSCRIPT_BASE
private static int	arrayExceptionNumber
ArrayExpressions	arrayExpressions
private DynamicRegion	dynRegion
private GlobalArraySubscriptMap	gsm
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
ArraySSAVisitor(gov.nasa.jpf.vm.ThreadInfo ti, DynamicRegion dynRegion)

Method Summary

Modifier and Type	Method and Description
private Stmt	createGammaStmtArray(int ref, za.ac.sun.cs.green.expr.Expression condition, za.ac.sun.cs.green.expr.Expression[] thenExpArr, za.ac.sun.cs.green.expr.Expression[] elseExpArr, java.lang.String type)
DynamicRegion	execute()
private Stmt	getIfThenElseStmt(ArrayRef arrayRef, Stmt assignStmt)
static Stmt	getThrowInstruction()
private boolean	isUnsupportedArrayRef(ArrayRef arrayRef)
private Stmt	mergeArrayExpressions(za.ac.sun.cs.green.expr.Expression condition, ArrayExpressions thenExps, ArrayExpressions elseExps)
static int	nextArrayExceptionNumber()
Stmt	visit(ArrayLengthInstruction c)
Stmt	visit(ArrayLoadInstruction c)
Stmt	visit(ArrayStoreInstruction putIns)
Stmt	visit(IfThenElseStmt stmt)

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

arrayExceptionNumber

private static int arrayExceptionNumber

dynRegion

private DynamicRegion dynRegion

ti

private gov.nasa.jpf.vm.ThreadInfo ti

ARRAY_SUBSCRIPT_BASE

static final int ARRAY_SUBSCRIPT_BASE

See Also:

Constant Field Values

gsm

private GlobalArraySubscriptMap gsm

arrayExpressions

public ArrayExpressions arrayExpressions

Constructor Detail

ArraySSAVisitor

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

Method Detail

visit

public Stmt visit(ArrayLengthInstruction 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

getIfThenElseStmt

private Stmt getIfThenElseStmt(ArrayRef arrayRef,
                               Stmt assignStmt)

getThrowInstruction

public static Stmt getThrowInstruction()

nextArrayExceptionNumber

public static int nextArrayExceptionNumber()

visit

public Stmt visit(ArrayStoreInstruction putIns)

Specified by:

visit in interface AstVisitor<Stmt>

Overrides:

visit in class AstMapVisitor

isUnsupportedArrayRef

private boolean isUnsupportedArrayRef(ArrayRef arrayRef)

visit

public Stmt visit(IfThenElseStmt stmt)

Specified by:

visit in interface AstVisitor<Stmt>

Overrides:

visit in class AstMapVisitor

mergeArrayExpressions

private Stmt mergeArrayExpressions(za.ac.sun.cs.green.expr.Expression condition,
                                   ArrayExpressions thenExps,
                                   ArrayExpressions elseExps)

createGammaStmtArray

private Stmt createGammaStmtArray(int ref,
                                  za.ac.sun.cs.green.expr.Expression condition,
                                  za.ac.sun.cs.green.expr.Expression[] thenExpArr,
                                  za.ac.sun.cs.green.expr.Expression[] elseExpArr,
                                  java.lang.String type)

execute

public DynamicRegion execute()

Specified by:

execute in class FixedPointAstMapVisitor