All Classes and Interfaces
Class
Description
AALOAD - Load reference from array.
AASTORE - Store into reference array For more information see the Java VM
specification.
AbstractArrayValue<TI extends org.sosy_lab.java_smt.api.Formula,TE extends org.sosy_lab.java_smt.api.Formula,VI extends Value<?,?>,VE extends Value<?,?>,K>
Abstract class for symbolic arrays.
Template Method pattern for processing instruction processing.
ACONST_NULL - Push null.
ALOAD - Load reference from local variable.
ANEWARRAY - Create new array of reference.
ARETURN - Return reference from method.
ArrayArrayValue<TE extends org.sosy_lab.java_smt.api.Formula>
ARRAYLENGTH - Get length of array.
ASTORE -Store reference into local variable.
ATHROW - Throw exception or error.
BALOAD - Load byte or boolean from array.
BASTORE - Store into byte or boolean array.
BIPUSH - Push byte.
Wrapper for Arrays that contain boolean values.
Wrapper to represent boolean values on the symbolic stack.
Wrapper for Arrays that contain byte values.
Wrapper to represent byte values on the symbolic stack.
CALOAD - Load char from array.
CASTORE - Store into char array.
Wrapper for Arrays that contain char values.
CHECKCAST - Check whether object is of given type.
Serializable depot for classes represented using their name and a corresponding class template in
a tree map
The Config class is responsible for reading the configuration file and providing the application
with the configuration options.
Sends the constraints recorded during symbolic execution to the symbolic explorer.
D2F - Convert double to float.
D2I - Convert double to int.
D2F - Convert double to long.
DADD - Add double.
DALOAD - Load double from array.
DASTORE - Store into double array.
Represents the different data types that can be encountered in method descriptors.
DCMPG - Compare double (greater than).
DCMPL - Compare double (less than).
DCONST_0 - Push double (0.0d).
DCONST_1 - Push double (1.0d).
DDIV - Divide double.
DLOAD - Load double from local variable.
DMUL - Convert double to float.
DNEG - Negate double.
Wrapper for Arrays that contain double values.
Wrapper for doubles to represent symbolic and concrete information on the symbolic stack
DREM - Remainder double.
DRETURN - Return double from method.
DSTORE - Store double into local variable.
DSUB - Subtract double.
DUP - Duplicate the top operand stack value.
DUP_X1 - Duplicate the top operand stack value and insert two values down.
DUP_X2 - Duplicate the top operand stack value and insert two or three values down.
DUP2 - Duplicate the top one or two operand stack values.
DUP2_X1 - Duplicate the top one or two operand stack values and insert two or three values down.
DUP2_X2 - Duplicate the top one or two operand stack values and insert two, three, or four values
down.
ErrorHandler is responsible for handling exceptions throughout the application.
F2D - Convert float to double.
F2I - Convert float to int.
F2L - Convert float to long.
FADD - Add float.
FALOAD - Load float from array.
FASTORE - Store into float array.
FCMPG - Compare float (greater than).
FCMPL - Compare float (less than).
FCONST_0 - Push float (0.0f).
FCONST_1 - Push float (1.0f).
FCONST_2 - Push float (2.0f).
FDIV - Divide float.
FLOAD - Load float from local variable.
FMUL - Multiply float.
FNEG - Negate float.
A symbolic Stack Frame that stores Values in the symbolic Stack and symbolic locals
FREM - Remainder float.
FRETURN - Return float from method.
FSTORE - Store float into local variable.
FSUB - Subtract float.
GETFIELD - Fetch field from object.
GETSTATIC - Get static field from class.
GETVALUE_boolean - Custom method call handled as an instruction to fetch the concrete value that
was produced/ loaded by another instruction.
GETVALUE_byte - Custom method call handled as an instruction to fetch the concrete value that was
produced/ loaded by another instruction.
GETVALUE_char - Custom method call handled as an instruction to fetch the concrete value that was
produced/ loaded by another instruction.
GETVALUE_double - Custom method call handled as an instruction to fetch the concrete value that
was produced/ loaded by another instruction.
GETVALUE_float - Custom method call handled as an instruction to fetch the concrete value that
was produced/ loaded by another instruction.
GETVALUE_int - Custom method call handled as an instruction to fetch the concrete value that was
produced/ loaded by another instruction.
GETVALUE_long - Custom method call handled as an instruction to fetch the concrete value that was
produced/ loaded by another instruction.
GETVALUE_Object - Custom method call handled as an instruction to fetch the concrete value that
was produced/ loaded by another instruction.
GETVALUE_short - Custom method call handled as an instruction to fetch the concrete value that
was produced/ loaded by another instruction.
GETVALUE_void - Custom method call handled as an instruction to fetch the concrete value that was
produced/ loaded by another instruction.
An object to keep track of (classId, methodId, instructionId) tuples during instrumentation.
GOTO - Branch always.
I2B - Convert int to byte.
I2C - Convert int to character.
I2D - Convert int to double.
I2F - Convert int to float.
I2L - Convert int to long.
I2S - Convert int to short.
IADD - Add int.
IALOAD - Load int from array.
IAND - Boolean AND int.
IASTORE - Store into int array.
ICONST_0 - Push int constant (0).
ICONST_1 - Push int constant (1).
ICONST_2 - Push int constant (2).
ICONST_3 - Push int constant (3).
ICONST_4 - Push int constant (4).
ICONST_5 - Push int constant (5).
ICONST_M1 - Push int constant (-1).
IDIV - Divide int.
IF_ACMPEQ - Branch if reference comparison succeeds (equals) For more information see the Java
VM specification.
IF_ACMPNE - Branch if reference comparison succeeds (not equals) For more information see the Java
VM specification.
IF_ICMPEQ - Branch if int comparison succeeds (equals) For more information see the Java
VM specification.
IF_ICMPGE - Branch if int comparison succeeds (greater or equals) For more information see the Java
VM specification.
IF_ICMPGT - Branch if int comparison succeeds (greater than) For more information see the Java
VM specification.
IF_ICMPLE - Branch if int comparison succeeds (less or equals) For more information see the Java
VM specification.
IF_ICMPLT - Branch if int comparison succeeds (less than) For more information see the Java
VM specification.
IF_ICMPNE - Branch if int comparison succeeds (not equals) For more information see the Java
VM specification.
IFEQ - Branch if int comparison with zero succeeds (equal) For more information see the Java VM
specification.
IFGE - Branch if int comparison with zero succeeds (greater or equal) For more information see
the Java VM
specification.
IFGT - Branch if int comparison with zero succeeds (greater than) For more information see the Java VM
specification.
IFLE - Branch if int comparison with zero succeeds (less than) For more information see the Java VM
specification.
IFLT - Branch if int comparison with zero succeeds (less than) For more information see the Java VM
specification.
IFNE - Branch if int comparison with zero succeeds (not equal) For more information see the Java VM
specification.
IFNONNULL - Branch if reference not null.
IFNULL - Branch if reference is null.
IINC - Increment local variable by constant.
ILOAD - Load int from local variable.
IMUL - Multiply int.
INEG - Negate int.
INSTANCEOF - Determine if object is of given type.
Base class for all instructions.
A visitor to visit a Java class.
A visitor to visit a Java method
Interface for instruction handling.
An agent provides an implementation of this interface in order to transform class files.
Wrapper for Arrays that contain integer values.
IntValue contains a pair of concrete value and a path constraint.
INVOKEDYNAMIC - Invoke a dynamically-computed call site.
INVOKEINTERFACE - Invoke interface method.
INVOKEMETHOD_END - Custom method handled as an instruction to signalize a method end.
INVOKEMETHOD_EXCEPTION - Custom method handled as an instruction to signalize a method end.
INVOKESPECIAL - Invoke instance method; direct invocation of instance initialization methods and
methods of the current class and its supertypes.
INVOKESTATIC - Invoke a class (static) method.
INVOKEVIRTUAL - Invoke instance method; dispatch based on class.
IOR - Boolean OR int.
IREM - Remainder int.
IRETURN - Return int from method.
ISHL - Shift left int.
ISHR - Arithmetic shift right int.
ISTORE - Store int into local variable.
ISUB - Subtract int.
IUSHR - Logical shift right int.
IXOR - Boolean XOR int.
JSR - Jump subroutine.
L2D - Convert long to double.
L2F - Convert long to float.
L2I - Convert long to int.
LADD - Add long.
LALOAD - Load long from array.
LAND - Boolean AND long.
LASTORE - Store into long array.
LCMP - Compare long.
LCONST_0 - Push long constant (0L).
LCONST_1 - Push long constant (1L).
LDC(_double) - Push item from run-time constant pool.
LDC(_float) - Push item from run-time constant pool.
LDC(_int) - Push item from run-time constant pool.
LDC(_long) - Push item from run-time constant pool.
LDC(_Object) - Push item from run-time constant pool.
LDC(_String) - Push item from run-time constant pool.
LDIV - Divide long.
LLOAD - Load long from local variable.
LMUL - Multiply long.
LNEG - Negate long.
This class can is used to directly communicate with the solver (currently Z3).
Wrapper for longs to represent symbolic and concrete information on the symbolic stack
LOOKUPSWITCH - Access jump table by key match and jump.
LOOP_BEGIN - Custom method call handled as an instruction to detect the beginning of loops.
LOOP_END - Custom method call handled as an instruction to detect the end of loops.
LOR - Boolean OR long.
LREM - Remainder long.
LRETURN - Return long from method.
LSHL - Shift left long.
LSHR - Arithmetic shift right long For more information see the Java VM
specification.
LSTORE - Store long into local variable.
LSUB - Subtract long.
LUSHR - Logical shift right long.
LXOR - Boolean XOR long.
Main runtime environment for parsing inputs and writing state files.
MAKE_SYMBOLIC - Custom method call handled as an instruction to initiate symbolic tracking of
variables.
MONITORENTER - Enter monitor for object.
MONITOREXIT - Exit monitor for object.
MULTIANEWARRAY - Create new multidimensional array.
NEW - Create new object.
NEWARRAY - Create new array.
NOP - Do nothing.
Wrapper for arrays of references (non-primitive types)
Containing the static info of a class and dynamic values of the static fields.
A visitor to visit a Java class.
A visitor to visit a Java method This class makes every parameter of the passed function
symbolic.
An agent provides an implementation of this interface in order to transform class files.
Author: Koushik Sen (ksen@cs.berkeley.edu) Date: 6/17/12 Time: 6:05 PM
POP - Pop the top operand stack value.
POP2 - Pop the top one or two operand stack values.
This class represents a utility for printing messages inside a box structure.
PUTFIELD - Set field in object.
PUTSTATIC - Set static field in class.
RET - Return from subroutine.
RETURN - Return void from method.
A ClassWriter that computes the common super class of two classes without actually loading them
with a ClassLoader.
SALOAD - Load short from array.
SASTORE - Store into short array.
Wrapper for shorts to represent symbolic and concrete information on the symbolic stack
SIPUSH - Push short.
All available solver modes.
A special probe instruction added by the instrumentation.
Wrapper for Arrays that contain String values.
A visitor to visit a Java method This class surrounds the whole function with a try catch blog to
ad a solve in case of an error.
A visitor to visit a Java class.
A visitor to visit a Java method
An agent provides an implementation of this interface in order to transform class files.
SWAP - Swap the top two operand stack values.
This class is used to process instructions and triggers symbolic execution handling through
visiting the current instruction.
Manages access to the trace of the symbolic execution.
A visitor to visit a Java class.
An agent provides an implementation of this interface in order to transform class files.
TABLESWITCH - Access jump table by index and jump.
This class runs all the different transformers.
Author: Koushik Sen (ksen@cs.berkeley.edu) Date: 7/1/12 Time: 10:50 PM
Abstract value of any type.