gov.nasa.jpf.symbc.veritesting

Class FixedPointWrapper

java.lang.Object

gov.nasa.jpf.symbc.veritesting.FixedPointWrapper

public class FixedPointWrapper
extends java.lang.Object

This class is called multiple times over different transformations. What it does is that it keeps a common state among all transformations, that is was called on.

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
(package private) static class	FixedPointWrapper.Transformation

Field Summary

Fields

Modifier and Type	Field and Description
private static boolean	changed Tells if there has been a change
private static FixedPointWrapper.Transformation	changedTransformation Tells which transformation is responsible for the change, thi carries the first transformation that has happened.
private static java.lang.Exception	firstException Keeps the first exception that has been encountered in all the transformations.
static long	fixedPointTime
static int	iterationNumber
static DynamicTable	multiPathRegSymbolValueTable
private static DynamicRegion	regionAfter
private static DynamicRegion	regionBefore
private static gov.nasa.jpf.vm.ThreadInfo	ti
private static gov.nasa.jpf.vm.StackFrame	topStackFrame

Constructor Summary

Constructors

Constructor and Description
FixedPointWrapper()

Method Summary

Modifier and Type	Method and Description
private static void	collectTransformationState(FixedPointAstMapVisitor currentTransformation) sets if change has happened and also sets up the transformation responsible for the change;
static DynamicRegion	executeFixedPointHighOrder(gov.nasa.jpf.vm.ThreadInfo ti, DynamicRegion dynRegion)
static DynamicRegion	executeFixedPointTransformations(gov.nasa.jpf.vm.ThreadInfo ti, DynamicRegion dynRegion)
static FixedPointWrapper.Transformation	getChangedTransformation()
static java.lang.Exception	getFirstException()
static int	getIterationNumber()
static DynamicRegion	getRegionAfter()
static boolean	isChangedFlag() Returns if change has happened
static boolean	isEqualRegion()
static void	resetChange()
static void	resetIteration()
static void	resetWrapper()

Methods inherited from class java.lang.Object

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

Field Detail

fixedPointTime

public static long fixedPointTime

multiPathRegSymbolValueTable

public static DynamicTable multiPathRegSymbolValueTable

changed

private static boolean changed

Tells if there has been a change

changedTransformation

private static FixedPointWrapper.Transformation changedTransformation

Tells which transformation is responsible for the change, thi carries the first transformation that has happened.

firstException

private static java.lang.Exception firstException

Keeps the first exception that has been encountered in all the transformations.

ti

private static gov.nasa.jpf.vm.ThreadInfo ti

topStackFrame

private static gov.nasa.jpf.vm.StackFrame topStackFrame

regionBefore

private static DynamicRegion regionBefore

regionAfter

private static DynamicRegion regionAfter

iterationNumber

public static int iterationNumber

Constructor Detail

FixedPointWrapper

public FixedPointWrapper()

Method Detail

getRegionAfter

public static DynamicRegion getRegionAfter()

isChangedFlag

public static boolean isChangedFlag()

Returns if change has happened

Returns:

isEqualRegion

public static boolean isEqualRegion()

getFirstException

public static java.lang.Exception getFirstException()

getIterationNumber

public static int getIterationNumber()

getChangedTransformation

public static FixedPointWrapper.Transformation getChangedTransformation()

collectTransformationState

private static void collectTransformationState(FixedPointAstMapVisitor currentTransformation)

sets if change has happened and also sets up the transformation responsible for the change;

resetIteration

public static void resetIteration()

resetChange

public static void resetChange()

resetWrapper

public static void resetWrapper()

executeFixedPointTransformations

public static DynamicRegion executeFixedPointTransformations(gov.nasa.jpf.vm.ThreadInfo ti,
                                                             DynamicRegion dynRegion)
                                                      throws StaticRegionException,
                                                             java.lang.CloneNotSupportedException

Throws:

StaticRegionException

java.lang.CloneNotSupportedException

executeFixedPointHighOrder

public static DynamicRegion executeFixedPointHighOrder(gov.nasa.jpf.vm.ThreadInfo ti,
                                                       DynamicRegion dynRegion)
                                                throws StaticRegionException,
                                                       java.lang.CloneNotSupportedException

Throws:

StaticRegionException

java.lang.CloneNotSupportedException