gov.nasa.jpf.symbc

Class SymbolicInstructionFactory

java.lang.Object

gov.nasa.jpf.jvm.JVMInstructionFactory

gov.nasa.jpf.jvm.bytecode.InstructionFactory

gov.nasa.jpf.symbc.SymbolicInstructionFactory

All Implemented Interfaces:

java.lang.Cloneable

public class SymbolicInstructionFactory
extends gov.nasa.jpf.jvm.bytecode.InstructionFactory

Field Summary

Fields

Modifier and Type	Field and Description
static int	bvlength
(package private) gov.nasa.jpf.vm.ClassInfo	ci
static boolean	collect_constraints
static boolean	concolicMode
static boolean	debugMode
static java.lang.String[]	dp
(package private) gov.nasa.jpf.util.ClassInfoFilter	filter
static boolean	fp
static za.ac.sun.cs.green.Green	greenSolver
static boolean	heuristicPartitionMode
static boolean	heuristicRandomMode
static int	maxPcLength
static long	maxPcMSec
static int	MaxTries
private boolean	pcChoiceOptimization
static boolean	preprocesOnly
static boolean	regressMode
static long	startSystemMillis
static java.lang.String[]	string_dp
static int	stringTimeout
private boolean	symArrays

Fields inherited from class gov.nasa.jpf.jvm.JVMInstructionFactory

singleton

Constructor Summary

Constructors

Constructor and Description
SymbolicInstructionFactory(gov.nasa.jpf.Config conf)

Method Summary

Modifier and Type	Method and Description
gov.nasa.jpf.vm.Instruction	aaload()
gov.nasa.jpf.vm.Instruction	aastore()
gov.nasa.jpf.vm.Instruction	aload_0()
gov.nasa.jpf.vm.Instruction	aload_1()
gov.nasa.jpf.vm.Instruction	aload_2()
gov.nasa.jpf.vm.Instruction	aload_3()
gov.nasa.jpf.vm.Instruction	aload(int localVarIndex)
gov.nasa.jpf.vm.Instruction	anewarray(java.lang.String typeDescriptor)
gov.nasa.jpf.vm.Instruction	arraylength()
gov.nasa.jpf.vm.Instruction	baload()
gov.nasa.jpf.vm.Instruction	bastore()
gov.nasa.jpf.vm.Instruction	caload()
gov.nasa.jpf.vm.Instruction	castore()
gov.nasa.jpf.vm.Instruction	d2f()
gov.nasa.jpf.vm.Instruction	d2i()
gov.nasa.jpf.vm.Instruction	d2l()
gov.nasa.jpf.vm.Instruction	dadd()
gov.nasa.jpf.vm.Instruction	daload()
gov.nasa.jpf.vm.Instruction	dastore()
gov.nasa.jpf.vm.Instruction	dcmpg()
gov.nasa.jpf.vm.Instruction	dcmpl()
gov.nasa.jpf.vm.Instruction	ddiv()
gov.nasa.jpf.vm.Instruction	dmul()
gov.nasa.jpf.vm.Instruction	dneg()
gov.nasa.jpf.vm.Instruction	drem()
gov.nasa.jpf.vm.Instruction	dsub()
gov.nasa.jpf.vm.Instruction	f2d()
gov.nasa.jpf.vm.Instruction	f2i()
gov.nasa.jpf.vm.Instruction	f2l()
gov.nasa.jpf.vm.Instruction	fadd()
gov.nasa.jpf.vm.Instruction	faload()
gov.nasa.jpf.vm.Instruction	fastore()
gov.nasa.jpf.vm.Instruction	fcmpg()
gov.nasa.jpf.vm.Instruction	fcmpl()
gov.nasa.jpf.vm.Instruction	fdiv()
gov.nasa.jpf.vm.Instruction	fmul()
gov.nasa.jpf.vm.Instruction	fneg()
gov.nasa.jpf.vm.Instruction	frem()
gov.nasa.jpf.vm.Instruction	fsub()
gov.nasa.jpf.vm.Instruction	getfield(java.lang.String fieldName, java.lang.String clsName, java.lang.String fieldDescriptor)
gov.nasa.jpf.vm.Instruction	getstatic(java.lang.String fieldName, java.lang.String clsName, java.lang.String fieldDescriptor)
gov.nasa.jpf.vm.Instruction	i2b()
gov.nasa.jpf.vm.Instruction	i2c()
gov.nasa.jpf.vm.Instruction	i2d()
gov.nasa.jpf.vm.Instruction	i2f()
gov.nasa.jpf.vm.Instruction	i2l()
gov.nasa.jpf.vm.Instruction	i2s()
gov.nasa.jpf.vm.Instruction	iadd()
gov.nasa.jpf.vm.Instruction	iaload()
gov.nasa.jpf.vm.Instruction	iand()
gov.nasa.jpf.vm.Instruction	iastore()
gov.nasa.jpf.vm.Instruction	idiv()
gov.nasa.jpf.vm.Instruction	if_icmpeq(int targetPc)
gov.nasa.jpf.vm.Instruction	if_icmpge(int targetPc)
gov.nasa.jpf.vm.Instruction	if_icmpgt(int targetPc)
gov.nasa.jpf.vm.Instruction	if_icmple(int targetPc)
gov.nasa.jpf.vm.Instruction	if_icmplt(int targetPc)
gov.nasa.jpf.vm.Instruction	if_icmpne(int targetPc)
gov.nasa.jpf.vm.Instruction	ifeq(int targetPc)
gov.nasa.jpf.vm.Instruction	ifge(int targetPc)
gov.nasa.jpf.vm.Instruction	ifgt(int targetPc)
gov.nasa.jpf.vm.Instruction	ifle(int targetPc)
gov.nasa.jpf.vm.Instruction	iflt(int targetPc)
gov.nasa.jpf.vm.Instruction	ifne(int targetPc)
gov.nasa.jpf.vm.Instruction	ifnonnull(int targetPc)
gov.nasa.jpf.vm.Instruction	ifnull(int targetPc)
gov.nasa.jpf.vm.Instruction	iinc(int localVarIndex, int incConstant)
gov.nasa.jpf.vm.Instruction	imul()
gov.nasa.jpf.vm.Instruction	ineg()
gov.nasa.jpf.vm.Instruction	invokeinterface(java.lang.String clsName, java.lang.String methodName, java.lang.String methodSignature)
gov.nasa.jpf.vm.Instruction	invokespecial(java.lang.String clsName, java.lang.String methodName, java.lang.String methodSignature)
gov.nasa.jpf.vm.Instruction	invokestatic(java.lang.String clsName, java.lang.String methodName, java.lang.String methodSignature)
gov.nasa.jpf.vm.Instruction	invokevirtual(java.lang.String clsName, java.lang.String methodName, java.lang.String methodSignature)
gov.nasa.jpf.vm.Instruction	ior()
gov.nasa.jpf.vm.Instruction	irem()
gov.nasa.jpf.vm.Instruction	ishl()
gov.nasa.jpf.vm.Instruction	ishr()
gov.nasa.jpf.vm.Instruction	isub()
gov.nasa.jpf.vm.Instruction	iushr()
gov.nasa.jpf.vm.Instruction	ixor()
gov.nasa.jpf.vm.Instruction	l2d()
gov.nasa.jpf.vm.Instruction	l2f()
gov.nasa.jpf.vm.Instruction	l2i()
gov.nasa.jpf.vm.Instruction	ladd()
gov.nasa.jpf.vm.Instruction	laload()
gov.nasa.jpf.vm.Instruction	land()
gov.nasa.jpf.vm.Instruction	lastore()
gov.nasa.jpf.vm.Instruction	lcmp()
gov.nasa.jpf.vm.Instruction	ldiv()
gov.nasa.jpf.vm.Instruction	lmul()
gov.nasa.jpf.vm.Instruction	lneg()
gov.nasa.jpf.vm.Instruction	lookupswitch(int defaultTargetPc, int nEntries)
gov.nasa.jpf.vm.Instruction	lor()
gov.nasa.jpf.vm.Instruction	lrem()
gov.nasa.jpf.vm.Instruction	lshl()
gov.nasa.jpf.vm.Instruction	lshr()
gov.nasa.jpf.vm.Instruction	lsub()
gov.nasa.jpf.vm.Instruction	lushr()
gov.nasa.jpf.vm.Instruction	lxor()
gov.nasa.jpf.vm.Instruction	multianewarray(java.lang.String clsName, int dimensions)
gov.nasa.jpf.vm.Instruction	new_(java.lang.String clsName)
gov.nasa.jpf.vm.Instruction	newarray(int typeCode)
gov.nasa.jpf.vm.Instruction	saload()
gov.nasa.jpf.vm.Instruction	sastore()
private void	setupGreen(gov.nasa.jpf.Config conf)
gov.nasa.jpf.vm.Instruction	tableswitch(int defaultTargetPc, int low, int high)

Methods inherited from class gov.nasa.jpf.jvm.bytecode.InstructionFactory

aconst_null, areturn, astore_0, astore_1, astore_2, astore_3, astore, athrow, bipush, checkcast, clone, dconst_0, dconst_1, directcallreturn, dload_0, dload_1, dload_2, dload_3, dload, dreturn, dstore_0, dstore_1, dstore_2, dstore_3, dstore, dup_x1, dup_x2, dup, dup2_x1, dup2_x2, dup2, executenative, fconst_0, fconst_1, fconst_2, finishclinit, fload_0, fload_1, fload_2, fload_3, fload, freturn, fstore_0, fstore_1, fstore_2, fstore_3, fstore, goto_, goto_w, iconst_0, iconst_1, iconst_2, iconst_3, iconst_4, iconst_5, iconst_m1, if_acmpeq, if_acmpne, iload_0, iload_1, iload_2, iload_3, iload, instanceof_, invokecg, invokeclinit, invokedynamic, ireturn, istore_0, istore_1, istore_2, istore_3, istore, jsr_w, jsr, lconst_0, lconst_1, ldc_w, ldc_w, ldc_w, ldc, ldc, ldc, ldc2_w, ldc2_w, lload_0, lload_1, lload_2, lload_3, lload, lreturn, lstore_0, lstore_1, lstore_2, lstore_3, lstore, monitorenter, monitorexit, nativereturn, nop, pop, pop2, putfield, putstatic, ret, return_, runstart, sipush, swap, wide

Methods inherited from class gov.nasa.jpf.jvm.JVMInstructionFactory

getFactory

Methods inherited from class java.lang.Object

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

Field Detail

dp

public static java.lang.String[] dp

string_dp

public static java.lang.String[] string_dp

stringTimeout

public static int stringTimeout

preprocesOnly

public static boolean preprocesOnly

debugMode

public static boolean debugMode

collect_constraints

public static boolean collect_constraints

regressMode

public static boolean regressMode

greenSolver

public static za.ac.sun.cs.green.Green greenSolver

bvlength

public static int bvlength

fp

public static boolean fp

pcChoiceOptimization

private final boolean pcChoiceOptimization

symArrays

private final boolean symArrays

concolicMode

public static boolean concolicMode

heuristicRandomMode

public static boolean heuristicRandomMode

heuristicPartitionMode

public static boolean heuristicPartitionMode

MaxTries

public static int MaxTries

maxPcLength

public static int maxPcLength

maxPcMSec

public static long maxPcMSec

startSystemMillis

public static long startSystemMillis

ci

gov.nasa.jpf.vm.ClassInfo ci

filter

gov.nasa.jpf.util.ClassInfoFilter filter

Constructor Detail

SymbolicInstructionFactory

public SymbolicInstructionFactory(gov.nasa.jpf.Config conf)

Method Detail

aload

public gov.nasa.jpf.vm.Instruction aload(int localVarIndex)

Overrides:

aload in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

aload_0

public gov.nasa.jpf.vm.Instruction aload_0()

Overrides:

aload_0 in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

aload_1

public gov.nasa.jpf.vm.Instruction aload_1()

Overrides:

aload_1 in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

aload_2

public gov.nasa.jpf.vm.Instruction aload_2()

Overrides:

aload_2 in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

aload_3

public gov.nasa.jpf.vm.Instruction aload_3()

Overrides:

aload_3 in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

iadd

public gov.nasa.jpf.vm.Instruction iadd()

Overrides:

iadd in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

iand

public gov.nasa.jpf.vm.Instruction iand()

Overrides:

iand in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

iinc

public gov.nasa.jpf.vm.Instruction iinc(int localVarIndex,
                                        int incConstant)

Overrides:

iinc in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

isub

public gov.nasa.jpf.vm.Instruction isub()

Overrides:

isub in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

imul

public gov.nasa.jpf.vm.Instruction imul()

Overrides:

imul in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

ineg

public gov.nasa.jpf.vm.Instruction ineg()

Overrides:

ineg in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

ifle

public gov.nasa.jpf.vm.Instruction ifle(int targetPc)

Overrides:

ifle in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

iflt

public gov.nasa.jpf.vm.Instruction iflt(int targetPc)

Overrides:

iflt in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

ifge

public gov.nasa.jpf.vm.Instruction ifge(int targetPc)

Overrides:

ifge in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

ifgt

public gov.nasa.jpf.vm.Instruction ifgt(int targetPc)

Overrides:

ifgt in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

ifeq

public gov.nasa.jpf.vm.Instruction ifeq(int targetPc)

Overrides:

ifeq in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

ifne

public gov.nasa.jpf.vm.Instruction ifne(int targetPc)

Overrides:

ifne in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

invokestatic

public gov.nasa.jpf.vm.Instruction invokestatic(java.lang.String clsName,
                                                java.lang.String methodName,
                                                java.lang.String methodSignature)

Overrides:

invokestatic in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

invokevirtual

public gov.nasa.jpf.vm.Instruction invokevirtual(java.lang.String clsName,
                                                 java.lang.String methodName,
                                                 java.lang.String methodSignature)

Overrides:

invokevirtual in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

invokeinterface

public gov.nasa.jpf.vm.Instruction invokeinterface(java.lang.String clsName,
                                                   java.lang.String methodName,
                                                   java.lang.String methodSignature)

Overrides:

invokeinterface in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

invokespecial

public gov.nasa.jpf.vm.Instruction invokespecial(java.lang.String clsName,
                                                 java.lang.String methodName,
                                                 java.lang.String methodSignature)

Overrides:

invokespecial in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

if_icmpge

public gov.nasa.jpf.vm.Instruction if_icmpge(int targetPc)

Overrides:

if_icmpge in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

if_icmpgt

public gov.nasa.jpf.vm.Instruction if_icmpgt(int targetPc)

Overrides:

if_icmpgt in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

if_icmple

public gov.nasa.jpf.vm.Instruction if_icmple(int targetPc)

Overrides:

if_icmple in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

if_icmplt

public gov.nasa.jpf.vm.Instruction if_icmplt(int targetPc)

Overrides:

if_icmplt in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

idiv

public gov.nasa.jpf.vm.Instruction idiv()

Overrides:

idiv in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

ishl

public gov.nasa.jpf.vm.Instruction ishl()

Overrides:

ishl in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

ishr

public gov.nasa.jpf.vm.Instruction ishr()

Overrides:

ishr in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

iushr

public gov.nasa.jpf.vm.Instruction iushr()

Overrides:

iushr in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

ixor

public gov.nasa.jpf.vm.Instruction ixor()

Overrides:

ixor in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

ior

public gov.nasa.jpf.vm.Instruction ior()

Overrides:

ior in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

irem

public gov.nasa.jpf.vm.Instruction irem()

Overrides:

irem in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

if_icmpeq

public gov.nasa.jpf.vm.Instruction if_icmpeq(int targetPc)

Overrides:

if_icmpeq in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

if_icmpne

public gov.nasa.jpf.vm.Instruction if_icmpne(int targetPc)

Overrides:

if_icmpne in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

fadd

public gov.nasa.jpf.vm.Instruction fadd()

Overrides:

fadd in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

fdiv

public gov.nasa.jpf.vm.Instruction fdiv()

Overrides:

fdiv in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

fmul

public gov.nasa.jpf.vm.Instruction fmul()

Overrides:

fmul in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

fneg

public gov.nasa.jpf.vm.Instruction fneg()

Overrides:

fneg in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

frem

public gov.nasa.jpf.vm.Instruction frem()

Overrides:

frem in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

fsub

public gov.nasa.jpf.vm.Instruction fsub()

Overrides:

fsub in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

fcmpg

public gov.nasa.jpf.vm.Instruction fcmpg()

Overrides:

fcmpg in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

fcmpl

public gov.nasa.jpf.vm.Instruction fcmpl()

Overrides:

fcmpl in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

dadd

public gov.nasa.jpf.vm.Instruction dadd()

Overrides:

dadd in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

dcmpg

public gov.nasa.jpf.vm.Instruction dcmpg()

Overrides:

dcmpg in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

dcmpl

public gov.nasa.jpf.vm.Instruction dcmpl()

Overrides:

dcmpl in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

ddiv

public gov.nasa.jpf.vm.Instruction ddiv()

Overrides:

ddiv in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

dmul

public gov.nasa.jpf.vm.Instruction dmul()

Overrides:

dmul in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

dneg

public gov.nasa.jpf.vm.Instruction dneg()

Overrides:

dneg in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

drem

public gov.nasa.jpf.vm.Instruction drem()

Overrides:

drem in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

dsub

public gov.nasa.jpf.vm.Instruction dsub()

Overrides:

dsub in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

ladd

public gov.nasa.jpf.vm.Instruction ladd()

Overrides:

ladd in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

land

public gov.nasa.jpf.vm.Instruction land()

Overrides:

land in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

lcmp

public gov.nasa.jpf.vm.Instruction lcmp()

Overrides:

lcmp in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

ldiv

public gov.nasa.jpf.vm.Instruction ldiv()

Overrides:

ldiv in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

lmul

public gov.nasa.jpf.vm.Instruction lmul()

Overrides:

lmul in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

lneg

public gov.nasa.jpf.vm.Instruction lneg()

Overrides:

lneg in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

lor

public gov.nasa.jpf.vm.Instruction lor()

Overrides:

lor in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

lrem

public gov.nasa.jpf.vm.Instruction lrem()

Overrides:

lrem in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

lshl

public gov.nasa.jpf.vm.Instruction lshl()

Overrides:

lshl in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

lshr

public gov.nasa.jpf.vm.Instruction lshr()

Overrides:

lshr in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

lsub

public gov.nasa.jpf.vm.Instruction lsub()

Overrides:

lsub in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

lushr

public gov.nasa.jpf.vm.Instruction lushr()

Overrides:

lushr in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

lxor

public gov.nasa.jpf.vm.Instruction lxor()

Overrides:

lxor in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

i2d

public gov.nasa.jpf.vm.Instruction i2d()

Overrides:

i2d in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

d2i

public gov.nasa.jpf.vm.Instruction d2i()

Overrides:

d2i in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

d2l

public gov.nasa.jpf.vm.Instruction d2l()

Overrides:

d2l in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

i2f

public gov.nasa.jpf.vm.Instruction i2f()

Overrides:

i2f in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

l2d

public gov.nasa.jpf.vm.Instruction l2d()

Overrides:

l2d in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

l2f

public gov.nasa.jpf.vm.Instruction l2f()

Overrides:

l2f in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

f2l

public gov.nasa.jpf.vm.Instruction f2l()

Overrides:

f2l in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

f2i

public gov.nasa.jpf.vm.Instruction f2i()

Overrides:

f2i in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

lookupswitch

public gov.nasa.jpf.vm.Instruction lookupswitch(int defaultTargetPc,
                                                int nEntries)

Overrides:

lookupswitch in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

tableswitch

public gov.nasa.jpf.vm.Instruction tableswitch(int defaultTargetPc,
                                               int low,
                                               int high)

Overrides:

tableswitch in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

d2f

public gov.nasa.jpf.vm.Instruction d2f()

Overrides:

d2f in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

f2d

public gov.nasa.jpf.vm.Instruction f2d()

Overrides:

f2d in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

i2b

public gov.nasa.jpf.vm.Instruction i2b()

Overrides:

i2b in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

i2c

public gov.nasa.jpf.vm.Instruction i2c()

Overrides:

i2c in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

i2s

public gov.nasa.jpf.vm.Instruction i2s()

Overrides:

i2s in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

i2l

public gov.nasa.jpf.vm.Instruction i2l()

Overrides:

i2l in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

l2i

public gov.nasa.jpf.vm.Instruction l2i()

Overrides:

l2i in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

getfield

public gov.nasa.jpf.vm.Instruction getfield(java.lang.String fieldName,
                                            java.lang.String clsName,
                                            java.lang.String fieldDescriptor)

Overrides:

getfield in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

getstatic

public gov.nasa.jpf.vm.Instruction getstatic(java.lang.String fieldName,
                                             java.lang.String clsName,
                                             java.lang.String fieldDescriptor)

Overrides:

getstatic in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

arraylength

public gov.nasa.jpf.vm.Instruction arraylength()

Overrides:

arraylength in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

aaload

public gov.nasa.jpf.vm.Instruction aaload()

Overrides:

aaload in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

aastore

public gov.nasa.jpf.vm.Instruction aastore()

Overrides:

aastore in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

baload

public gov.nasa.jpf.vm.Instruction baload()

Overrides:

baload in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

bastore

public gov.nasa.jpf.vm.Instruction bastore()

Overrides:

bastore in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

caload

public gov.nasa.jpf.vm.Instruction caload()

Overrides:

caload in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

castore

public gov.nasa.jpf.vm.Instruction castore()

Overrides:

castore in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

daload

public gov.nasa.jpf.vm.Instruction daload()

Overrides:

daload in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

dastore

public gov.nasa.jpf.vm.Instruction dastore()

Overrides:

dastore in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

faload

public gov.nasa.jpf.vm.Instruction faload()

Overrides:

faload in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

fastore

public gov.nasa.jpf.vm.Instruction fastore()

Overrides:

fastore in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

iaload

public gov.nasa.jpf.vm.Instruction iaload()

Overrides:

iaload in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

iastore

public gov.nasa.jpf.vm.Instruction iastore()

Overrides:

iastore in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

laload

public gov.nasa.jpf.vm.Instruction laload()

Overrides:

laload in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

lastore

public gov.nasa.jpf.vm.Instruction lastore()

Overrides:

lastore in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

saload

public gov.nasa.jpf.vm.Instruction saload()

Overrides:

saload in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

sastore

public gov.nasa.jpf.vm.Instruction sastore()

Overrides:

sastore in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

new_

public gov.nasa.jpf.vm.Instruction new_(java.lang.String clsName)

Overrides:

new_ in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

ifnonnull

public gov.nasa.jpf.vm.Instruction ifnonnull(int targetPc)

Overrides:

ifnonnull in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

ifnull

public gov.nasa.jpf.vm.Instruction ifnull(int targetPc)

Overrides:

ifnull in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

newarray

public gov.nasa.jpf.vm.Instruction newarray(int typeCode)

Overrides:

newarray in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

anewarray

public gov.nasa.jpf.vm.Instruction anewarray(java.lang.String typeDescriptor)

Overrides:

anewarray in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

multianewarray

public gov.nasa.jpf.vm.Instruction multianewarray(java.lang.String clsName,
                                                  int dimensions)

Overrides:

multianewarray in class gov.nasa.jpf.jvm.bytecode.InstructionFactory

setupGreen

private void setupGreen(gov.nasa.jpf.Config conf)