gov.nasa.jpf.symbc.veritesting.ChoiceGenerator

Class StaticPCChoiceGenerator

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

All Implemented Interfaces:

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

Direct Known Subclasses:

StaticBranchChoiceGenerator

public abstract class StaticPCChoiceGenerator
extends gov.nasa.jpf.symbc.numeric.PCChoiceGenerator

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static class	StaticPCChoiceGenerator.Kind

Field Summary

Fields

Modifier and Type	Field and Description
protected gov.nasa.jpf.vm.StackFrame	currentTopFrame
protected DynamicRegion	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
StaticPCChoiceGenerator(int count, DynamicRegion region, gov.nasa.jpf.vm.Instruction instruction)

Method Summary

Modifier and Type	Method and Description
abstract gov.nasa.jpf.vm.Instruction	execute(gov.nasa.jpf.vm.ThreadInfo ti, gov.nasa.jpf.vm.Instruction instructionToExecute, int choice)
static StaticPCChoiceGenerator.Kind	getKind(gov.nasa.jpf.vm.Instruction instruction)
protected DynamicRegion	getRegion()
abstract void	makeVeritestingCG(gov.nasa.jpf.vm.ThreadInfo ti, gov.nasa.jpf.vm.Instruction instruction, java.lang.String key)

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

region

protected DynamicRegion region

currentTopFrame

protected gov.nasa.jpf.vm.StackFrame currentTopFrame

Constructor Detail

StaticPCChoiceGenerator

public StaticPCChoiceGenerator(int count,
                               DynamicRegion region,
                               gov.nasa.jpf.vm.Instruction instruction)

Method Detail

getRegion

protected DynamicRegion getRegion()

execute

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

Throws:

StaticRegionException

getKind

public static StaticPCChoiceGenerator.Kind getKind(gov.nasa.jpf.vm.Instruction instruction)

makeVeritestingCG

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

Throws:

StaticRegionException