- a -

• abort() : stdlib.c
• abs() : stdlib.c
• accelerate_functions() : accelerate.h , accelerate.cpp
• accept() : smt_logics.cpp , smt_commands.cpp , smt_terms.cpp , smt_options.cpp , smt_sorts.cpp
• 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.h , graphml.cpp , string_dependencies.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.h , java_string_library_preprocess.cpp
• add_pragma_disable_assigns_check() : instrument_spec_assigns.cpp , instrument_spec_assigns.h , 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_float_expressions.cpp
• 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_unreachable() : unreachable_instructions.cpp
• alloca() : stdlib.c
• 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.h , ansi_c_typecheck.cpp
• 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.h , mp_arith.cpp
• 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.h , dstring.h , goto_program.h , goto_program.cpp , properties.h , properties.cpp , static_verifier.cpp
• as_value() : abstract_environment.cpp
• as_vcd_binary() : vcd_goto_trace.cpp
• asctime() : time.c
• asprintf() : stdio.c
• assembler_name() : as_mode.cpp
• assert_type_consistency() : java_object_factory.cpp
• assign_from_json() : assignments_from_json.h
• assign_parameter_names() : java_bytecode_convert_method.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
• atoi() : stdlib.c
• atol() : stdlib.c
• attempt_assign_length_from_type() : array_pool.cpp