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

Class ArrayUtil

java.lang.Object

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

public class ArrayUtil
extends java.lang.Object

Constructor Summary

Constructors

Constructor and Description
ArrayUtil()

Method Summary

Modifier and Type	Method and Description
static Pair<za.ac.sun.cs.green.expr.Expression,java.lang.String>	constructArrayITE(za.ac.sun.cs.green.expr.Expression indexExpression, int index, Pair<za.ac.sun.cs.green.expr.Expression[],java.lang.String> valuesTypePair)
static void	doArrayStore(gov.nasa.jpf.vm.ThreadInfo ti, ArrayExpressions arrayExpressions, DynamicTable<za.ac.sun.cs.green.expr.Expression> constantsTable)
static Pair<za.ac.sun.cs.green.expr.Expression,java.lang.String>	getArrayElement(gov.nasa.jpf.vm.ElementInfo ei, int index)
private static za.ac.sun.cs.green.expr.Expression	getArrayElementInner(gov.nasa.jpf.vm.ElementInfo ei, int index, java.lang.String type)
static int	getArrayLength(gov.nasa.jpf.vm.ThreadInfo ti, int ref)
static Pair<za.ac.sun.cs.green.expr.Expression,java.lang.String>	getExpression(gov.nasa.jpf.vm.ThreadInfo ti, ArrayRef c, Pair<za.ac.sun.cs.green.expr.Expression[],java.lang.String> valuesTypePair)
static Pair<za.ac.sun.cs.green.expr.Expression[],java.lang.String>	getInitialArrayValues(gov.nasa.jpf.vm.ThreadInfo ti, int ref)

Methods inherited from class java.lang.Object

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

Constructor Detail

ArrayUtil

public ArrayUtil()

Method Detail

getExpression

public static Pair<za.ac.sun.cs.green.expr.Expression,java.lang.String> getExpression(gov.nasa.jpf.vm.ThreadInfo ti,
                                                                                      ArrayRef c,
                                                                                      Pair<za.ac.sun.cs.green.expr.Expression[],java.lang.String> valuesTypePair)

constructArrayITE

public static Pair<za.ac.sun.cs.green.expr.Expression,java.lang.String> constructArrayITE(za.ac.sun.cs.green.expr.Expression indexExpression,
                                                                                          int index,
                                                                                          Pair<za.ac.sun.cs.green.expr.Expression[],java.lang.String> valuesTypePair)

getArrayElement

public static Pair<za.ac.sun.cs.green.expr.Expression,java.lang.String> getArrayElement(gov.nasa.jpf.vm.ElementInfo ei,
                                                                                        int index)

getArrayElementInner

private static za.ac.sun.cs.green.expr.Expression getArrayElementInner(gov.nasa.jpf.vm.ElementInfo ei,
                                                                       int index,
                                                                       java.lang.String type)

getArrayLength

public static int getArrayLength(gov.nasa.jpf.vm.ThreadInfo ti,
                                 int ref)

getInitialArrayValues

public static Pair<za.ac.sun.cs.green.expr.Expression[],java.lang.String> getInitialArrayValues(gov.nasa.jpf.vm.ThreadInfo ti,
                                                                                                int ref)

doArrayStore

public static void doArrayStore(gov.nasa.jpf.vm.ThreadInfo ti,
                                ArrayExpressions arrayExpressions,
                                DynamicTable<za.ac.sun.cs.green.expr.Expression> constantsTable)
                         throws StaticRegionException

Throws:

StaticRegionException