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

Class ArrayExpressions

java.lang.Object

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

public class ArrayExpressions
extends java.lang.Object

Field Summary

Fields

Modifier and Type	Field and Description
java.util.HashMap<java.lang.Integer,java.lang.String>	arrayTypesTable
java.util.HashMap<java.lang.Integer,za.ac.sun.cs.green.expr.Expression[]>	table
private gov.nasa.jpf.vm.ThreadInfo	ti
int	uniqueNum

Constructor Summary

Constructors

Constructor and Description
ArrayExpressions(gov.nasa.jpf.vm.ThreadInfo ti)
ArrayExpressions(gov.nasa.jpf.vm.ThreadInfo ti, java.util.HashMap newTable, java.util.HashMap newTypesTable)

Method Summary

Modifier and Type	Method and Description
void	add(java.lang.Integer v1, Pair<za.ac.sun.cs.green.expr.Expression[],java.lang.String> v2)
ArrayExpressions	clone()
za.ac.sun.cs.green.expr.Expression	get(ArrayRef arrayRef)
java.lang.String	getType(int ref)
za.ac.sun.cs.green.expr.Expression[]	lookup(java.lang.Integer ref)
ArrayExpressions	makeUnique(int uniqueNum)
void	remove(java.lang.Integer ref)
java.lang.String	toString()
void	update(ArrayRef arrayRef, za.ac.sun.cs.green.expr.Expression value)

Methods inherited from class java.lang.Object

equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

table

public final java.util.HashMap<java.lang.Integer,za.ac.sun.cs.green.expr.Expression[]> table

arrayTypesTable

public final java.util.HashMap<java.lang.Integer,java.lang.String> arrayTypesTable

ti

private gov.nasa.jpf.vm.ThreadInfo ti

uniqueNum

public int uniqueNum

Constructor Detail

ArrayExpressions

public ArrayExpressions(gov.nasa.jpf.vm.ThreadInfo ti)

ArrayExpressions

public ArrayExpressions(gov.nasa.jpf.vm.ThreadInfo ti,
                        java.util.HashMap newTable,
                        java.util.HashMap newTypesTable)

Method Detail

clone

public ArrayExpressions clone()

Overrides:

clone in class java.lang.Object

add

public void add(java.lang.Integer v1,
                Pair<za.ac.sun.cs.green.expr.Expression[],java.lang.String> v2)

update

public void update(ArrayRef arrayRef,
                   za.ac.sun.cs.green.expr.Expression value)

lookup

public za.ac.sun.cs.green.expr.Expression[] lookup(java.lang.Integer ref)

remove

public void remove(java.lang.Integer ref)

getType

public java.lang.String getType(int ref)

get

public za.ac.sun.cs.green.expr.Expression get(ArrayRef arrayRef)
                                       throws StaticRegionException

Throws:

StaticRegionException

makeUnique

public ArrayExpressions makeUnique(int uniqueNum)
                            throws StaticRegionException

Throws:

StaticRegionException

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object