java_bytecode Directory Reference

Directory dependency graph for java_bytecode:

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