gov.nasa.jpf.symbc.veritesting.ast.def

Class AstVarExpr

java.lang.Object

za.ac.sun.cs.green.expr.Expression

za.ac.sun.cs.green.expr.Variable

gov.nasa.jpf.symbc.veritesting.ast.def.CloneableVariable

gov.nasa.jpf.symbc.veritesting.ast.def.AstVarExpr

All Implemented Interfaces:

java.io.Serializable, java.lang.Cloneable, java.lang.Comparable<za.ac.sun.cs.green.expr.Expression>

public class AstVarExpr
extends CloneableVariable

AstVarExpr MWW: this is the variable expression for generated local variables. It is currently used in the removeEarlyReturn transformation. For now, we do not distinguish between a variable definition and use. This is in the spirit of SPF, which also does ot make that distinction. However, care must be taken so that we do not declare two variables of the same name with different types.

See Also:

Serialized Form

Field Summary

Fields

Modifier and Type	Field and Description
java.lang.String	type
private int	uniqueNum

Constructor Summary

Constructors

Constructor and Description
AstVarExpr(java.lang.String name, java.lang.String type)
AstVarExpr(java.lang.String name, java.lang.String type, int unique)

Method Summary

Modifier and Type	Method and Description
void	accept(za.ac.sun.cs.green.expr.Visitor visitor)
AstVarExpr	clone()
boolean	equals(java.lang.Object o)
int	getLeftLength()
int	getLength()
java.util.List<java.lang.String>	getOperationVector()
java.lang.String	getSymName()
int	getUniqueNum()
int	hashCode()
AstVarExpr	makeUnique(int unique)
int	numVar()
int	numVarLeft()
java.lang.String	toString()

Methods inherited from class za.ac.sun.cs.green.expr.Variable

getName, getOriginal

Methods inherited from class za.ac.sun.cs.green.expr.Expression

compareTo

Methods inherited from class java.lang.Object

finalize, getClass, notify, notifyAll, wait, wait, wait

Field Detail

type

public final java.lang.String type

uniqueNum

private int uniqueNum

Constructor Detail

AstVarExpr

public AstVarExpr(java.lang.String name,
                  java.lang.String type)

AstVarExpr

public AstVarExpr(java.lang.String name,
                  java.lang.String type,
                  int unique)

Method Detail

accept

public void accept(za.ac.sun.cs.green.expr.Visitor visitor)
            throws za.ac.sun.cs.green.expr.VisitorException

Specified by:

accept in class za.ac.sun.cs.green.expr.Expression

Throws:

za.ac.sun.cs.green.expr.VisitorException

equals

public boolean equals(java.lang.Object o)

Specified by:

equals in class CloneableVariable

toString

public java.lang.String toString()

Specified by:

toString in class za.ac.sun.cs.green.expr.Expression

getLength

public int getLength()

Specified by:

getLength in class za.ac.sun.cs.green.expr.Expression

getLeftLength

public int getLeftLength()

Specified by:

getLeftLength in class za.ac.sun.cs.green.expr.Expression

numVar

public int numVar()

Specified by:

numVar in class za.ac.sun.cs.green.expr.Expression

numVarLeft

public int numVarLeft()

Specified by:

numVarLeft in class za.ac.sun.cs.green.expr.Expression

getOperationVector

public java.util.List<java.lang.String> getOperationVector()

Specified by:

getOperationVector in class za.ac.sun.cs.green.expr.Expression

clone

public AstVarExpr clone()

Specified by:

clone in class CloneableVariable

makeUnique

public AstVarExpr makeUnique(int unique)
                      throws StaticRegionException

Specified by:

makeUnique in class CloneableVariable

Throws:

StaticRegionException

getSymName

public java.lang.String getSymName()

hashCode

public int hashCode()

Specified by:

hashCode in class CloneableVariable

getUniqueNum

public int getUniqueNum()