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

_

- i -

• id2boolean() : c_types_util.h
• id2string() : irep.h
• implemented_method_symbol() : lambda_synthesis.cpp
• implication() : goto_check_c.cpp
• implicit() : full_slicer.cpp
• indent_str() : irep.cpp
• index_array_size() : c_safety_checks.cpp
• inductiveness_check() : inductiveness.cpp, inductiveness.h
• infer_loop_assigns() : utils.cpp, utils.h
• infer_opaque_type_fields() : java_bytecode_language.cpp
• init_function_symbols() : dfcc_is_cprover_symbol.cpp
• init_module() : driver.h
• init_static_symbols() : dfcc_is_cprover_symbol.cpp
• init_symbol() : java_entry_point.cpp
• initial_index_set() : string_refinement.cpp
• initial_smt_object_map() : object_tracking.cpp, object_tracking.h
• initialize_abstract_object() : variable_sensitivity_object_factory.cpp
• initialize_from_source_files() : initialize_goto_model.cpp, initialize_goto_model.h
• initialize_goto_model() : initialize_goto_model.cpp, initialize_goto_model.h
• initialize_nondet_string_fields() : java_object_factory.cpp
• initialize_properties() : properties.cpp, properties.h
• initialize_ssa_identifier() : ssa_expr.cpp
• initialize_yyc_scanner() : cscanner.cpp
• inline_function() : dfcc_utils.cpp
• insert_before_and_update_jumps() : utils.cpp, utils.h
• insert_before_swap_and_advance() : utils.cpp, utils.h
• insert_final_assert_false() : insert_final_assert_false.cpp, insert_final_assert_false.h
• insert_nondet_init_code() : convert_java_nondet.cpp
• install_signal_catcher() : signal_catcher.cpp, signal_catcher.h
• instantiate() : string_constraint_instantiation.cpp, string_constraint_instantiation.h, string_refinement.cpp
• instantiate_atomic_compare_exchange() : c_typecheck_gcc_polymorphic_builtins.cpp
• instantiate_atomic_compare_exchange_n() : c_typecheck_gcc_polymorphic_builtins.cpp
• instantiate_atomic_exchange() : c_typecheck_gcc_polymorphic_builtins.cpp
• instantiate_atomic_exchange_n() : c_typecheck_gcc_polymorphic_builtins.cpp
• instantiate_atomic_fetch_op() : c_typecheck_gcc_polymorphic_builtins.cpp
• instantiate_atomic_load() : c_typecheck_gcc_polymorphic_builtins.cpp
• instantiate_atomic_load_n() : c_typecheck_gcc_polymorphic_builtins.cpp
• instantiate_atomic_op_fetch() : c_typecheck_gcc_polymorphic_builtins.cpp
• instantiate_atomic_store() : c_typecheck_gcc_polymorphic_builtins.cpp
• instantiate_atomic_store_n() : c_typecheck_gcc_polymorphic_builtins.cpp
• instantiate_byte_array() : lower_byte_operators.cpp
• instantiate_contract_lambda() : instrument_contracts.cpp
• instantiate_new_object() : lambda_synthesis.cpp
• instantiate_not_contains() : string_constraint_instantiation.h
• instantiate_sync_bool_compare_and_swap() : c_typecheck_gcc_polymorphic_builtins.cpp
• instantiate_sync_fetch() : c_typecheck_gcc_polymorphic_builtins.cpp
• instantiate_sync_lock_release() : c_typecheck_gcc_polymorphic_builtins.cpp
• instantiate_sync_lock_test_and_set() : c_typecheck_gcc_polymorphic_builtins.cpp
• instantiate_sync_val_compare_and_swap() : c_typecheck_gcc_polymorphic_builtins.cpp
• instruction_from_json() : json_goto_function.cpp
• instruction_ordinals() : sese_regions.cpp
• instrument_contract_checks() : instrument_contracts.cpp
• instrument_contracts() : instrument_contracts.cpp, instrument_contracts.h
• instrument_cover_goals() : cover.cpp, cover.h
• instrument_end_thread() : java_bytecode_concurrency_instrumentation.cpp
• instrument_equal_operands() : expr2statement_list.cpp
• instrument_get_current_thread_id() : java_bytecode_concurrency_instrumentation.cpp
• instrument_get_monitor_count() : java_bytecode_concurrency_instrumentation.cpp
• instrument_given_invariants() : instrument_given_invariants.cpp, instrument_given_invariants.h
• instrument_intervals() : interval_analysis.cpp
• instrument_preconditions() : instrument_preconditions.cpp, instrument_preconditions.h
• instrument_start_thread() : java_bytecode_concurrency_instrumentation.cpp
• instrument_synchronized_code() : java_bytecode_concurrency_instrumentation.cpp
• int_of_hex_char() : string_constraint_generator_valueof.cpp
• integer2binary() : mp_arith.cpp, mp_arith.h
• integer2bvrep() : arith_tools.cpp, arith_tools.h
• integer2string() : mp_arith.cpp, mp_arith.h
• integer_address() : pointer_predicates.cpp, pointer_predicates.h
• integer_interval_to_string() : java_object_factory.cpp
• interpreter() : interpreter.cpp, interpreter.h
• interrupt() : interrupt.cpp, interrupt.h
• interrupt_solver() : satcheck_minisat2.cpp
• intersection() : graph.h
• interval_analysis() : interval_analysis.cpp, interval_analysis.h
• interval_constraint() : interval_constraint.cpp, interval_constraint.h
• interval_from_relation() : interval_abstract_value.cpp
• interval_from_x_ge_value() : interval_abstract_value.cpp
• interval_from_x_gt_value() : interval_abstract_value.cpp
• interval_from_x_le_value() : interval_abstract_value.cpp
• interval_from_x_lt_value() : interval_abstract_value.cpp
• intervals_expression_transform() : abstract_value_object.cpp
• introduce_temporaries() : weak_memory.cpp, weak_memory.h
• invalid_argument() : variable_sensitivity_configuration.cpp
• invariant_failure_containing() : invariant.cpp, invariant.h
• invariant_violated_string() : invariant.h
• invariant_violated_structured() : invariant.h
• inverse() : rational.cpp, rational.h
• invert_expr() : abstract_environment.cpp
• invert_relation() : interval_abstract_value.cpp
• invert_result() : abstract_environment.cpp
• invokedynamic_synthetic_constructor() : lambda_synthesis.cpp, lambda_synthesis.h
• invokedynamic_synthetic_method() : lambda_synthesis.cpp, lambda_synthesis.h
• irep2lisp() : lispirep.cpp, lispirep.h
• irep2name() : cpp_type2name.cpp
• is_a_bv_type() : value_set_dereference.cpp
• is_a_char_type() : simplify_state_expr.cpp
• is_access_expr() : abstract_environment.cpp
• is_assignable() : expr_util.cpp, expr_util.h
• is_assigned() : dfcc_cfg_info.cpp
• is_assignment_from() : replace_java_nondet.cpp
• is_assignment_to_instrumented_variable() : utils.cpp, utils.h
• is_assigns_clause_replacement_tracking_comment() : utils.cpp, utils.h
• is_associative_and_commutative_for_type() : simplify_utils.cpp
• is_bitvector() : util.cpp, util.h
• is_c_bool_type() : c_types_util.h
• is_c_char_pointer_type() : c_types_util.h
• is_c_char_type() : c_types_util.h
• is_c_enum_type() : c_types_util.h
• is_c_integral_pointer_type() : c_types_util.h
• is_c_integral_type() : c_types_util.h
• is_char_array_type() : string_refinement_util.cpp, string_refinement_util.h
• is_char_pointer_type() : string_refinement_util.cpp, string_refinement_util.h
• is_char_type() : string_refinement_util.cpp, string_refinement_util.h
• is_clinit_function() : java_static_initializers.cpp, java_static_initializers.h
• is_clinit_wrapper_function() : java_static_initializers.cpp, java_static_initializers.h
• is_comment() : ctoken.h
• is_condition() : cover_util.cpp, cover_util.h
• is_constant() : std_types.h
• is_constant_or_has_constant_components() : std_types.cpp, std_types.h
• is_constructor() : java_bytecode_convert_method.cpp
• is_core_memory_predicate() : dfcc_lift_memory_predicates.cpp
• is_dereference() : abstract_pointer_object.cpp
• is_dereference_integer_object() : simplify_expr_pointer.cpp
• is_digit_with_radix() : string_constraint_generator.h, string_constraint_generator_valueof.cpp
• is_dot_i_file() : c_preprocess.cpp
• is_dynamic() : object_tracking.cpp
• is_dynamic_allocation() : abstract_environment.cpp
• is_empty() : goto_convert.cpp, document_properties.cpp
• is_enum_with_type_equal_to_declaring_type() : assignments_from_json.cpp
• is_eof() : ctoken.h
• is_eq() : value_set_abstract_object.cpp
• is_failed_assertion_step() : build_goto_trace.cpp
• is_failed_symbol() : add_failed_symbols.h
• is_false() : literal.h
• is_fence() : fence.cpp, fence.h
• is_function_built_in_or_extern() : graphml_witness.cpp
• is_goto_binary() : read_goto_binary.cpp, read_goto_binary.h
• is_high_surrogate() : string_constraint_generator_code_points.cpp
• is_identifier() : parse.cpp, ctoken.h
• is_index_member_symbol() : goto_trace.cpp
• is_instantiation_of_flexible_array() : c_typecheck_base.cpp
• is_java_array_tag() : java_types.cpp, java_types.h
• is_java_array_type() : java_types.cpp, java_types.h
• is_java_generic_class_type() : java_types.h
• is_java_generic_parameter() : java_types.h
• is_java_generic_parameter_tag() : java_types.h
• is_java_generic_struct_tag_type() : java_types.h
• is_java_generic_type() : java_types.h
• is_java_implicitly_generic_class_type() : java_types.h
• is_java_main() : java_entry_point.cpp
• is_java_string_literal_id() : java_utils.cpp, java_utils.h
• is_java_string_type() : java_utils.cpp, java_utils.h
• is_le() : value_set_abstract_object.cpp
• is_loop_free() : utils.cpp, utils.h
• is_low_surrogate() : string_constraint_generator_code_points.cpp
• is_lower_case() : string_builtin_function.cpp
• is_lt() : value_set_abstract_object.cpp
• is_lwfence() : fence.cpp, fence.h
• is_main_symbol_invalid() : statement_list_entry_point.cpp
• is_mcdc_pair() : cover_instrument_mcdc.cpp
• is_multidim_java_array_type() : java_types.cpp, java_types.h
• is_multiplication_by_constant() : pointer_offset_size.cpp
• is_non_null_library_global() : java_utils.cpp, java_utils.h
• is_nondet_initializable_static() : nondet_static.cpp, nondet_static.h
• is_nondet_pointer() : convert_java_nondet.cpp
• is_nondet_returning_object() : replace_java_nondet.cpp
• is_not_bool() : expr2statement_list.cpp
• is_not_zero() : expr_util.cpp, expr_util.h
• is_null() : string_format_builtin_function.cpp
• is_number() : mathematical_types.cpp, mathematical_types.h
• is_object_creation() : abstract_environment.cpp
• is_object_field_element() : may_alias.cpp, may_alias.h
• is_old() : instrument_contracts.cpp
• is_operator() : ctoken.h
• is_osx_fat_header() : osx_fat_reader.cpp, osx_fat_reader.h
• is_osx_mach_object() : osx_fat_reader.cpp, osx_fat_reader.h
• is_overlay_class() : java_class_loader.cpp
• is_param_expr() : dfcc_lift_memory_predicates.cpp
• is_pointer_addition() : abstract_object.cpp
• is_pointer_subtraction() : bv_pointers_wide.cpp, bv_pointers.cpp
• is_positive() : string_constraint_generator.h, string_constraint_generator_main.cpp
• is_preprocessor_directive() : ctoken.h
• is_primitive_wrapper_type_id() : java_utils.cpp, java_utils.h
• is_primitive_wrapper_type_name() : java_utils.cpp, java_utils.h
• is_procedure_local() : instrument_contracts.cpp
• is_property_less_than() : report_util.cpp
• is_property_to_check() : properties.cpp, properties.h
• is_ptr_argument() : string_abstraction.cpp
• is_ptr_comparison() : abstract_environment.cpp, abstract_environment.h
• is_ptr_diff() : abstract_environment.cpp, abstract_environment.h
• is_reference() : pointer_expr.h, std_types.cpp, assignments_from_json.cpp
• is_refined_string_type() : refined_string_type.h
• is_return_value_identifier() : remove_returns.cpp, remove_returns.h
• is_return_value_symbol() : remove_returns.cpp, remove_returns.h
• is_return_with_variable() : replace_java_nondet.cpp
• is_rvalue_reference() : pointer_expr.h, std_types.cpp
• is_separator() : ctoken.h
• is_set_extreme() : value_set_abstract_object.cpp
• is_shared() : race_check.cpp
• is_signed() : util.cpp
• is_signed_or_unsigned_bitvector() : bitvector_types.h
• is_size_one() : goto_convert.cpp
• is_skip() : remove_skip.cpp, remove_skip.h
• is_smt2_simple_identifier() : smt2_conv.cpp
• is_smt2_simple_symbol_character() : smt2_tokenizer.cpp, smt2_tokenizer.h
• is_space() : jar_file.cpp
• is_ssa_expr() : ssa_expr.h
• is_store_to_slot() : java_local_variable_table.cpp
• is_string_constant_initialization() : symex_assign.cpp
• is_subsumed() : inductiveness.cpp
• is_symbol_member() : instrument_contracts.cpp
• is_symbol_with_id() : replace_java_nondet.cpp
• is_transformed_loop_end() : utils.cpp, utils.h
• is_transformed_loop_head() : utils.cpp, utils.h
• is_true() : literal.h
• is_typecast_from_void_ptr() : abstract_pointer_object.cpp
• is_typecast_with_id() : replace_java_nondet.cpp
• is_unsigned() : util.cpp
• is_upper_case() : string_builtin_function.cpp
• is_user_specified_clinit_function() : java_static_initializers.cpp, java_static_initializers.h
• is_valid_java_array() : java_types.cpp, java_types.h
• is_valid_path_strategy() : path_storage.cpp, path_storage.h
• is_valid_smt_identifier() : smt_terms.cpp
• is_valid_string_constraint() : string_refinement.cpp
• is_value() : abstract_environment.cpp
• is_void_pointer() : pointer_expr.h
• is_ws() : ctoken.h
• is_zero_char() : simplify_state_expr.cpp
• is_zero_string() : string_instrumentation.cpp, string_instrumentation.h
• is_zero_width() : smt2_conv.cpp