gov.nasa.jpf.symbc.veritesting.ChoiceGenerator

Class StaticBranchChoiceGenerator

java.lang.Object

gov.nasa.jpf.vm.ChoiceGeneratorBase<java.lang.Integer>

gov.nasa.jpf.vm.choice.IntIntervalGenerator

gov.nasa.jpf.symbc.numeric.PCChoiceGenerator

gov.nasa.jpf.symbc.veritesting.ChoiceGenerator.StaticPCChoiceGenerator

gov.nasa.jpf.symbc.veritesting.ChoiceGenerator.StaticBranchChoiceGenerator

All Implemented Interfaces:

gov.nasa.jpf.vm.ChoiceGenerator<java.lang.Integer>, gov.nasa.jpf.vm.IntChoiceGenerator, java.lang.Cloneable

public class StaticBranchChoiceGenerator
extends StaticPCChoiceGenerator

Nested Class Summary

Nested classes/interfaces inherited from class gov.nasa.jpf.symbc.veritesting.ChoiceGenerator.StaticPCChoiceGenerator

StaticPCChoiceGenerator.Kind

Field Summary

Fields

Modifier and Type	Field and Description
static int	ELSE_CHOICE
static int	HEURISTICS_ELSE_CHOICE
static int	HEURISTICS_THEN_CHOICE
static boolean	heuristicsCountingMode
static int	RETURN_CHOICE
static int	STATIC_CHOICE
static int	THEN_CHOICE

Fields inherited from class gov.nasa.jpf.symbc.veritesting.ChoiceGenerator.StaticPCChoiceGenerator

currentTopFrame, region

Fields inherited from class gov.nasa.jpf.symbc.numeric.PCChoiceGenerator

PC

Fields inherited from class gov.nasa.jpf.vm.choice.IntIntervalGenerator

delta, max, min, next

Fields inherited from class gov.nasa.jpf.vm.ChoiceGeneratorBase

attr, id, idRef, insn, isCascaded, isDone, MARKER, prev, random, stateId, ti

Constructor Summary

Constructors

Constructor and Description
StaticBranchChoiceGenerator(DynamicRegion region, gov.nasa.jpf.vm.Instruction instruction)
StaticBranchChoiceGenerator(DynamicRegion region, gov.nasa.jpf.vm.Instruction instruction, boolean heuristicsOn)

Method Summary

Modifier and Type	Method and Description
static gov.nasa.jpf.symbc.numeric.PathCondition	createPC(gov.nasa.jpf.symbc.numeric.PathCondition pc, za.ac.sun.cs.green.expr.Expression regionSummary, za.ac.sun.cs.green.expr.Expression constraint)
gov.nasa.jpf.vm.Instruction	execute(gov.nasa.jpf.vm.ThreadInfo ti, gov.nasa.jpf.vm.Instruction instructionToExecute, int choice)
private gov.nasa.jpf.vm.Instruction	executeBinaryIf(gov.nasa.jpf.vm.Instruction instruction, int choice)
gov.nasa.jpf.vm.Instruction	executeNullIf(gov.nasa.jpf.vm.Instruction instruction)
gov.nasa.jpf.vm.Instruction	executeUnaryIf(gov.nasa.jpf.vm.Instruction instruction, int choice)
static int	getNumSatChoices(DynamicRegion region)
static boolean	isOnlyStaticChoiceSat(DynamicRegion region)
void	makeVeritestingCG(gov.nasa.jpf.vm.ThreadInfo ti, gov.nasa.jpf.vm.Instruction instructionToExecute, java.lang.String key)

Methods inherited from class gov.nasa.jpf.symbc.veritesting.ChoiceGenerator.StaticPCChoiceGenerator

getKind, getRegion

Methods inherited from class gov.nasa.jpf.symbc.numeric.PCChoiceGenerator

getCurrentPC, getMethodName, getOffset, isReverseOrder, randomize, setCurrentPC, setMethodName, setNextChoice, setOffset, setPC

Methods inherited from class gov.nasa.jpf.vm.choice.IntIntervalGenerator

advance, getChoice, getChoices, getChoiceType, getNextChoice, getProcessedNumberOfChoices, getTotalNumberOfChoices, hasMoreChoices, isAscending, reorder, reset, reverse, supportsReordering, toString

Methods inherited from class gov.nasa.jpf.vm.ChoiceGeneratorBase

addAttr, advance, attrIterator, attrIterator, clone, deepClone, getAll, getAllChoices, getAllOfType, getAttr, getAttr, getCascade, getCascadedParent, getId, getIdRef, getInsn, getNextAttr, getNumberOfParents, getPreviousChoiceGenerator, getPreviousChoiceGeneratorOfType, getProcessedChoices, getSourceLocation, getStateId, getThreadInfo, getUnprocessedChoices, hasAttr, hasAttr, hasAttrValue, init, isCascaded, isDone, isProcessed, isSchedulingPoint, removeAttr, replaceAttr, select, setAttr, setCascaded, setContext, setCurrent, setDone, setId, setIdRef, setInsn, setPreviousChoiceGenerator, setStateId, setThreadInfo, useRandomization

Methods inherited from class java.lang.Object

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

Methods inherited from interface gov.nasa.jpf.vm.ChoiceGenerator

addAttr, advance, attrIterator, attrIterator, clone, deepClone, getAll, getAllChoices, getAllOfType, getAttr, getAttr, getCascade, getCascadedParent, getId, getIdRef, getInsn, getNextAttr, getNumberOfParents, getPreviousChoiceGenerator, getPreviousChoiceGeneratorOfType, getProcessedChoices, getSourceLocation, getStateId, getThreadInfo, getUnprocessedChoices, hasAttr, hasAttr, isCascaded, isDone, isProcessed, isSchedulingPoint, removeAttr, replaceAttr, select, setAttr, setCascaded, setContext, setCurrent, setDone, setId, setIdRef, setInsn, setPreviousChoiceGenerator, setStateId, setThreadInfo

Field Detail

STATIC_CHOICE

public static int STATIC_CHOICE

THEN_CHOICE

public static int THEN_CHOICE

ELSE_CHOICE

public static int ELSE_CHOICE

RETURN_CHOICE

public static int RETURN_CHOICE

HEURISTICS_THEN_CHOICE

public static int HEURISTICS_THEN_CHOICE

HEURISTICS_ELSE_CHOICE

public static int HEURISTICS_ELSE_CHOICE

heuristicsCountingMode

public static boolean heuristicsCountingMode

Constructor Detail

StaticBranchChoiceGenerator

public StaticBranchChoiceGenerator(DynamicRegion region,
                                   gov.nasa.jpf.vm.Instruction instruction)

StaticBranchChoiceGenerator

public StaticBranchChoiceGenerator(DynamicRegion region,
                                   gov.nasa.jpf.vm.Instruction instruction,
                                   boolean heuristicsOn)

Method Detail

execute

public gov.nasa.jpf.vm.Instruction execute(gov.nasa.jpf.vm.ThreadInfo ti,
                                           gov.nasa.jpf.vm.Instruction instructionToExecute,
                                           int choice)
                                    throws StaticRegionException

Specified by:

execute in class StaticPCChoiceGenerator

Throws:

StaticRegionException

executeBinaryIf

private gov.nasa.jpf.vm.Instruction executeBinaryIf(gov.nasa.jpf.vm.Instruction instruction,
                                                    int choice)
                                             throws StaticRegionException

Throws:

StaticRegionException

executeNullIf

public gov.nasa.jpf.vm.Instruction executeNullIf(gov.nasa.jpf.vm.Instruction instruction)

executeUnaryIf

public gov.nasa.jpf.vm.Instruction executeUnaryIf(gov.nasa.jpf.vm.Instruction instruction,
                                                  int choice)
                                           throws StaticRegionException

Throws:

StaticRegionException

createPC

public static gov.nasa.jpf.symbc.numeric.PathCondition createPC(gov.nasa.jpf.symbc.numeric.PathCondition pc,
                                                                za.ac.sun.cs.green.expr.Expression regionSummary,
                                                                za.ac.sun.cs.green.expr.Expression constraint)

makeVeritestingCG

public void makeVeritestingCG(gov.nasa.jpf.vm.ThreadInfo ti,
                              gov.nasa.jpf.vm.Instruction instructionToExecute,
                              java.lang.String key)
                       throws StaticRegionException

Specified by:

makeVeritestingCG in class StaticPCChoiceGenerator

Throws:

StaticRegionException

getNumSatChoices

public static int getNumSatChoices(DynamicRegion region)

isOnlyStaticChoiceSat

public static boolean isOnlyStaticChoiceSat(DynamicRegion region)