java_bytecode Directory Reference

Directory dependency graph for java_bytecode:

Files
	assignments_from_json.cpp
	assignments_from_json.h
	bytecode_info.cpp
	bytecode_info.h
	character_refine_preprocess.cpp
	Preprocess a goto-programs so that calls to the java Character library are replaced by simple expressions.
	character_refine_preprocess.h
	Preprocess a goto-programs so that calls to the java Character library are replaced by simple expressions.
	ci_lazy_methods.cpp
	ci_lazy_methods.h
	Collect methods needed to be loaded using the lazy method.
	ci_lazy_methods_needed.cpp
	Context-insensitive lazy methods container.
	ci_lazy_methods_needed.h
	Context-insensitive lazy methods container.
	code_with_references.cpp
	code_with_references.h
	convert_java_nondet.cpp
	Convert side_effect_expr_nondett expressions.
	convert_java_nondet.h
	Convert side_effect_expr_nondett expressions using java_object_factory.
	create_array_with_type_intrinsic.cpp
	Implementation of CProver.createArrayWithType intrinsic.
	create_array_with_type_intrinsic.h
	Implementation of CProver.createArrayWithType intrinsic.
	expr2java.cpp
	expr2java.h
	generic_parameter_specialization_map.cpp
	generic_parameter_specialization_map.h
	generic_parameter_specialization_map_keys.cpp
	generic_parameter_specialization_map_keys.h
	Author: Diffblue Ltd.
	jar_file.cpp
	jar_file.h
	jar_pool.cpp
	jar_pool.h
	java_bmc_util.cpp
	Bounded Model Checking Utils for Java.
	java_bmc_util.h
	Bounded Model Checking Utils for Java.
	java_bytecode_concurrency_instrumentation.cpp
	java_bytecode_concurrency_instrumentation.h
	java_bytecode_convert_class.cpp
	JAVA Bytecode Language Conversion.
	java_bytecode_convert_class.h
	JAVA Bytecode Language Conversion.
	java_bytecode_convert_method.cpp
	JAVA Bytecode Language Conversion.
	java_bytecode_convert_method.h
	JAVA Bytecode Language Conversion.
	java_bytecode_convert_method_class.h
	JAVA Bytecode Language Conversion.
	java_bytecode_instrument.cpp
	java_bytecode_instrument.h
	java_bytecode_internal_additions.cpp
	java_bytecode_internal_additions.h
	java_bytecode_language.cpp
	java_bytecode_language.h
	java_bytecode_parse_tree.cpp
	java_bytecode_parse_tree.h
	java_bytecode_parser.cpp
	java_bytecode_parser.h
	java_bytecode_typecheck.cpp
	JAVA Bytecode Conversion / Type Checking.
	java_bytecode_typecheck.h
	JAVA Bytecode Language Type Checking.
	java_bytecode_typecheck_code.cpp
	JAVA Bytecode Conversion / Type Checking.
	java_bytecode_typecheck_expr.cpp
	JAVA Bytecode Conversion / Type Checking.
	java_bytecode_typecheck_type.cpp
	JAVA Bytecode Conversion / Type Checking.
	java_class_loader.cpp
	java_class_loader.h
	java_class_loader_base.cpp
	java_class_loader_base.h
	java_class_loader_limit.cpp
	limit class path loading
	java_class_loader_limit.h
	limit class path loading
	java_entry_point.cpp
	java_entry_point.h
	java_enum_static_init_unwind_handler.cpp
	Unwind loops in static initializers.
	java_enum_static_init_unwind_handler.h
	Unwind loops in static initializers.
	java_expr.h
	Java-specific exprt subclasses.
	java_local_variable_table.cpp
	Java local variable table processing.
	java_multi_path_symex_checker.cpp
	java_multi_path_symex_checker.h
	Goto Checker using Bounded Model Checking for Java.
	java_multi_path_symex_only_checker.h
	Goto Checker using Bounded Model Checking for Java.
	java_object_factory.cpp
	java_object_factory.h
	This module is responsible for the synthesis of code (in the form of a sequence of codet statements) that can allocate and initialize non-deterministically both primitive Java types and objects.
	java_object_factory_parameters.cpp
	java_object_factory_parameters.h
	java_pointer_casts.cpp
	JAVA Pointer Casts.
	java_pointer_casts.h
	JAVA Pointer Casts.
	java_qualifiers.cpp
	Java-specific type qualifiers.
	java_qualifiers.h
	Java-specific type qualifiers.
	java_root_class.cpp
	java_root_class.h
	java_single_path_symex_checker.cpp
	java_single_path_symex_checker.h
	Goto Checker using Single Path Symbolic Execution for Java.
	java_single_path_symex_only_checker.h
	Goto Checker using Single Path Symbolic Execution for Java.
	java_static_initializers.cpp
	java_static_initializers.h
	java_string_library_preprocess.cpp
	Java_string_libraries_preprocess, gives code for methods on strings of the java standard library.
	java_string_library_preprocess.h
	Produce code for simple implementation of String Java libraries.
	java_string_literal_expr.h
	Representation of a constant Java string.
	java_string_literals.cpp
	java_string_literals.h
	java_trace_validation.cpp
	java_trace_validation.h
	java_types.cpp
	java_types.h
	java_utils.cpp
	java_utils.h
	lambda_synthesis.cpp
	Java lambda code synthesis.
	lambda_synthesis.h
	Java lambda code synthesis.
	lazy_goto_functions_map.h
	Author: Diffblue Ltd.
	lazy_goto_model.cpp
	Author: Diffblue Ltd.
	lazy_goto_model.h
	Author: Diffblue Ltd.
	lift_clinit_calls.cpp
	lift_clinit_calls.h
	load_method_by_regex.cpp
	load_method_by_regex.h
	Process a pattern to use as a regex for selecting extra entry points for ci_lazy_methodst.
	mz_zip_archive.cpp
	mz_zip_archive.h
	nondet.cpp
	nondet.h
	pattern.h
	Pattern matching for bytecode instructions.
	remove_exceptions.cpp
	Remove exception handling.
	remove_exceptions.h
	Remove function exceptional returns.
	remove_instanceof.cpp
	Remove Instance-of Operators.
	remove_instanceof.h
	Remove Instance-of Operators.
	remove_java_new.cpp
	Remove Java New Operators.
	remove_java_new.h
	Remove Java New Operators.
	replace_java_nondet.cpp
	Replace Java Nondet expressions.
	replace_java_nondet.h
	Replace Java Nondet expressions.
	select_pointer_type.cpp
	Handle selection of correct pointer type (for example changing abstract classes to concrete versions).
	select_pointer_type.h
	Handle selection of correct pointer type (for example changing abstract classes to concrete versions).
	simple_method_stubbing.cpp
	Java simple opaque stub generation.
	simple_method_stubbing.h
	Java simple opaque stub generation.
	synthetic_methods_map.h
	Synthetic methods are particular methods internally generated by the Java frontend, including thunks to ensure static initializers are run once and initializers created for unknown / stub types.