Here is a list of all functions with links to the files they belong to:

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

R

S

T

U

V

W

X

Y

Z

_

- a -

• accelerate_functions() : accelerate.cpp, accelerate.h
• actuals_replace_map() : instrument_preconditions.cpp
• add_array_to_length_association() : java_string_library_preprocess.cpp, java_string_library_preprocess.h
• add_axioms_for_format() : string_format_builtin_function.cpp
• add_axioms_for_format_specifier() : string_format_builtin_function.cpp
• add_character_set_constraint() : java_string_library_preprocess.cpp, java_string_library_preprocess.h
• add_checked_pragmas() : dfcc_library.cpp
• add_dependency_to_string_subexprs() : string_dependencies.cpp
• add_equations_for_symbol_resolution() : string_refinement.cpp
• add_failed_symbol() : add_failed_symbols.cpp
• add_failed_symbol_if_needed() : add_failed_symbols.cpp, add_failed_symbols.h
• add_failed_symbols() : add_failed_symbols.cpp, add_failed_symbols.h
• add_format_hook() : format_expr.cpp, format_expr.h
• add_function() : instrument_contracts.cpp
• add_generic_type_information() : java_types.cpp
• add_initialize_call() : statement_list_entry_point.cpp
• add_java_array_types() : java_bytecode_convert_class.cpp, java_bytecode_convert_class.h
• add_keys_to_container() : java_string_library_preprocess.cpp
• add_library() : cprover_library.cpp, cprover_library.h
• add_main_function_block_call() : statement_list_entry_point.cpp
• add_new_variable_symbol() : java_static_initializers.cpp
• add_node() : string_dependencies.cpp, string_dependencies.h, graphml.cpp
• add_one_function() : link_to_library.cpp
• add_or_get_symbol() : java_bytecode_concurrency_instrumentation.cpp
• add_padding() : padding.cpp, padding.h
• add_padding_gcc() : padding.cpp
• add_padding_msvc() : padding.cpp
• add_parameter() : dfcc_utils.cpp
• add_pointer_to_array_association() : java_string_library_preprocess.cpp, java_string_library_preprocess.h
• add_pragma_disable_assigns_check() : instrument_spec_assigns.cpp, instrument_spec_assigns.h
• add_pragma_disable_pointer_checks() : instrument_spec_assigns.cpp, instrument_spec_assigns.h
• add_propagate_static_local_pragma() : instrument_spec_assigns.cpp, instrument_spec_assigns.h
• add_stack_depth_symbol() : stack_depth.cpp
• add_string_equation_to_symbol_resolution() : string_refinement.cpp
• add_to_index_set() : string_refinement.cpp
• add_to_json() : unreachable_instructions.cpp
• add_to_xml() : unreachable_instructions.cpp
• add_uninitialized_locals_assertions() : uninitialized.cpp, uninitialized.h
• address_bits() : arith_tools.cpp, arith_tools.h
• address_taken() : address_taken.cpp, address_taken.h
• address_to_lvalue() : report_traces.cpp
• adjust_array_types() : shadow_memory_util.cpp
• adjust_byte_extract_rec() : symex_clean_expr.cpp
• adjust_float_expressions() : adjust_float_expressions.cpp, adjust_float_expressions.h
• adjust_invoke_argument_types() : java_bytecode_convert_method.cpp
• adjust_type_if_necessary() : lambda_synthesis.cpp
• adjust_width() : lower_byte_operators.cpp
• advance_to_next_key() : java_static_initializers.cpp
• aliasing() : wp.cpp
• align_center_with_border() : parse_options.cpp, parse_options.h
• alignment() : padding.cpp, padding.h
• all_dereferences_are_valid() : utils.cpp, utils.h
• all_subs_are_pairs() : smt_response_validation.cpp
• all_symbols_in_scope() : graphml_witness.cpp
• all_unreachable() : unreachable_instructions.cpp
• allocate_array() : code_with_references.cpp, code_with_references.h
• allocate_nondet_length_array() : java_object_factory.cpp
• alt_copy_segment() : goto2graph.cpp
• analyse_checks_directly_preceding_function_call() : remove_virtual_functions.cpp
• and_fkt() : miniBDD.cpp
• annotate_assigns() : utils.cpp, utils.h
• annotate_decreases() : utils.cpp, utils.h
• annotate_invariants() : utils.cpp, utils.h
• ansi_c_architecture_strings() : ansi_c_internal_additions.cpp, ansi_c_internal_additions.h
• ansi_c_entry_point() : ansi_c_entry_point.cpp, ansi_c_entry_point.h
• ansi_c_internal_additions() : ansi_c_internal_additions.cpp, ansi_c_internal_additions.h
• ansi_c_scanner_init() : ansi_c_parser.h
• ansi_c_typecheck() : ansi_c_typecheck.cpp, ansi_c_typecheck.h
• any_intervals() : abstract_value_object.cpp
• any_of_type() : abstract_value_object.cpp
• any_value_sets() : abstract_value_object.cpp
• api_message_get_string() : api.cpp, api.h
• api_message_is_error() : api.cpp, api.h
• append_numbers() : format_number_range.cpp
• append_safe_havoc_code_for_expr() : utils.cpp
• append_universal_char() : unescape_string.cpp
• apply_to_index_range() : full_array_abstract_object.cpp
• apply_to_objects_in_dereference() : symex_dereference.cpp
• approximate_nondet() : wp.cpp, wp.h
• approximate_nondet_rec() : wp.cpp
• architecture_string() : ansi_c_internal_additions.cpp
• are_any_top() : value_set_abstract_object.cpp
• are_types_compatible() : shadow_memory_util.cpp
• arg_is_type_compatible() : remove_function_pointers.cpp
• arith_left_shift() : mp_arith.cpp, mp_arith.h
• arith_right_shift() : mp_arith.cpp, mp_arith.h
• array_element_from_pointer() : array_element_from_pointer.cpp, array_element_from_pointer.h
• array_loop_init_code() : java_object_factory.cpp
• array_name() : array_name.cpp, array_name.h
• array_primitive_init_code() : java_object_factory.cpp
• as_const() : as_const.h
• as_const_ptr() : as_const.h
• as_string() : static_verifier.cpp, static_verifier.h, properties.cpp, properties.h, goto_program.cpp, goto_program.h, dstring.h
• as_value() : abstract_environment.cpp
• as_vcd_binary() : vcd_goto_trace.cpp
• assembler_name() : as_mode.cpp
• assert_type_consistency() : java_object_factory.cpp
• assign_array_data_component_from_json() : assignments_from_json.cpp
• assign_det_length_array_from_json() : assignments_from_json.cpp
• assign_enum_from_json() : assignments_from_json.cpp
• assign_from_json() : assignments_from_json.cpp, assignments_from_json.h
• assign_from_json_rec() : assignments_from_json.cpp
• assign_non_enum_pointer_from_json() : assignments_from_json.cpp
• assign_nondet_length_array_from_json() : assignments_from_json.cpp
• assign_null() : assignments_from_json.cpp
• assign_parameter_names() : java_bytecode_convert_method.cpp
• assign_pointer_from_json() : assignments_from_json.cpp
• assign_pointer_with_given_type_from_json() : assignments_from_json.cpp
• assign_primitive_from_json() : assignments_from_json.cpp
• assign_reference_from_json() : assignments_from_json.cpp
• assign_string_from_json() : assignments_from_json.cpp
• assign_struct_components_from_json() : assignments_from_json.cpp
• assign_struct_from_json() : assignments_from_json.cpp
• assigns_match() : instrument_contracts.cpp
• associate_pointer_sizes() : type_size_mapping.cpp, type_size_mapping.h
• assume_and() : abstract_environment.cpp
• assume_eq() : abstract_environment.cpp
• assume_eq_unbounded() : abstract_environment.cpp
• assume_expr_integral() : java_object_factory.cpp
• assume_greater_than() : abstract_environment.cpp
• assume_less_than() : abstract_environment.cpp
• assume_less_than_unbounded() : abstract_environment.cpp
• assume_not() : abstract_environment.cpp
• assume_noteq() : abstract_environment.cpp
• assume_or() : abstract_environment.cpp
• at_scope_exit() : convert_expr_to_smt.cpp
• attempt_assign_length_from_type() : array_pool.cpp