JCHPreAPI
type cmd_t = (CHLanguage.code_int, CHLanguage.cfg_int) CHLanguage.command_t
class type cmd_list_int = object ... end
class type code_graph_int = object ... end
class type system_settings_int = object ... end
class type signature_bindings_int = object ... end
class type class_summary_int = object ... end
class type bytecode_location_int = object ... end
class type operation_locations_int = object ... end
class type j_invariant_int = object ... end
class type invariants_int = object ... end
class type field_stub_int = object ... end
type field_info_type_t =
| ConcreteField of JCHBasicTypesAPI.field_int
| StubbedField of field_stub_int
| MissingField of JCHBasicTypesAPI.class_field_signature_int
class type field_info_int = object ... end
type class_info_type_t =
| ConcreteClass of JCHBasicTypesAPI.java_class_or_interface_int
| InterfaceType of JCHBasicTypesAPI.java_class_or_interface_int
| AbstractClass of JCHBasicTypesAPI.java_class_or_interface_int
| StubbedClass of class_summary_int
| MissingClass of JCHBasicTypesAPI.class_name_int
class type class_info_int = object ... end
type loop_info_t = {
li_first_pc : int;
li_entry_pc : int;
li_last_pc : int;
li_instr_count : int;
li_cond_pcs : int list;
li_inner_loops : (int * int) list;
li_outer_loops : (int * int) list;
li_max_iterations : JCHBasicTypesAPI.jterm_t list;
li_pc_invariants : (int * JCHBasicTypesAPI.relational_expr_t list) list;
li_calls : (int * int * int) list;
}
type method_loop_infos_t =
JCHBasicTypesAPI.class_method_signature_int * loop_info_t list
type bc_basicvalue_t =
| BcvArg of int
| BcvIntConst of CHNumerical.numerical_t
| BcvLongConst of CHNumerical.numerical_t
| BcvByteConst of CHNumerical.numerical_t
| BcvShortConst of CHNumerical.numerical_t
| BcvDoubleConst of float
| BcvFloatConst of float
| BcvArrayElement of JCHBasicTypesAPI.java_basic_type_t
* bc_objectvalue_t
* bc_basicvalue_t
| BcvThisField of JCHBasicTypesAPI.class_name_int
* JCHBasicTypesAPI.field_signature_int
| BcvThatField of JCHBasicTypesAPI.class_name_int
* JCHBasicTypesAPI.field_signature_int
* bc_objectvalue_t
| BcvStaticField of JCHBasicTypesAPI.class_name_int
* JCHBasicTypesAPI.field_signature_int
| BcvArrayLength of bc_objectvalue_t
| BcvInstanceOf of JCHBasicTypesAPI.object_type_t * bc_objectvalue_t
| BcvBinOpResult of JCHBasicTypesAPI.opcode_t * bc_basicvalue_t * bc_basicvalue_t
| BcvUnOpResult of JCHBasicTypesAPI.opcode_t * bc_basicvalue_t
| BcvQResult of JCHBasicTypesAPI.opcode_t list
* bc_value_t list
* bc_basicvalue_t
* bc_basicvalue_t
| BcvConvert of JCHBasicTypesAPI.opcode_t * bc_basicvalue_t
| BcvCallRv of bc_call_t
and bc_objectvalue_t =
| BcoArg of int
| BcoNull
| BcoClassConst of JCHBasicTypesAPI.object_type_t
| BcoStringConst of string
| BcoNewObject of JCHBasicTypesAPI.class_name_int * bc_value_t list
| BcoNewArray of JCHBasicTypesAPI.value_type_t * bc_basicvalue_t
| BcoMultiNewArray of JCHBasicTypesAPI.object_type_t * bc_basicvalue_t list
| BcoArrayElement of JCHBasicTypesAPI.java_basic_type_t
* bc_objectvalue_t
* bc_basicvalue_t
| BcoThisField of JCHBasicTypesAPI.class_name_int
* JCHBasicTypesAPI.field_signature_int
| BcoThatField of JCHBasicTypesAPI.class_name_int
* JCHBasicTypesAPI.field_signature_int
* bc_objectvalue_t
| BcoStaticField of JCHBasicTypesAPI.class_name_int
* JCHBasicTypesAPI.field_signature_int
| BcoCheckCast of JCHBasicTypesAPI.object_type_t * bc_objectvalue_t
| BcoQResult of JCHBasicTypesAPI.opcode_t list
* bc_value_t list
* bc_objectvalue_t
* bc_objectvalue_t
| BcoCallRv of bc_call_t
and bc_call_t = {
bcp_type : string;
bcp_base_object : bc_objectvalue_t option;
bcp_base_type : JCHBasicTypesAPI.object_type_t;
bcp_ms : JCHBasicTypesAPI.method_signature_int;
bcp_args : bc_value_t list;
}
type bc_action_t =
| BcNop
| BcNopX
| BcInitObject
| BcInitSuper
| BcNewObject of JCHBasicTypesAPI.class_name_int * bc_value_t list
| BcDropValues of bc_value_t list
| BcPutThisField of JCHBasicTypesAPI.class_name_int
* JCHBasicTypesAPI.field_signature_int
* bc_value_t
| BcPutThatField of JCHBasicTypesAPI.class_name_int
* JCHBasicTypesAPI.field_signature_int
* bc_objectvalue_t
* bc_value_t
| BcPutStaticField of JCHBasicTypesAPI.class_name_int
* JCHBasicTypesAPI.field_signature_int
* bc_value_t
| BcArrayStore of JCHBasicTypesAPI.java_basic_type_t
* bc_objectvalue_t
* bc_basicvalue_t
* bc_value_t
| BcConditionalAction of JCHBasicTypesAPI.opcode_t list
* bc_value_t list
* bc_action_t list
* bc_action_t list
| BcWrapCall of bc_call_t
| BcThrow of bc_objectvalue_t
type bc_action_value_t =
| BcaValue of bc_value_t
| BcaAction of bc_action_t
| BcaActions of bc_action_t list
| BcaTest of JCHBasicTypesAPI.opcode_t list * bc_value_t list
| BcaRetGoto of JCHBasicTypesAPI.opcode_t
| BcaOpcodes of JCHBasicTypesAPI.opcode_t list
| BcaRvActions of bc_action_t list * bc_value_t
type bc_pattern_t =
| BcpNop
| BcpNopX
| BcpAction of bc_action_t list
| BcpResult of bc_action_t list * bc_value_t
| BcpThrow of bc_action_t list * bc_objectvalue_t
| BcpResultExcept of JCHBasicTypesAPI.class_name_int
* bc_action_t list
* bc_value_t
* bc_value_t
| BcpResultExceptThrow of JCHBasicTypesAPI.class_name_int
* bc_action_t list
* bc_value_t
* bc_objectvalue_t
| BcpActionExcept of JCHBasicTypesAPI.class_name_int * bc_action_t list
| BcpActionExceptThrow of JCHBasicTypesAPI.class_name_int
* bc_action_t list
* bc_objectvalue_t
| BcpInfiniteLoop of bc_action_t list
| BcpIllegalSeq of string * JCHBasicTypesAPI.opcode_t list
type precondition_predicate_t =
| PreRelationalExpr of JCHBasicTypesAPI.relational_expr_t
| PreNull of JCHBasicTypesAPI.jterm_t
| PreNotNull of JCHBasicTypesAPI.jterm_t
| PreValidString of JCHBasicTypesAPI.jterm_t * string
type postcondition_predicate_t =
| PostRelationalExpr of JCHBasicTypesAPI.relational_expr_t
| PostTrue
| PostFalse
| PostNewObject of JCHBasicTypesAPI.class_name_int
| PostNull
| PostNotNull
| PostElement of JCHBasicTypesAPI.jterm_t
| PostEmptyCollection
| PostSameCollection of JCHBasicTypesAPI.jterm_t
| PostWrapped of JCHBasicTypesAPI.jterm_t
| PostUnwrapped
| PostValidString of string
| PostObjectClass of JCHBasicTypesAPI.class_name_int
class type postcondition_int = object ... end
type sideeffect_t =
| NumericJoin of JCHBasicTypesAPI.jterm_t
* JCHBasicTypesAPI.jterm_t
* JCHBasicTypesAPI.jterm_t
| NumericAbstract of JCHBasicTypesAPI.jterm_t
| SetValue of JCHBasicTypesAPI.jterm_t
| Wrap of JCHBasicTypesAPI.jterm_t * JCHBasicTypesAPI.jterm_t
| ConditionalSideEffect of precondition_predicate_t * sideeffect_t
type taint_element_t =
| TTransfer of JCHBasicTypesAPI.jterm_t * JCHBasicTypesAPI.jterm_t
| TRefEqual of JCHBasicTypesAPI.jterm_t * JCHBasicTypesAPI.jterm_t
| TDefPut of JCHBasicTypesAPI.jterm_t
| TRemove of JCHBasicTypesAPI.jterm_t
class type taint_int = object ... end
class type string_sink_int = object ... end
class type resource_sink_int = object ... end
class type exception_info_int = object ... end
class type function_summary_int = object ... end
type method_info_type_t =
| ConcreteMethod of JCHBasicTypesAPI.method_int
| UntranslatedConcreteMethod of JCHBasicTypesAPI.method_int
| Stub of function_summary_int
| NativeMethod of JCHBasicTypesAPI.method_int
| AbstractMethod of JCHBasicTypesAPI.method_int
| InterfaceInheritedMethod of JCHBasicTypesAPI.class_method_signature_int
| MissingMethod of JCHBasicTypesAPI.class_method_signature_int
| ExcludedMethod of JCHBasicTypesAPI.method_int * string
class type handler_block_int = object ... end
class type exception_handlers_int = object ... end
class type method_info_int = object ... end
class type bc_block_int = object ... end
class type bc_graph_int = object ... end
class type function_summary_library_int = object ... end
class type userdata_int = object ... end
class type costresults_int = object ... end
class type method_target_int = object ... end
class type instruction_info_int = object ... end
class type relational_invariant_int = object ... end
type taint_origin_type_t =
| T_ORIG_VAR of int * CHLanguage.variable_t
| T_ORIG_FIELD of int * string * int * int
| T_ORIG_CALL of int * string * int * int
| T_ORIG_TOP_TARGET of method_target_int * int * int
| T_ORIG_STUB of int * int * int
type taint_node_type_t =
| TN_FIELD of int
| TN_VAR of int * CHLanguage.variable_t * int
| TN_VAR_EQ of int
* CHLanguage.variable_t
* CHLanguage.variable_t
* CHLanguage.symbol_t list
| TN_CALL of int
* int
* int
* int
* CHLanguage.variable_t option
* CHLanguage.variable_t list
| TN_UNKNOWN_CALL of int
* int
* int
* CHLanguage.variable_t option
* CHLanguage.variable_t list
| TN_CONDITIONAL of int * int
| TN_OBJECT_FIELD of int * CHLanguage.variable_t * int * int
| TN_SIZE of int * CHLanguage.variable_t * int
| TN_REF_EQUAL
class type taint_dictionary_int = object ... end
class type taint_origin_int = object ... end
class type taint_origin_set_int = object ... end
class type taint_node_int = object ... end
class type application_int = object ... end
type call_targets_t =
| NonVirtualTarget of non_virtual_target_type_t * int
| ConstrainedVirtualTargets of string * int list
| VirtualTargets of int list
| EmptyTarget of bool
* JCHBasicTypesAPI.class_name_int
* JCHBasicTypesAPI.method_signature_int
class type method_signature_implementations_int = object ... end
class type cgdictionary_int = object ... end
class type callgraph_base_int = object ... end
class type method_summary_builder_int = object ... end
class type chif_system_int = object ... end
class type method_invariants_int = object ... end
class type tainted_variable_int = object ... end
class type method_taints_int = object ... end
class type class_analysis_results_int = object ... end
class type application_analysis_results_int = object ... end