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

Class ArrayRef

java.lang.Object

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

public class ArrayRef
extends java.lang.Object

Field Summary

Fields

Modifier and Type	Field and Description
za.ac.sun.cs.green.expr.Expression	index
int	ref

Constructor Summary

Constructors

Constructor and Description
ArrayRef(int ref, za.ac.sun.cs.green.expr.Expression index)

Method Summary

Modifier and Type	Method and Description
protected ArrayRef	clone()
boolean	equals(java.lang.Object obj)
za.ac.sun.cs.green.expr.Expression	getIndex()
int	getRef()
static boolean	looseArrayRefEquals(ArrayRef arrayRef, ArrayRef key)
static ArrayRef	makeArrayRef(ArrayLoadInstruction getIns)
static ArrayRef	makeArrayRef(ArrayStoreInstruction getIns)
java.lang.String	toString()

Methods inherited from class java.lang.Object

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

Field Detail

ref

public final int ref

index

public final za.ac.sun.cs.green.expr.Expression index

Constructor Detail

ArrayRef

public ArrayRef(int ref,
                za.ac.sun.cs.green.expr.Expression index)

Method Detail

makeArrayRef

public static ArrayRef makeArrayRef(ArrayLoadInstruction getIns)

makeArrayRef

public static ArrayRef makeArrayRef(ArrayStoreInstruction getIns)

getIndex

public za.ac.sun.cs.green.expr.Expression getIndex()

getRef

public int getRef()

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

equals

public boolean equals(java.lang.Object obj)

Overrides:

equals in class java.lang.Object

clone

protected ArrayRef clone()

Overrides:

clone in class java.lang.Object

looseArrayRefEquals

public static boolean looseArrayRefEquals(ArrayRef arrayRef,
                                          ArrayRef key)