cprover
|
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. | |