- 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_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_sizeof_type_rec()
: symex_builtin_functions.cpp
- c_type_as_string()
: c_types.cpp
, c_types.h
- call_on_code()
: validate_code.cpp
- call_on_expr()
: validate_expressions.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 >()
: std_expr.h
- can_cast_expr< and_exprt >()
: std_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< binary_exprt >()
: std_expr.h
- can_cast_expr< binary_relation_exprt >()
: std_expr.h
- can_cast_expr< bitand_exprt >()
: std_expr.h
- can_cast_expr< bitnot_exprt >()
: std_expr.h
- can_cast_expr< bitor_exprt >()
: std_expr.h
- can_cast_expr< bitxor_exprt >()
: std_expr.h
- can_cast_expr< bswap_exprt >()
: std_expr.h
- can_cast_expr< byte_extract_exprt >()
: byte_operators.h
- can_cast_expr< byte_update_exprt >()
: byte_operators.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 >()
: std_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 >()
: std_code.h
- can_cast_expr< code_declt >()
: std_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_function_callt >()
: std_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 >()
: std_code.h
- can_cast_expr< code_labelt >()
: std_code.h
- can_cast_expr< code_landingpadt >()
: std_code.h
- can_cast_expr< code_outputt >()
: std_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 >()
: std_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.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 >()
: std_expr.h
- can_cast_expr< cond_exprt >()
: std_expr.h
- can_cast_expr< constant_exprt >()
: std_expr.h
- can_cast_expr< dereference_exprt >()
: std_expr.h
- can_cast_expr< div_exprt >()
: std_expr.h
- can_cast_expr< dynamic_object_exprt >()
: std_expr.h
- can_cast_expr< equal_exprt >()
: std_expr.h
- can_cast_expr< extractbit_exprt >()
: std_expr.h
- can_cast_expr< extractbits_exprt >()
: std_expr.h
- can_cast_expr< factorial_power_exprt >()
: mathematical_expr.h
- can_cast_expr< fieldref_exprt >()
: java_bytecode_parse_tree.h
- can_cast_expr< floatbv_typecast_exprt >()
: std_expr.h
- can_cast_expr< function_application_exprt >()
: mathematical_expr.h
- can_cast_expr< goto_trace_constant_pointer_exprt >()
: goto_trace.h
- can_cast_expr< ieee_float_equal_exprt >()
: std_expr.h
- can_cast_expr< ieee_float_notequal_exprt >()
: std_expr.h
- can_cast_expr< ieee_float_op_exprt >()
: std_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< isfinite_exprt >()
: std_expr.h
- can_cast_expr< isinf_exprt >()
: std_expr.h
- can_cast_expr< isnan_exprt >()
: std_expr.h
- can_cast_expr< isnormal_exprt >()
: std_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< let_exprt >()
: std_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< mod_exprt >()
: std_expr.h
- can_cast_expr< mult_exprt >()
: std_expr.h
- can_cast_expr< nil_exprt >()
: std_expr.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_descriptor_exprt >()
: std_expr.h
- can_cast_expr< or_exprt >()
: std_expr.h
- can_cast_expr< plus_exprt >()
: std_expr.h
- can_cast_expr< popcount_exprt >()
: std_expr.h
- can_cast_expr< power_exprt >()
: mathematical_expr.h
- can_cast_expr< quantifier_exprt >()
: mathematical_expr.h
- can_cast_expr< refined_string_exprt >()
: string_expr.h
- can_cast_expr< rem_exprt >()
: std_expr.h
- can_cast_expr< replication_exprt >()
: std_expr.h
- can_cast_expr< shift_exprt >()
: std_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_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< 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_plus_exprt >()
: std_expr.h
- can_cast_expr< union_exprt >()
: std_expr.h
- can_cast_expr< update_exprt >()
: std_expr.h
- can_cast_expr< vector_exprt >()
: std_expr.h
- can_cast_expr< with_exprt >()
: std_expr.h
- can_cast_expr< xor_exprt >()
: std_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< bv_typet >()
: std_types.h
- can_cast_type< c_bit_field_typet >()
: std_types.h
- can_cast_type< c_bool_typet >()
: std_types.h
- can_cast_type< c_enum_tag_typet >()
: std_types.h
- can_cast_type< c_enum_typet >()
: std_types.h
- can_cast_type< class_typet >()
: std_types.h
- can_cast_type< code_typet >()
: std_types.h
- can_cast_type< complex_typet >()
: std_types.h
- can_cast_type< enumeration_typet >()
: std_types.h
- can_cast_type< fixedbv_typet >()
: std_types.h
- can_cast_type< floatbv_typet >()
: std_types.h
- can_cast_type< integer_bitvector_typet >()
: std_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 >()
: std_types.h
- can_cast_type< range_typet >()
: std_types.h
- can_cast_type< reference_typet >()
: std_types.h
- can_cast_type< signedbv_typet >()
: std_types.h
- can_cast_type< string_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 >()
: std_types.h
- can_cast_type< union_typet >()
: std_types.h
- can_cast_type< unsignedbv_typet >()
: std_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
- 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
- check_address_structure()
: java_trace_validation.cpp
, java_trace_validation.h
- check_and_replace_target()
: replace_java_nondet.cpp
- check_apply_invariants()
: code_contracts.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_index_structure()
: java_trace_validation.cpp
, java_trace_validation.h
- check_lhs_assumptions()
: java_trace_validation.cpp
- check_member_structure()
: java_trace_validation.cpp
, java_trace_validation.h
- check_renaming()
: renaming_level.cpp
, renaming_level.h
- check_renaming_l1()
: renaming_level.cpp
, renaming_level.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
- checked_dereference()
: java_utils.cpp
, java_utils.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
- 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_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_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
- code_assign_function_application()
: java_string_library_preprocess.cpp
- codepoint_hex_to_utf16_native_endian()
: unicode.h
, unicode.cpp
- codepoint_hex_to_utf8()
: unicode.cpp
, unicode.h
- 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_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
- comment()
: race_check.cpp
- compare_components()
: jsil_types.cpp
- compiler_name()
: gcc_mode.cpp
- complex_member()
: remove_complex.cpp
- component()
: std_expr.cpp
- compute_address_taken_functions()
: compute_called_functions.cpp
, compute_called_functions.h
, compute_called_functions.cpp
- compute_called_functions()
: compute_called_functions.cpp
, compute_called_functions.h
, compute_called_functions.cpp
- compute_called_functions_from_ai()
: unreachable_instructions.cpp
- compute_functions()
: compute_called_functions.cpp
- compute_innermost_loop_ids()
: sese_regions.cpp
- compute_pointer_offset()
: pointer_offset_size.cpp
, pointer_offset_size.h
- concat_dir_file()
: file_util.h
, file_util.cpp
- concurrency()
: concurrency.cpp
, concurrency.h
- conditional_array_cast()
: java_bytecode_convert_method.cpp
- cone_of_influence()
: cone_of_influence.h
- configure_gcc()
: gcc_version.cpp
, gcc_version.h
- conjunction()
: std_expr.h
, std_expr.cpp
- const_literal()
: literal.h
- constant_bool()
: java_entry_point.cpp
- constant_float()
: string_constraint_generator_float.cpp
- constructor_of()
: constructor_of.h
- constructor_symbol()
: lambda_synthesis.cpp
- contains()
: string_constraint_instantiation.cpp
- contains_instanceof()
: remove_instanceof.cpp
- contains_symbol_prefix()
: graphml_witness.cpp
- convert()
: value_set_analysis.cpp
, xml_irep.h
, satcheck_minisat2.cpp
, satcheck_minisat.cpp
, builtin_factory.cpp
, json_goto_trace.h
, xml_goto_trace.h
, value_set_analysis.cpp
, xml_goto_trace.cpp
, value_set_analysis.h
, xml_irep.cpp
, satcheck_glucose.cpp
, xml_irep.h
, xml_irep.cpp
, value_set_analysis.h
- convert_annotations()
: java_bytecode_convert_class.cpp
, java_bytecode_convert_class.h
- convert_assert()
: json_goto_trace.h
, json_goto_trace.cpp
- convert_bool_literal()
: convert_bool_literal.cpp
, convert_bool_literal.h
- 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.h
, json_goto_trace.cpp
- convert_dint_bit_literal_value()
: convert_dint_literal.cpp
, convert_dint_literal.h
- convert_dint_dec_literal_value()
: convert_dint_literal.h
, convert_dint_literal.cpp
- convert_dint_hex_literal_value()
: convert_dint_literal.cpp
, convert_dint_literal.h
- convert_dint_literal_value()
: convert_dint_literal.cpp
- convert_float_literal()
: convert_float_literal.cpp
, convert_float_literal.h
- convert_identifier()
: convert_string_value.h
, convert_string_value.cpp
- convert_input()
: json_goto_trace.h
, json_goto_trace.cpp
- convert_int_bit_literal()
: convert_int_literal.h
, convert_int_literal.cpp
- convert_int_bit_literal_value()
: convert_int_literal.h
, convert_int_literal.cpp
- convert_int_dec_literal()
: convert_int_literal.h
, convert_int_literal.cpp
- convert_int_dec_literal_value()
: convert_int_literal.h
, convert_int_literal.cpp
- convert_int_hex_literal()
: convert_int_literal.h
, convert_int_literal.cpp
- convert_int_hex_literal_value()
: convert_int_literal.h
, convert_int_literal.cpp
- convert_integer_literal()
: convert_integer_literal.cpp
, convert_integer_literal.h
- convert_java_annotations()
: java_bytecode_convert_class.h
, java_bytecode_convert_class.cpp
- convert_label()
: convert_string_value.h
, convert_string_value.cpp
- convert_line()
: converter.cpp
, file_converter.cpp
- convert_member_name_to_enum_value()
: c_types_util.h
- convert_nondet()
: convert_java_nondet.cpp
, convert_java_nondet.h
, convert_java_nondet.cpp
, convert_java_nondet.h
, convert_java_nondet.cpp
- convert_one_string_literal()
: convert_string_literal.cpp
- convert_output()
: json_goto_trace.h
, json_goto_trace.cpp
- convert_properties_json()
: show_properties.cpp
, show_properties.h
- convert_real_literal()
: convert_real_literal.cpp
, convert_real_literal.h
- convert_return()
: json_goto_trace.cpp
, json_goto_trace.h
- convert_string_literal()
: convert_string_literal.cpp
, convert_string_literal.h
- convert_symex_target_equation()
: bmc_util.h
, bmc_util.cpp
- convert_synchronized_methods()
: java_bytecode_concurrency_instrumentation.cpp
, java_bytecode_concurrency_instrumentation.h
- convert_threadblock()
: java_bytecode_concurrency_instrumentation.h
, java_bytecode_concurrency_instrumentation.cpp
- convert_title()
: convert_string_value.cpp
, convert_string_value.h
- convert_version()
: convert_string_value.h
, convert_string_value.cpp
- copy_array()
: cpp_typecheck_constructor.cpp
- copy_member()
: cpp_typecheck_constructor.cpp
- copy_parent()
: cpp_typecheck_constructor.cpp
- count_eloc()
: count_eloc.cpp
, count_eloc.h
- count_expr_typed()
: show_program.cpp
- count_properties()
: properties.h
, properties.cpp
- cover_instrument_end_of_function()
: cover_instrument_other.cpp
, cover_instrument.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()
: parse.cpp
, cpp_parser.cpp
- cpp_symbol_expr()
: cpp_util.h
, cpp_util.cpp
- cpp_type2name()
: cpp_type2name.h
, cpp_type2name.cpp
- cpp_typecheck()
: cpp_typecheck.h
, cpp_typecheck.cpp
- cprover_c_library_factory()
: cprover_library.h
, cprover_library.cpp
- cprover_cpp_library_factory()
: cprover_library.h
, cprover_library.cpp
- create_alias_expression()
: code_contracts.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_clinit_wrapper_function_symbol()
: java_static_initializers.cpp
- create_clinit_wrapper_symbols()
: java_static_initializers.cpp
- create_data_block_parameter()
: statement_list_typecheck.cpp
- create_directory()
: file_util.h
, file_util.cpp
- create_fatal_assertion()
: std_code.h
, std_code.cpp
- create_function_symbol()
: java_static_initializers.cpp
- create_initialize()
: jsil_entry_point.cpp
- create_invokedynamic_synthetic_classes()
: lambda_synthesis.cpp
, lambda_synthesis.h
- create_java_initialize()
: java_entry_point.cpp
, java_entry_point.h
- create_method_stub_symbol()
: java_bytecode_convert_method.cpp
, java_bytecode_convert_method.h
- create_parameter_names()
: java_bytecode_convert_method.h
, java_bytecode_convert_method.cpp
- create_parameter_symbols()
: java_bytecode_convert_method.cpp
, java_bytecode_convert_method.h
- 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.h
, call_graph_test_utils.cpp
- cubes()
: miniBDD.h
, miniBDD.cpp