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

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

- c -

• c2cpp() : cpp_internal_additions.cpp
• c_bit_field_replacement_type() : c_bit_field_replacement_type.cpp, c_bit_field_replacement_type.h
• c_bool_type() : c_types.cpp, c_types.h
• c_implicit_typecast() : c_typecast.cpp, c_typecast.h
• c_implicit_typecast_arithmetic() : c_typecast.cpp, c_typecast.h
• c_index_type() : c_types.cpp, c_types.h
• c_nondet_symbol_factory() : c_nondet_symbol_factory.cpp, c_nondet_symbol_factory.h
• c_preprocess() : c_preprocess.cpp, c_preprocess.h
• c_preprocess_arm() : c_preprocess.cpp
• c_preprocess_codewarrior() : c_preprocess.cpp
• c_preprocess_gcc_clang() : c_preprocess.cpp
• c_preprocess_none() : c_preprocess.cpp
• c_preprocess_visual_studio() : c_preprocess.cpp
• c_safety_checks() : c_safety_checks.cpp, c_safety_checks.h
• c_safety_checks_address_rec() : c_safety_checks.cpp
• c_safety_checks_rec() : c_safety_checks.cpp
• c_sizeof_type_rec() : symex_builtin_functions.cpp
• c_test_program : c_preprocess.cpp
• c_translation_unitt : mini_c_parser.h
• c_type_as_string() : c_types.cpp, c_types.h
• c_wrangler() : c_wrangler.cpp, c_wrangler.h
• CALL_ON_CODE : validate_code.cpp
• call_on_code() : validate_code.cpp
• CALL_ON_EXPR : validate_expressions.cpp
• call_on_expr() : validate_expressions.cpp
• CALL_ON_TYPE : validate_types.cpp
• call_on_type() : validate_types.cpp
• can_cast_expr() : expr_cast.h
• can_cast_expr< abs_exprt >() : std_expr.h
• can_cast_expr< address_of_exprt >() : pointer_expr.h
• can_cast_expr< and_exprt >() : std_expr.h
• can_cast_expr< annotated_pointer_constant_exprt >() : pointer_expr.h
• can_cast_expr< array_comprehension_exprt >() : std_expr.h
• can_cast_expr< array_exprt >() : std_expr.h
• can_cast_expr< array_list_exprt >() : std_expr.h
• can_cast_expr< array_of_exprt >() : std_expr.h
• can_cast_expr< ashr_exprt >() : bitvector_expr.h
• can_cast_expr< binary_exprt >() : std_expr.h
• can_cast_expr< binary_overflow_exprt >() : bitvector_expr.h
• can_cast_expr< binary_relation_exprt >() : std_expr.h
• can_cast_expr< binding_exprt >() : std_expr.h
• can_cast_expr< bit_cast_exprt >() : c_expr.h
• can_cast_expr< bitand_exprt >() : bitvector_expr.h
• can_cast_expr< bitnand_exprt >() : bitvector_expr.h
• can_cast_expr< bitnor_exprt >() : bitvector_expr.h
• can_cast_expr< bitnot_exprt >() : bitvector_expr.h
• can_cast_expr< bitor_exprt >() : bitvector_expr.h
• can_cast_expr< bitreverse_exprt >() : bitvector_expr.h
• can_cast_expr< bitxnor_exprt >() : bitvector_expr.h
• can_cast_expr< bitxor_exprt >() : bitvector_expr.h
• can_cast_expr< bswap_exprt >() : bitvector_expr.h
• can_cast_expr< byte_extract_exprt >() : byte_operators.h
• can_cast_expr< byte_update_exprt >() : byte_operators.h
• can_cast_expr< case_exprt >() : std_expr.h
• can_cast_expr< class_method_descriptor_exprt >() : std_expr.h
• can_cast_expr< code_asm_gcct >() : std_code.h
• can_cast_expr< code_asmt >() : std_code.h
• can_cast_expr< code_assertt >() : std_code.h
• can_cast_expr< code_assignt >() : goto_instruction_code.h
• can_cast_expr< code_assumet >() : std_code.h
• can_cast_expr< code_blockt >() : std_code.h
• can_cast_expr< code_breakt >() : std_code.h
• can_cast_expr< code_continuet >() : std_code.h
• can_cast_expr< code_deadt >() : goto_instruction_code.h
• can_cast_expr< code_declt >() : goto_instruction_code.h
• can_cast_expr< code_dowhilet >() : std_code.h
• can_cast_expr< code_expressiont >() : std_code.h
• can_cast_expr< code_fort >() : std_code.h
• can_cast_expr< code_frontend_assignt >() : std_code.h
• can_cast_expr< code_frontend_declt >() : std_code.h
• can_cast_expr< code_frontend_returnt >() : std_code.h
• can_cast_expr< code_function_callt >() : goto_instruction_code.h
• can_cast_expr< code_gcc_switch_case_ranget >() : std_code.h
• can_cast_expr< code_gotot >() : std_code.h
• can_cast_expr< code_ifthenelset >() : std_code.h
• can_cast_expr< code_inputt >() : goto_instruction_code.h
• can_cast_expr< code_labelt >() : std_code.h
• can_cast_expr< code_landingpadt >() : std_code.h
• can_cast_expr< code_outputt >() : goto_instruction_code.h
• can_cast_expr< code_pop_catcht >() : std_code.h
• can_cast_expr< code_push_catcht >() : std_code.h
• can_cast_expr< code_returnt >() : goto_instruction_code.h
• can_cast_expr< code_skipt >() : std_code.h
• can_cast_expr< code_switch_caset >() : std_code.h
• can_cast_expr< code_switcht >() : std_code.h
• can_cast_expr< code_try_catcht >() : std_code.h
• can_cast_expr< code_whilet >() : std_code.h
• can_cast_expr< codet >() : std_code_base.h
• can_cast_expr< complex_exprt >() : std_expr.h
• can_cast_expr< complex_imag_exprt >() : std_expr.h
• can_cast_expr< complex_real_exprt >() : std_expr.h
• can_cast_expr< concatenation_exprt >() : bitvector_expr.h
• can_cast_expr< cond_exprt >() : std_expr.h
• can_cast_expr< conditional_target_group_exprt >() : c_expr.h
• can_cast_expr< constant_exprt >() : std_expr.h
• can_cast_expr< count_leading_zeros_exprt >() : bitvector_expr.h
• can_cast_expr< count_trailing_zeros_exprt >() : bitvector_expr.h
• can_cast_expr< cstrlen_exprt >() : pointer_expr.h
• can_cast_expr< dereference_exprt >() : pointer_expr.h
• can_cast_expr< div_exprt >() : std_expr.h
• can_cast_expr< dynamic_object_exprt >() : pointer_expr.h
• can_cast_expr< element_address_exprt >() : pointer_expr.h
• can_cast_expr< empty_union_exprt >() : std_expr.h
• can_cast_expr< enum_is_in_range_exprt >() : c_expr.h
• can_cast_expr< equal_exprt >() : std_expr.h
• can_cast_expr< euclidean_mod_exprt >() : std_expr.h
• can_cast_expr< exists_exprt >() : mathematical_expr.h
• can_cast_expr< extractbit_exprt >() : bitvector_expr.h
• can_cast_expr< extractbits_exprt >() : bitvector_expr.h
• can_cast_expr< factorial_power_exprt >() : mathematical_expr.h
• can_cast_expr< field_address_exprt >() : pointer_expr.h
• can_cast_expr< field_sensitive_ssa_exprt >() : field_sensitivity.h
• can_cast_expr< fieldref_exprt >() : java_bytecode_parse_tree.h
• can_cast_expr< find_first_set_exprt >() : bitvector_expr.h
• can_cast_expr< floatbv_round_to_integral_exprt >() : floatbv_expr.h
• can_cast_expr< floatbv_typecast_exprt >() : floatbv_expr.h
• can_cast_expr< forall_exprt >() : mathematical_expr.h
• can_cast_expr< function_application_exprt >() : mathematical_expr.h
• can_cast_expr< greater_than_exprt >() : std_expr.h
• can_cast_expr< greater_than_or_equal_exprt >() : std_expr.h
• can_cast_expr< ieee_float_equal_exprt >() : floatbv_expr.h
• can_cast_expr< ieee_float_notequal_exprt >() : floatbv_expr.h
• can_cast_expr< ieee_float_op_exprt >() : floatbv_expr.h
• can_cast_expr< if_exprt >() : std_expr.h
• can_cast_expr< implies_exprt >() : std_expr.h
• can_cast_expr< index_designatort >() : std_expr.h
• can_cast_expr< index_exprt >() : std_expr.h
• can_cast_expr< is_cstring_exprt >() : pointer_expr.h
• can_cast_expr< is_dynamic_object_exprt >() : pointer_expr.h
• can_cast_expr< is_invalid_pointer_exprt >() : pointer_predicates.h
• can_cast_expr< isfinite_exprt >() : floatbv_expr.h
• can_cast_expr< isinf_exprt >() : floatbv_expr.h
• can_cast_expr< isnan_exprt >() : floatbv_expr.h
• can_cast_expr< isnormal_exprt >() : floatbv_expr.h
• can_cast_expr< java_instanceof_exprt >() : java_expr.h
• can_cast_expr< java_string_literal_exprt >() : java_string_literal_expr.h
• can_cast_expr< lambda_exprt >() : mathematical_expr.h
• can_cast_expr< less_than_exprt >() : std_expr.h
• can_cast_expr< less_than_or_equal_exprt >() : std_expr.h
• can_cast_expr< let_exprt >() : std_expr.h
• can_cast_expr< literal_exprt >() : literal_expr.h
• can_cast_expr< literal_vector_exprt >() : literal_vector_expr.h
• can_cast_expr< live_object_exprt >() : pointer_expr.h
• can_cast_expr< lshr_exprt >() : bitvector_expr.h
• can_cast_expr< member_designatort >() : std_expr.h
• can_cast_expr< member_exprt >() : std_expr.h
• can_cast_expr< minus_exprt >() : std_expr.h
• can_cast_expr< minus_overflow_exprt >() : bitvector_expr.h
• can_cast_expr< mod_exprt >() : std_expr.h
• can_cast_expr< mult_exprt >() : std_expr.h
• can_cast_expr< mult_overflow_exprt >() : bitvector_expr.h
• can_cast_expr< named_term_exprt >() : std_expr.h
• can_cast_expr< nil_exprt >() : std_expr.h
• can_cast_expr< nondet_padding_exprt >() : nondet_padding.h
• can_cast_expr< nondet_symbol_exprt >() : std_expr.h
• can_cast_expr< not_exprt >() : std_expr.h
• can_cast_expr< notequal_exprt >() : std_expr.h
• can_cast_expr< object_address_exprt >() : pointer_expr.h
• can_cast_expr< object_descriptor_exprt >() : pointer_expr.h
• can_cast_expr< object_size_exprt >() : pointer_expr.h
• can_cast_expr< or_exprt >() : std_expr.h
• can_cast_expr< overflow_result_exprt >() : bitvector_expr.h
• can_cast_expr< plus_exprt >() : std_expr.h
• can_cast_expr< plus_overflow_exprt >() : bitvector_expr.h
• can_cast_expr< pointer_in_range_exprt >() : pointer_expr.h
• can_cast_expr< pointer_object_exprt >() : pointer_expr.h
• can_cast_expr< pointer_offset_exprt >() : pointer_expr.h
• can_cast_expr< popcount_exprt >() : bitvector_expr.h
• can_cast_expr< power_exprt >() : mathematical_expr.h
• can_cast_expr< prophecy_pointer_in_range_exprt >() : pointer_expr.h
• can_cast_expr< prophecy_r_ok_exprt >() : pointer_expr.h
• can_cast_expr< prophecy_r_or_w_ok_exprt >() : pointer_expr.h
• can_cast_expr< prophecy_w_ok_exprt >() : pointer_expr.h
• can_cast_expr< quantifier_exprt >() : mathematical_expr.h
• can_cast_expr< r_ok_exprt >() : pointer_expr.h
• can_cast_expr< r_or_w_ok_exprt >() : pointer_expr.h
• can_cast_expr< refined_string_exprt >() : string_expr.h
• can_cast_expr< replication_exprt >() : bitvector_expr.h
• can_cast_expr< saturating_minus_exprt >() : bitvector_expr.h
• can_cast_expr< saturating_plus_exprt >() : bitvector_expr.h
• can_cast_expr< separate_exprt >() : pointer_expr.h
• can_cast_expr< shift_exprt >() : bitvector_expr.h
• can_cast_expr< shl_exprt >() : bitvector_expr.h
• can_cast_expr< shl_overflow_exprt >() : bitvector_expr.h
• can_cast_expr< shuffle_vector_exprt >() : c_expr.h
• can_cast_expr< side_effect_expr_assignt >() : std_code.h
• can_cast_expr< side_effect_expr_function_callt >() : std_code.h
• can_cast_expr< side_effect_expr_nondett >() : std_code.h
• can_cast_expr< side_effect_expr_overflowt >() : c_expr.h
• can_cast_expr< side_effect_expr_statement_expressiont >() : std_code.h
• can_cast_expr< side_effect_expr_throwt >() : std_code.h
• can_cast_expr< side_effect_exprt >() : std_code.h
• can_cast_expr< sign_exprt >() : std_expr.h
• can_cast_expr< ssa_exprt >() : ssa_expr.h
• can_cast_expr< string_constantt >() : string_constant.h
• can_cast_expr< struct_exprt >() : std_expr.h
• can_cast_expr< symbol_exprt >() : std_expr.h
• can_cast_expr< transt >() : mathematical_expr.h
• can_cast_expr< type_exprt >() : std_expr.h
• can_cast_expr< typecast_exprt >() : std_expr.h
• can_cast_expr< unary_exprt >() : std_expr.h
• can_cast_expr< unary_minus_exprt >() : std_expr.h
• can_cast_expr< unary_minus_overflow_exprt >() : bitvector_expr.h
• can_cast_expr< unary_overflow_exprt >() : bitvector_expr.h
• can_cast_expr< unary_plus_exprt >() : std_expr.h
• can_cast_expr< union_exprt >() : std_expr.h
• can_cast_expr< update_bit_exprt >() : bitvector_expr.h
• can_cast_expr< update_bits_exprt >() : bitvector_expr.h
• can_cast_expr< update_exprt >() : std_expr.h
• can_cast_expr< vector_exprt >() : std_expr.h
• can_cast_expr< w_ok_exprt >() : pointer_expr.h
• can_cast_expr< with_exprt >() : std_expr.h
• can_cast_expr< writeable_object_exprt >() : pointer_expr.h
• can_cast_expr< xnor_exprt >() : std_expr.h
• can_cast_expr< xor_exprt >() : std_expr.h
• can_cast_expr< zero_extend_exprt >() : bitvector_expr.h
• can_cast_type() : expr_cast.h
• can_cast_type< annotated_typet >() : java_types.h
• can_cast_type< array_typet >() : std_types.h
• can_cast_type< bitvector_typet >() : std_types.h
• can_cast_type< bool_typet >() : std_types.h
• can_cast_type< bv_typet >() : bitvector_types.h
• can_cast_type< c_bit_field_typet >() : c_types.h
• can_cast_type< c_bool_typet >() : c_types.h
• can_cast_type< c_enum_tag_typet >() : c_types.h
• can_cast_type< c_enum_typet >() : c_types.h
• can_cast_type< class_typet >() : std_types.h
• can_cast_type< code_typet >() : std_types.h
• can_cast_type< code_with_contract_typet >() : c_types.h
• can_cast_type< complex_typet >() : std_types.h
• can_cast_type< enumeration_typet >() : std_types.h
• can_cast_type< fixedbv_typet >() : bitvector_types.h
• can_cast_type< floatbv_typet >() : bitvector_types.h
• can_cast_type< integer_bitvector_typet >() : bitvector_types.h
• can_cast_type< java_class_typet >() : java_types.h
• can_cast_type< java_generic_parametert >() : java_types.h
• can_cast_type< java_generic_typet >() : java_types.h
• can_cast_type< java_method_typet >() : java_types.h
• can_cast_type< java_reference_typet >() : java_types.h
• can_cast_type< mathematical_function_typet >() : mathematical_types.h
• can_cast_type< pointer_typet >() : pointer_expr.h
• can_cast_type< range_typet >() : std_types.h
• can_cast_type< reference_typet >() : pointer_expr.h
• can_cast_type< signedbv_typet >() : bitvector_types.h
• can_cast_type< string_typet >() : std_types.h
• can_cast_type< struct_or_union_tag_typet >() : std_types.h
• can_cast_type< struct_tag_typet >() : std_types.h
• can_cast_type< struct_typet >() : std_types.h
• can_cast_type< struct_union_typet >() : std_types.h
• can_cast_type< tag_typet >() : std_types.h
• can_cast_type< typedef_typet >() : typedef_type.h
• can_cast_type< union_tag_typet >() : c_types.h
• can_cast_type< union_typet >() : c_types.h
• can_cast_type< unsignedbv_typet >() : bitvector_types.h
• can_cast_type< vector_typet >() : std_types.h
• can_evaluate_to_constant() : java_trace_validation.cpp, java_trace_validation.h
• cannot_be_neg() : string_constraint.cpp
• capitalize() : string_utils.cpp, string_utils.h
• car_havoc_methodt : instrument_spec_assigns.h
• cast_or_reinterpret() : expr_initializer.cpp
• CATCH : goto_program.h
• cbmc_invariants_should_throw : invariant.cpp, invariant.h
• CBMC_NORETURN : invariant.h
• CBMC_OPTIONS : cbmc_parse_options.h
• CBMC_VERSION : version.h
• cfg_dominatorst : cfg_dominators.h
• cfg_post_dominatorst : cfg_dominators.h
• change_impact() : change_impact.cpp, change_impact.h
• char16_t_type() : c_types.cpp, c_types.h
• char32_t_type() : c_types.cpp, c_types.h
• char_type() : c_types.cpp, c_types.h
• character_equals_ignore_case() : string_constraint_generator_comparison.cpp
• CHARACTER_FOR_UNKNOWN : string_builtin_function.h
• check_address_structure() : java_trace_validation.cpp, java_trace_validation.h
• check_and_replace_target() : replace_java_nondet.cpp
• check_annotated_pointer_constant_structure() : java_trace_validation.cpp
• check_assertion() : static_verifier.cpp
• check_axioms() : string_refinement.cpp
• check_c_implicit_typecast() : c_typecast.cpp, c_typecast.h
• check_call_sequence() : call_sequences.cpp, call_sequences.h
• check_code() : validate_code.cpp, validate_code.h
• check_constant_structure() : java_trace_validation.cpp, java_trace_validation.h
• check_expr() : validate_expressions.cpp, validate_expressions.h
• check_has_contract_rec() : dfcc_cfg_info.cpp
• check_index_structure() : java_trace_validation.cpp, java_trace_validation.h
• check_inner_loops_have_contracts() : dfcc_cfg_info.cpp
• check_lhs_assumptions() : java_trace_validation.cpp
• check_member_structure() : java_trace_validation.cpp, java_trace_validation.h
• check_one_of_options() : variable_sensitivity_configuration.cpp
• check_renaming() : renaming_level.cpp, renaming_level.h
• check_renaming_l1() : renaming_level.cpp, renaming_level.h
• CHECK_RETURN : invariant.h
• CHECK_RETURN_STRUCTURED : invariant.h
• CHECK_RETURN_WITH_DIAGNOSTICS : invariant.h
• CHECK_RETURN_WITH_IREP : invariant_utils.h
• check_rhs_assumptions() : java_trace_validation.cpp
• check_step_assumptions() : java_trace_validation.cpp
• check_struct_structure() : java_trace_validation.cpp, java_trace_validation.h
• check_symbol_structure() : java_trace_validation.cpp, java_trace_validation.h
• check_trace_assumptions() : java_trace_validation.cpp, java_trace_validation.h
• check_type() : validate_types.cpp, validate_types.h
• check_value_set_contains_only_null_ptr() : shadow_memory_util.cpp, shadow_memory_util.h
• checked_dereference() : java_utils.cpp, java_utils.h
• child_pid : signal_catcher.cpp
• clang_builtin_headers : ansi_c_internal_additions.cpp, ansi_c_internal_additions.h
• class_name_from_method_name() : java_utils.cpp, java_utils.h
• class_to_declared_symbols() : java_static_initializers.cpp, java_static_initializers.h
• clean_deref() : java_pointer_casts.cpp
• clean_identifier() : expr2c.cpp, dump_c.cpp
• clean_pointer_expr() : shadow_memory_util.cpp, shadow_memory_util.h
• clean_string_constant() : shadow_memory_util.cpp
• cleanup_module() : driver.h
• cleanup_var_table() : java_local_variable_table.cpp
• clinit_already_run_variable_name() : java_static_initializers.cpp
• clinit_function_name() : java_static_initializers.cpp
• clinit_function_suffix : java_static_initializers.cpp
• clinit_local_init_complete_var_name() : java_static_initializers.cpp
• clinit_state_var_name() : java_static_initializers.cpp
• clinit_states_type() : java_static_initializers.cpp
• clinit_statest : java_static_initializers.cpp
• clinit_thread_local_state_var_name() : java_static_initializers.cpp
• clinit_wrapper_do_recursive_calls() : java_static_initializers.cpp
• clinit_wrapper_name() : java_static_initializers.cpp, java_static_initializers.h
• clinit_wrapper_suffix : java_static_initializers.cpp
• CLONE : abstract_object.h
• clone_and_rename_function() : dfcc_utils.cpp
• clone_parameters() : dfcc_utils.cpp
• CNF_DUMP_BLOCK_SIZE : magic.h
• code_assign_function_application() : java_string_library_preprocess.cpp
• codepoint_hex_to_utf16_native_endian() : unicode.cpp, unicode.h
• codepoint_hex_to_utf8() : unicode.cpp, unicode.h
• collapse_overlapping_intervals() : value_set_abstract_object.cpp
• collapse_values_in_intervals() : value_set_abstract_object.cpp
• collect_comma_expression() : cpp_typecheck_expr.cpp
• collect_conditions() : cover_util.cpp, cover_util.h
• collect_conditions_rec() : cover_util.cpp, cover_util.h
• collect_decisions() : cover_util.cpp, cover_util.h
• collect_decisions_rec() : cover_util.cpp, cover_util.h
• collect_deref_expr() : mm_io.cpp
• collect_eloc() : count_eloc.cpp
• collect_error_messages() : smt_response_validation.cpp
• collect_error_messages_impl() : smt_response_validation.cpp
• collect_intervals() : value_set_abstract_object.cpp
• collect_mcdc_controlling() : cover_instrument_mcdc.cpp
• collect_mcdc_controlling_nested() : cover_instrument_mcdc.cpp
• collect_mcdc_controlling_rec() : cover_instrument_mcdc.cpp
• collect_open_variables() : slice.cpp, slice.h
• collect_operands() : cover_util.cpp, cover_util.h
• collect_virtual_function_callees() : remove_virtual_functions.cpp, remove_virtual_functions.h
• colour_map : event_graph.cpp
• combine_condition_and_max_values() : shadow_memory_util.cpp
• combine_in_and_post_invariant_clauses() : synthesizer_utils.cpp, synthesizer_utils.h
• COMMAND_ID : smt_commands.cpp, smt_commands.h
• comment() : race_check.cpp
• COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT : common_harness_generator_options.h
• COMMON_HARNESS_GENERATOR_HAVOC_MEMBER_OPT : common_harness_generator_options.h
• COMMON_HARNESS_GENERATOR_HELP : common_harness_generator_options.h
• COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT : common_harness_generator_options.h
• COMMON_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT : common_harness_generator_options.h
• COMMON_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT : common_harness_generator_options.h
• COMMON_HARNESS_GENERATOR_MIN_NULL_TREE_DEPTH_OPT : common_harness_generator_options.h
• COMMON_HARNESS_GENERATOR_OPTIONS : common_harness_generator_options.h
• COMPACT_CARRY : bv_utils.cpp
• COMPACT_ITE : cnf.cpp
• COMPACT_LT_OR_LE : bv_utils.cpp
• COMPACT_OBJECT_SIZE_EQ : bv_pointers.cpp
• compact_values() : value_set_abstract_object.cpp
• compare_to_collection() : shadow_memory_util.cpp
• compiler_name() : gcc_mode.cpp
• complex_member() : remove_complex.cpp
• complexity_violationt : complexity_violation.h
• component() : std_expr.cpp
• compute_address_taken_functions() : compute_called_functions.cpp, compute_called_functions.h
• compute_called_functions() : compute_called_functions.cpp, compute_called_functions.h
• compute_called_functions_from_ai() : unreachable_instructions.cpp
• compute_functions() : compute_called_functions.cpp
• compute_innermost_loop_ids() : sese_regions.cpp
• compute_max_over_bytes() : shadow_memory_util.cpp, shadow_memory_util.h
• compute_or_over_bytes() : shadow_memory_util.cpp, shadow_memory_util.h
• compute_pointer_offset() : pointer_offset_size.cpp, pointer_offset_size.h
• concurrency() : concurrency.cpp, concurrency.h
• conditional_array_cast() : java_bytecode_convert_method.cpp
• conditional_cast_floatbv_to_unsignedbv() : shadow_memory_util.cpp
• cone_of_influence() : cone_of_influence.h
• config : api.cpp, config.cpp, config.h
• configure_gcc() : gcc_version.cpp, gcc_version.h
• conjunction() : std_expr.cpp, std_expr.h
• const_literal() : literal.h
• CONSTANT : variable_sensitivity_configuration.h
• constant_bool() : java_entry_point.cpp
• CONSTANT_Class : java_bytecode_parser.cpp
• CONSTANT_Double : java_bytecode_parser.cpp
• CONSTANT_Fieldref : java_bytecode_parser.cpp
• CONSTANT_Float : java_bytecode_parser.cpp
• constant_float() : string_constraint_generator_float.cpp
• CONSTANT_Integer : java_bytecode_parser.cpp
• CONSTANT_InterfaceMethodref : java_bytecode_parser.cpp
• CONSTANT_InvokeDynamic : java_bytecode_parser.cpp
• CONSTANT_Long : java_bytecode_parser.cpp
• CONSTANT_MethodHandle : java_bytecode_parser.cpp
• CONSTANT_Methodref : java_bytecode_parser.cpp
• CONSTANT_MethodType : java_bytecode_parser.cpp
• CONSTANT_NameAndType : java_bytecode_parser.cpp
• CONSTANT_String : java_bytecode_parser.cpp
• CONSTANT_Utf8 : java_bytecode_parser.cpp
• constants_expression_transform() : abstract_value_object.cpp
• construct_terminals() : enumerative_loop_contracts_synthesizer.cpp
• construct_value_expr_from_smt() : construct_value_expr_from_smt.cpp, construct_value_expr_from_smt.h
• constructor_of() : constructor_of.h
• constructor_symbol() : lambda_synthesis.cpp
• contains() : string_constraint_instantiation.cpp
• contains_instanceof() : remove_instanceof.cpp
• contains_null_or_invalid() : shadow_memory_util.cpp, shadow_memory_util.h
• contains_symbol_prefix() : graphml_witness.cpp, cegis_verifier.cpp
• CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK : instrument_spec_assigns.cpp
• CONTRACTS_PREFIX : dfcc_library.cpp
• convert() : builtin_factory.cpp, json_goto_trace.h, xml_goto_trace.cpp, xml_goto_trace.h, satcheck_glucose.cpp, satcheck_minisat.cpp, satcheck_minisat2.cpp, xml_irep.cpp, xml_irep.h
• convert_annotations() : java_bytecode_convert_class.cpp, java_bytecode_convert_class.h
• convert_array_update_to_smt() : convert_expr_to_smt.cpp
• convert_assert() : json_goto_trace.cpp, json_goto_trace.h
• convert_assumptions() : satcheck_glucose.cpp, satcheck_minisat2.cpp
• convert_bit_vector_cast() : convert_expr_to_smt.cpp
• convert_bool_literal() : convert_bool_literal.cpp, convert_bool_literal.h
• convert_c_bool_cast() : convert_expr_to_smt.cpp
• convert_character_literal() : convert_character_literal.cpp, convert_character_literal.h
• convert_decl() : json_goto_trace.cpp, json_goto_trace.h
• convert_default() : json_goto_trace.cpp, json_goto_trace.h
• convert_dint_bit_literal_value() : convert_dint_literal.cpp, convert_dint_literal.h
• convert_dint_dec_literal_value() : convert_dint_literal.cpp, convert_dint_literal.h
• convert_dint_hex_literal_value() : convert_dint_literal.cpp, convert_dint_literal.h
• convert_dint_literal_value() : convert_dint_literal.cpp
• convert_expr_to_smt() : convert_expr_to_smt.cpp, convert_expr_to_smt.h
• convert_float_literal() : convert_float_literal.cpp, convert_float_literal.h
• convert_identifier() : convert_string_value.cpp, convert_string_value.h
• convert_input() : json_goto_trace.cpp, json_goto_trace.h
• convert_int_bit_literal() : convert_int_literal.cpp, convert_int_literal.h
• convert_int_bit_literal_value() : convert_int_literal.cpp, convert_int_literal.h
• convert_int_dec_literal() : convert_int_literal.cpp, convert_int_literal.h
• convert_int_dec_literal_value() : convert_int_literal.cpp, convert_int_literal.h
• convert_int_hex_literal() : convert_int_literal.cpp, convert_int_literal.h
• convert_int_hex_literal_value() : convert_int_literal.cpp, convert_int_literal.h
• convert_integer_literal() : convert_integer_literal.cpp, convert_integer_literal.h
• convert_java_annotations() : java_bytecode_convert_class.cpp, java_bytecode_convert_class.h
• convert_label() : convert_string_value.cpp, convert_string_value.h
• convert_line() : file_converter.cpp, converter.cpp
• convert_member_name_to_enum_value() : c_types_util.h
• convert_member_union() : boolbv_member.cpp
• convert_multiary_operator_to_terms() : convert_expr_to_smt.cpp
• convert_nondet() : convert_java_nondet.cpp, convert_java_nondet.h
• convert_one_string_literal() : convert_string_literal.cpp
• convert_output() : json_goto_trace.cpp, json_goto_trace.h
• convert_properties_json() : show_properties.cpp, show_properties.h
• convert_real_literal() : convert_real_literal.cpp, convert_real_literal.h
• convert_relational_to_smt() : convert_expr_to_smt.cpp
• convert_return() : json_goto_trace.cpp, json_goto_trace.h
• convert_statement_expression() : goto_clean_expr.cpp
• convert_string_literal() : convert_string_literal.cpp, convert_string_literal.h
• convert_symex_target_equation() : bmc_util.cpp, bmc_util.h
• convert_synchronized_methods() : java_bytecode_concurrency_instrumentation.cpp, java_bytecode_concurrency_instrumentation.h
• convert_threadblock() : java_bytecode_concurrency_instrumentation.cpp, java_bytecode_concurrency_instrumentation.h
• convert_title() : convert_string_value.cpp, convert_string_value.h
• convert_to_smt_shift() : convert_expr_to_smt.cpp
• convert_type_to_smt_sort() : convert_expr_to_smt.cpp, convert_expr_to_smt.h
• convert_version() : convert_string_value.cpp, convert_string_value.h
• copy_array() : cpp_typecheck_constructor.cpp
• copy_member() : cpp_typecheck_constructor.cpp
• copy_on_write_pointeet< Num >::unshareable : cow.h
• copy_parameter_identifiers() : read_bin_goto_object.cpp
• copy_parent() : cpp_typecheck_constructor.cpp
• count_eloc() : count_eloc.cpp, count_eloc.h
• count_expr_typed() : show_program.cpp
• count_frame() : inductiveness.cpp
• count_globals() : abstract_environment.cpp
• count_properties() : properties.cpp, properties.h
• count_trailing_bit_width() : struct_encoding.cpp
• counterexample() : counterexample_found.cpp
• counterexample_found() : counterexample_found.cpp, counterexample_found.h
• cover_instrument_end_of_function() : cover_instrument.h, cover_instrument_other.cpp
• coverage_criteriont : cover.h
• cpp_convert_auto() : cpp_convert_type.cpp, cpp_convert_type.h
• cpp_convert_plain_type() : cpp_convert_type.cpp, cpp_convert_type.h
• cpp_exception_id() : cpp_exception_id.cpp, cpp_exception_id.h
• cpp_exception_list() : cpp_exception_id.cpp, cpp_exception_id.h
• cpp_exception_list_rec() : cpp_exception_id.cpp
• cpp_expr2name() : cpp_type2name.cpp, cpp_type2name.h
• cpp_internal_additions() : cpp_internal_additions.cpp, cpp_internal_additions.h
• cpp_parse() : cpp_parser.cpp, parse.cpp
• cpp_symbol_expr() : cpp_util.cpp, cpp_util.h
• cpp_type2name() : cpp_type2name.cpp, cpp_type2name.h
• cpp_typecheck() : cpp_typecheck.cpp, cpp_typecheck.h
• CPROVER_ASSERT : statement_list_typecheck.cpp
• CPROVER_ASSUME : statement_list_typecheck.cpp
• cprover_builtin_headers : ansi_c_internal_additions.cpp, ansi_c_internal_additions.h
• cprover_c_library_factory() : cprover_library.cpp, cprover_library.h
• cprover_c_library_factory_force_load() : cprover_library.cpp, cprover_library.h
• cprover_cpp_library_factory() : cprover_library.cpp, cprover_library.h
• CPROVER_EXIT_CONVERSION_FAILED : exit_codes.h
• CPROVER_EXIT_EXCEPTION : exit_codes.h
• CPROVER_EXIT_INCORRECT_TASK : exit_codes.h
• CPROVER_EXIT_INTERNAL_ERROR : exit_codes.h
• CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY : exit_codes.h
• CPROVER_EXIT_PARSE_ERROR : exit_codes.h
• CPROVER_EXIT_PREPROCESSOR_TEST_FAILED : exit_codes.h
• CPROVER_EXIT_SET_PROPERTIES_FAILED : exit_codes.h
• CPROVER_EXIT_SUCCESS : exit_codes.h
• CPROVER_EXIT_USAGE_ERROR : exit_codes.h
• CPROVER_EXIT_VERIFICATION_INCONCLUSIVE : exit_codes.h
• CPROVER_EXIT_VERIFICATION_SAFE : exit_codes.h
• CPROVER_EXIT_VERIFICATION_UNSAFE : exit_codes.h
• CPROVER_FAT_CIGAM : osx_fat_reader.cpp
• CPROVER_FAT_MAGIC : osx_fat_reader.cpp
• CPROVER_FKT_PREFIX : cprover_prefix.h
• CPROVER_HIDE : statement_list_entry_point.cpp
• cprover_methods_to_ignore : java_utils.cpp, java_utils.h
• CPROVER_MH_CIGAM : osx_fat_reader.cpp
• CPROVER_MH_CIGAM_64 : osx_fat_reader.cpp
• CPROVER_MH_MAGIC : osx_fat_reader.cpp
• CPROVER_MH_MAGIC_64 : osx_fat_reader.cpp
• CPROVER_OPTIONS : cprover_parse_options.h
• CPROVER_PREFIX : cprover_prefix.h
• CPROVER_TEMP_RLO : statement_list_typecheck.cpp
• create_abstract_object() : variable_sensitivity_object_factory.cpp
• create_addr_of_contract_write_set() : dfcc_wrapper_program.cpp
• create_addr_of_ensures_write_set() : dfcc_wrapper_program.cpp
• create_addr_of_ptr_pred_ctx() : dfcc_wrapper_program.cpp
• create_addr_of_requires_write_set() : dfcc_wrapper_program.cpp
• create_and_declare_local() : lambda_synthesis.cpp
• create_array_with_type_body() : create_array_with_type_intrinsic.cpp, create_array_with_type_intrinsic.h
• create_assignable_builtin_names() : dfcc_library.cpp
• create_clinit_wrapper_function_symbol() : java_static_initializers.cpp
• create_clinit_wrapper_symbols() : java_static_initializers.cpp
• create_context_abstract_object() : variable_sensitivity_object_factory.cpp
• create_contract_write_set() : dfcc_wrapper_program.cpp
• create_data_block_parameter() : statement_list_typecheck.cpp
• create_dfcc_fun_to_name() : dfcc_library.cpp
• create_dfcc_hook() : dfcc_library.cpp
• create_dfcc_type_to_name() : dfcc_library.cpp
• create_ensures_write_set() : dfcc_wrapper_program.cpp
• create_fatal_assertion() : std_code.cpp, std_code.h
• create_fresh_symbol() : instrument_spec_assigns.cpp
• create_function_symbol() : java_static_initializers.cpp
• create_havoc_hook() : dfcc_library.cpp
• create_invokedynamic_synthetic_classes() : lambda_synthesis.cpp, lambda_synthesis.h
• create_java_initialize() : java_entry_point.cpp, java_entry_point.h
• create_max_expr() : shadow_memory_util.cpp
• create_method_stub_symbol() : java_bytecode_convert_method.cpp, java_bytecode_convert_method.h
• create_parameter_names() : java_bytecode_convert_method.cpp, java_bytecode_convert_method.h
• create_parameter_symbols() : java_bytecode_convert_method.cpp, java_bytecode_convert_method.h
• create_ptr_pred_ctx() : dfcc_wrapper_program.cpp
• create_requires_write_set() : dfcc_wrapper_program.cpp
• create_static_function_call() : remove_virtual_functions.cpp
• create_static_initializer_symbols() : java_static_initializers.cpp, java_static_initializers.h
• create_stub_global_initializers() : java_static_initializers.h
• create_stub_global_symbol() : java_bytecode_language.cpp
• create_stub_global_symbols() : java_bytecode_language.cpp
• create_user_specified_clinit_function_symbol() : java_static_initializers.cpp
• create_void_function_symbol() : call_graph_test_utils.cpp, call_graph_test_utils.h
• cscanner_ptr : cscanner.cpp, cscanner.h
• cubes() : miniBDD.cpp, miniBDD.h
• CURRENT_FUNCTION_NAME : invariant.h
• cw_builtin_headers : ansi_c_internal_additions.cpp, ansi_c_internal_additions.h