Here is a list of all class members with links to the classes 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 -

• c17 : ansi_c_parsert
• c23 : ansi_c_parsert
• c_assigns : ansi_c_convert_typet, code_with_contract_typet
• c_bit_field_typet() : c_bit_field_typet
• c_bool_cnt : ansi_c_convert_typet
• c_bool_typet() : c_bool_typet
• c_converter : gdb_value_extractort
• c_ensures : ansi_c_convert_typet, code_with_contract_typet
• c_enum_tag_typet() : c_enum_tag_typet
• c_enum_typet() : c_enum_typet
• c_frees : ansi_c_convert_typet, code_with_contract_typet
• c_object_factory_parameterst() : c_object_factory_parameterst
• c_qualifiers : ansi_c_convert_typet
• c_qualifierst() : c_qualifierst
• c_requires : ansi_c_convert_typet, code_with_contract_typet
• c_standard : configt::ansi_ct
• c_standardt : configt::ansi_ct
• c_storage_spec : ansi_c_convert_typet
• c_storage_spect() : c_storage_spect
• c_str() : dstringt, string_containert, string_ptrt
• c_test_input_generatort() : c_test_input_generatort
• c_typecastt() : c_typecastt
• c_typecheck_baset() : c_typecheck_baset
• c_typet : c_typecastt
• cache : boolbv_widtht, dfcc_swap_and_wrapt, goto_inlinet, graphml_witnesst, prop_conv_solvert
• cache_dereference() : goto_symext
• cache_dereferences : symex_configt
• cached_output : smt2_dect
• cachet : boolbv_widtht, goto_inlinet, prop_conv_solvert
• caching : goto_inlinet
• call_arguments() : goto_programt::instructiont
• call_depth : aggressive_slicert
• call_function() : function_call_harness_generatort::implt, goto_programt::instructiont
• call_graph : aggressive_slicert
• call_grapht() : call_grapht, call_grapht::directed_grapht
• call_lhs : framet, goto_programt::instructiont
• call_listt : goto_inlinet
• call_location_number : goto_inlinet::goto_inline_logt::goto_inline_log_infot
• call_stack : check_call_sequencet::statet, goto_symex_statet, goto_symex_statet::threadt, interpretert, state_encodingt
• call_stack_entryt() : call_stack_historyt::call_stack_entryt
• call_stack_history_factoryt() : call_stack_history_factoryt
• call_stack_historyt() : call_stack_historyt
• call_stackt : interpretert
• callable_methods : ci_lazy_methods_neededt
• callback : api_message_handlert
• called_function : goto_trace_stept, SSA_stept
• caller : call_stack_historyt::call_stack_entryt
• caller_is_known : reachability_slicert::search_stack_entryt
• caller_write_set : dfcc_wrapper_programt
• calling_function : interpretert::function_assignments_contextt
• calling_location : framet
• calls_memory_predicates() : dfcc_lift_memory_predicatest
• callsites : call_grapht, call_grapht::edge_with_callsitest
• callsitest : call_grapht
• callt : goto_inlinet
• camel_case() : labelt
• can_build_identifier() : ssa_exprt
• can_convert_lazy_method() : language_filest
• can_forward_propagatet() : can_forward_propagatet
• can_generate_function_body() : janalyzer_parse_optionst, jbmc_parse_optionst
• can_generate_function_bodyt : lazy_goto_functions_mapt, lazy_goto_modelt
• can_keep_file_local() : ansi_c_languaget, languaget, statement_list_languaget
• can_load_class() : java_class_loadert
• can_produce_function() : abstract_goto_modelt, goto_modelt, lazy_goto_functions_mapt, lazy_goto_modelt, wrapper_goto_modelt
• can_receive() : piped_processt
• car_expr_listt : instrument_spec_assignst
• car_exprt() : car_exprt
• carry() : bv_utilst
• carry_out() : bv_utilst
• cartesian_product_of_enumerators() : non_leaf_enumeratort
• case_exprt() : case_exprt
• case_guard() : goto_convertt
• case_is_allowed : c_typecheck_baset
• case_last : goto_program2codet::caset
• case_op() : code_switch_caset
• case_selector : goto_program2codet::caset
• case_start : goto_program2codet::caset
• case_value() : case_exprt
• cases : goto_convertt::break_switch_targetst, goto_convertt::targetst
• cases_listt : goto_program2codet
• cases_map : goto_convertt::break_switch_targetst, goto_convertt::targetst
• cases_mapt : goto_convertt
• casest : goto_convertt
• caset : goto_convertt, goto_program2codet::caset
• cast() : smt_check_sat_response_kindt, smt_indext, smt_responset, smt_sortt
• CAST_AS_NEEDED : java_bytecode_convert_methodt
• cast_away_constness() : cpp_typecheckt
• cast_bv_to_signed() : smt2_parsert
• cast_bv_to_unsigned() : smt2_parsert
• catch_expr() : code_landingpadt
• catch_handlerst : remove_exceptionst
• catch_map : framet
• catch_type : java_bytecode_parse_treet::methodt::exceptiont
• cause_loop_ids : cext
• cav11 : shared_bufferst
• cbegin() : cfg_baset< T, P, I >::entry_mapt, dense_integer_mapt< K, V, KeyToDenseInteger >, event_grapht::critical_cyclet, expanding_vectort< T >, fixed_keys_map_wrappert< mapt >, guarded_range_domaint, json_arrayt, json_objectt, numberingt< keyt, hasht >, range_domaint, union_find< T, hasht >, value_set_fit::object_map_dt
• cbmc_invariants_should_throwt() : cbmc_invariants_should_throwt
• cbmc_loop_id : dfcc_loop_infot
• cbmc_parse_optionst() : cbmc_parse_optionst
• cegis_evaluatort() : cegis_evaluatort
• cegis_verifiert() : cegis_verifiert
• cend() : cfg_baset< T, P, I >::entry_mapt, dense_integer_mapt< K, V, KeyToDenseInteger >, event_grapht::critical_cyclet, expanding_vectort< T >, fixed_keys_map_wrappert< mapt >, guarded_range_domaint, json_arrayt, json_objectt, numberingt< keyt, hasht >, range_domaint, union_find< T, hasht >, value_set_fit::object_map_dt
• cerr_message_handlert() : cerr_message_handlert
• cexs : cegis_evaluatort
• cext() : cext
• cfg : cfg_dominators_templatet< P, T, post_dom >, full_slicert, local_bitvector_analysist, local_may_aliast, points_tot, reachability_slicert
• cfg_baset() : cfg_baset< T, P, I >
• cfg_cycles_filter() : instrumentert
• cfg_dominators : natural_loops_templatet< P, T, C >
• cfg_info : instrument_spec_assignst
• cfg_nodet() : full_slicert::cfg_nodet
• cfg_post_dominators() : dependence_grapht, variable_sensitivity_dependence_grapht
• cfg_visitort() : instrumentert::cfg_visitort, shared_bufferst::cfg_visitort
• cfgt : cfg_dominators_templatet< P, T, post_dom >, full_slicert, points_tot, reachability_slicert
• chain() : minisat_prooft
• change_impact() : change_impactt
• change_impactt() : change_impactt
• change_spec() : bv_arithmetict, ieee_floatt
• CHANGED : simplify_exprt::resultt< T >
• changed : flow_insensitive_abstract_domain_baset, simplify_exprt, value_set_fit
• changed_vars : path_acceleratort
• changesett : journalling_symbol_tablet
• CHAR : c_typecastt
• char16_t_count : cpp_convert_typet
• char32_t_count : cpp_convert_typet
• char_assign() : string_abstractiont
• char_cnt : ansi_c_convert_typet
• char_is_unsigned : configt::ansi_ct
• char_representation_length : expr2javat
• char_type : java_string_library_preprocesst, string_constantt
• char_width : configt::ansi_ct
• CHARACTER : format_specifiert
• character : gdb_apit::pointer_valuet, string_concat_char_builtin_functiont, string_set_char_builtin_functiont
• character_preprocess : java_string_library_preprocesst
• CHARACTER_UPPER : format_specifiert
• check() : array_list_exprt, array_typet, binary_exprt, binary_overflow_exprt, binary_predicate_exprt, binary_relation_exprt, bitvector_typet, bv_typet, c_bit_field_typet, c_bool_typet, case_exprt, code_assignt, code_deadt, code_declt, code_frontend_assignt, code_frontend_declt, code_frontend_returnt, code_function_callt, code_inputt, code_outputt, code_returnt, conditional_target_group_exprt, constant_exprt, count_leading_zeros_exprt, count_trailing_zeros_exprt, custom_bitvector_analysist, dereference_exprt, equal_exprt, exprt, find_first_set_exprt, fixedbv_typet, floatbv_typet, goto_symex_fault_localizert, if_exprt, java_instanceof_exprt, member_exprt, nullary_exprt, overflow_result_exprt, pointer_typet, predicate_exprt, reference_typet, signedbv_typet, ssa_exprt, ternary_exprt, type_with_subtypet, typet, unary_exprt, unary_minus_overflow_exprt, unary_overflow_exprt, unary_predicate_exprt, unsignedbv_typet, update_bit_exprt, update_bits_exprt, update_exprt
• check_AC() : event_grapht::critical_cyclet
• check_address_can_be_taken() : c_typecastt
• check_all_functions_found() : code_contractst
• check_apply_loop_contracts() : code_contractst
• check_arithmetic_exception() : java_bytecode_instrumentt
• check_array_access() : java_bytecode_instrumentt
• check_array_length() : java_bytecode_instrumentt
• check_array_types() : cpp_declarator_convertert
• check_BC() : event_grapht::critical_cyclet
• check_break() : goto_symext, symex_bmc_incremental_one_loopt
• check_call_sequencet() : check_call_sequencet
• check_class_cast() : java_bytecode_instrumentt
• check_command_accepted() : gdb_apit
• check_complexity() : complexity_limitert
• check_component_access() : cpp_typecheckt
• check_containment() : gdb_value_extractort::memory_scopet
• check_contract() : dfcc_swap_and_wrapt
• check_field_exists() : java_bytecode_convert_classt
• check_fixed_size_array() : cpp_typecheckt
• check_frame_conditions_function() : code_contractst
• check_history_expr_return_value() : c_typecheck_baset
• check_inclusion_assignment() : instrument_spec_assignst
• check_inclusion_heap_allocated_and_invalidate_aliases() : instrument_spec_assignst
• check_index() : unsigned_union_find
• check_inductive() : acceleration_utilst, polynomial_acceleratort
• check_inline_map() : goto_inlinet
• check_lhs() : escape_domaint
• check_matching_operand_types() : smt2_parsert
• check_member_initializers() : cpp_typecheckt
• check_method_stub() : java_simple_method_stubst
• check_null_dereference() : java_bytecode_instrumentt
• check_qualifiers() : cpp_typecastt
• check_rec() : goto_check_ct
• check_rec_address() : goto_check_ct
• check_rec_arithmetic_op() : goto_check_ct
• check_rec_div() : goto_check_ct
• check_rec_if() : goto_check_ct
• check_rec_logical_op() : goto_check_ct
• check_replace_ensures_was_freed_preconditions_call() : dfcc_libraryt
• check_replacement_map() : replace_callst
• check_returns_removed : goto_model_validation_optionst
• check_SAT() : bv_refinementt
• check_sat() : scratch_programt
• check_shadow_memory_api_calls() : goto_check_ct
• check_side_effect : loop_contract_configt
• check_signature_compat() : dfcc_contract_handlert
• check_statust : goto_check_ct
• check_transform_goto_model_preconditions() : dfcct
• check_type() : invariant_propagationt, value_set_analysis_fit
• check_UNSAT() : bv_refinementt
• check_was_freed() : c_typecheck_baset
• CHECKED : goto_check_ct
• checked : overflow_instrumentert
• checked_expr : cegis_evaluatort, goto_null_checkt
• checked_pointer : cext
• checked_when_taken : goto_null_checkt
• checker : scratch_programt
• child_abstract_object : context_abstract_objectt
• child_process_id : piped_processt
• child_stream : json_streamt
• children : class_hierarchyt::entryt, structured_data_entryt
• children_too_complex : framet::active_loop_infot
• choice() : shared_bufferst
• choice_symbols : memory_model_baset
• choice_symbolst : memory_model_baset
• CHOP : java_bytecode_parse_treet::methodt::stack_map_table_entryt
• chops : java_bytecode_parse_treet::methodt::stack_map_table_entryt
• chunk : sharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >
• ci_lazy_methods_neededt() : ci_lazy_methods_neededt
• ci_lazy_methodst() : ci_lazy_methodst
• cit() : ctokenitt
• class_has_clinit_method : java_bytecode_convert_methodt
• class_hierarchy : ci_lazy_methodst, get_virtual_calleest, janalyzer_parse_optionst, java_bytecode_convert_methodt, java_bytecode_languaget, jbmc_parse_optionst, remove_exceptionst, remove_instanceoft, remove_virtual_functionst, taint_analysist, uncaught_exceptions_domaint
• class_hierarchyt() : class_hierarchyt
• class_id() : class_method_descriptor_exprt, dispatch_table_entryt, method_bytecodet::class_method_and_bytecodet
• class_identifier : class_hierarchy_graph_nodet, cpp_idt, resolve_inherited_componentt::inherited_componentt
• class_index : base_ref_infot
• class_infot() : class_infot
• class_initializer_seen : ci_lazy_methodst::convert_method_resultt
• class_map : class_hierarchyt, java_class_loadert
• class_mapt : class_hierarchyt
• class_method_descriptor_exprt() : class_method_descriptor_exprt
• class_name() : fieldref_exprt
• class_name_to_jar_file() : java_class_loader_baset
• class_name_to_os_file() : java_class_loader_baset
• class_nb : data_dpt
• class_refs : java_bytecode_parse_treet
• class_refst : java_bytecode_parse_treet
• class_template_identifier() : cpp_typecheckt
• class_template_symbol() : cpp_typecheckt
• class_typet() : class_typet
• classpath : configt::javat
• classpath_entries : java_class_loader_baset
• classpath_entryt() : java_class_loader_baset::classpath_entryt
• classpatht : configt::javat
• classt : java_bytecode_convert_classt, java_bytecode_parse_treet::classt, java_bytecode_parsert
• clause : c_wranglert::function_contract_clauset, c_wranglert::loop_contract_clauset
• clause_counter : cnf_solvert
• clause_id : clauset::stept
• clause_set : solver_hardnesst::sat_hardnesst
• clauses : cnf_clause_listt, resolution_prooft< T >, solver_hardnesst::sat_hardnesst
• clausest : cnf_clause_listt, resolution_prooft< T >
• clean() : cleanert
• clean_cache() : string_dependenciest
• clean_code : c_typecheck_baset
• clean_configuration : expr2c_configurationt
• clean_expr() : goto_convertt, goto_symext
• clean_expr_address_of() : goto_convertt
• clean_expr_resultt() : goto_convertt::clean_expr_resultt
• clean_up() : cpp_typecheckt
• cleaner : havoc_assigns_targetst
• cleanert() : cleanert
• cleanup() : goto_inlinet::goto_inline_logt, goto_unwindt::unwind_logt
• cleanup_code() : goto_program2codet
• cleanup_code_block() : goto_program2codet
• cleanup_code_ifthenelse() : goto_program2codet
• cleanup_decl() : dump_ct
• cleanup_expr() : dump_ct, goto_program2codet
• cleanup_function_call() : goto_program2codet
• cleanup_functions : escape_domaint::cleanupt
• cleanup_harness() : dump_ct
• cleanup_map : escape_domaint
• cleanup_mapt : escape_domaint
• cleanup_type() : dump_ct
• clear() : abstract_object_sett, ai_baset, ai_storage_baset, ansi_c_parse_treet, automatont, c_qualifierst, c_storage_spect, cmdlinet, cpp_idt, cpp_parse_treet, cpp_token_buffert, cpp_tokent, dstringt, event_grapht, expanding_vectort< T >, flow_insensitive_abstract_domain_baset, flow_insensitive_analysis_baset, flow_insensitive_analysist< T >, goto_functionst, goto_functiont, goto_inlinet, goto_modelt, goto_programt, goto_programt::instructiont, goto_tracet, grapht< N >, history_sensitive_storaget, irep_hash_container_baset, irep_hash_mapt< Key, T >, irep_serializationt, irep_serializationt::ireps_containert, irept, java_qualifierst, journalling_symbol_tablet, jsont, language_filest, literalt, local_bitvector_analysist::flagst, location_sensitive_storaget, mini_bddt, numberingt< keyt, hasht >, path_acceleratort, path_fifot, path_lifot, path_storaget, reference_counting< T, empty >, replace_symbolt, sharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >, sharing_nodet< keyT, valueT, equalT >, sparse_bitvector_analysist< V >, sparse_vectort< T >, statement_list_parse_treet, string_dependenciest, symbol_table_baset, symbol_table_buildert, symbol_tablet, symex_target_equationt, temp_dirt, template_mapt, trace_map_storaget, tree_nodet< treet, named_subtreest, sharing >, union_find< T, hasht >, unsigned_union_find, value_set_domain_fit, value_set_fit, value_sett, xml_parse_treet, xmlt
• clear_bit() : custom_bitvector_domaint
• clear_cache() : boolbvt, prop_conv_solvert, rd_range_domaint
• clear_classpath() : java_class_loader_baset
• clear_files() : language_filest
• clear_function() : parsert, source_locationt
• clear_input_flags() : interpretert
• clear_interrupt() : satcheck_minisat2_baset< T >
• clear_module_state() : statement_list_typecheckt
• clear_network_state() : statement_list_typecheckt
• clear_set() : find_is_fresh_calls_visitort
• clear_static_lifetime() : decorated_symbol_exprt
• clear_thread_local() : decorated_symbol_exprt
• clear_top() : abstract_objectt
• cleareol() : consolet
• clobbers() : code_asm_gcct
• clock() : partial_order_concurrencyt
• clock_type : partial_order_concurrencyt
• clockt : timestampert
• clone() : c_qualifierst, java_qualifierst
• clone_and_rename_function() : dfcc_utilst
• close() : json_streamt
• clusters : dott
• cmdline : armcc_modet, compilet, cw_modet, goto_cc_modet, linker_script_merget, ms_cl_modet, parse_options_baset
• cmdlinet() : cmdlinet
• cnf_clause_list_assignmentt() : cnf_clause_list_assignmentt
• cnf_clause_listt() : cnf_clause_listt
• cnf_handled_well() : propt
• cnf_solvert() : cnf_solvert
• cnft() : cnft
• code() : code_gcc_switch_case_ranget, code_labelt, code_switch_caset, code_without_referencest, get_or_create_reference_resultt, goto_programt::instructiont, java_bytecode_convert_methodt::converted_instructiont
• code_asm_gcct() : code_asm_gcct
• code_asmt() : code_asmt
• code_assertt() : code_assertt
• code_assign_components_to_java_string() : java_string_library_preprocesst
• code_assign_java_string_to_string_expr() : java_string_library_preprocesst
• code_assign_string_expr_to_java_string() : java_string_library_preprocesst
• code_assignt() : code_assignt
• code_assumet() : code_assumet
• code_blockt() : code_blockt
• code_breakt() : code_breakt
• code_continuet() : code_continuet
• code_contractst() : code_contractst
• code_deadt() : code_deadt
• code_declt() : code_declt
• code_dowhilet() : code_dowhilet
• code_expressiont() : code_expressiont
• code_for_function() : java_string_library_preprocesst
• code_fort() : code_fort
• code_frontend_assignt() : code_frontend_assignt
• code_frontend_declt() : code_frontend_declt
• code_frontend_returnt() : code_frontend_returnt
• code_function_bodyt() : code_function_bodyt
• code_function_callt() : code_function_callt
• code_gcc_switch_case_ranget() : code_gcc_switch_case_ranget
• code_gotot() : code_gotot
• code_ifthenelset() : code_ifthenelset
• code_inputt() : code_inputt
• code_labelt() : code_labelt
• code_landingpadt() : code_landingpadt
• code_nonconst() : goto_programt::instructiont
• code_operandst : code_blockt
• code_outputt() : code_outputt
• code_pop_catcht() : code_pop_catcht
• code_push_catcht() : code_push_catcht
• code_return_function_application() : java_string_library_preprocesst
• code_returnt() : code_returnt
• code_skipt() : code_skipt
• code_switch_caset() : code_switch_caset
• code_switcht() : code_switcht
• code_try_catcht() : code_try_catcht
• code_typet() : code_typet
• code_whilet() : code_whilet
• code_with_contract : dfcc_contract_functionst
• code_with_contract_typet() : code_with_contract_typet
• code_without_referencest() : code_without_referencest
• codet() : codet
• codomain() : mathematical_function_typet
• coeff : monomialt, polynomialt
• coefficients : algebraic_numbert, linear_functiont
• coefficientst : algebraic_numbert
• col_to_size_t() : instrument_spec_assignst::location_intervalt
• collect() : concurrency_instrumentationt, ranget< iteratort >
• collect_allocations() : goto_check_ct
• collect_arrays() : arrayst
• collect_bindings() : letifyt
• collect_callsites : call_grapht
• collect_cycles() : event_grapht, event_grapht::graph_explorert, instrumentert
• collect_cycles_by_SCCs() : instrumentert
• collect_generate_factory_options() : goto_harness_parse_optionst
• collect_guards() : goto_symex_fault_localizert
• collect_indices() : arrayst
• collect_malloc_calls() : gdb_apit
• collect_open_variables() : symex_slicet
• collect_operands() : goto_convertt
• collect_pairs() : event_grapht, event_grapht::graph_pensieve_explorert, instrumenter_pensievet
• collect_pairs_naive() : event_grapht, instrumenter_pensievet
• collect_parameters_to_lift() : dfcc_lift_memory_predicatest
• collect_references() : memory_snapshot_harness_generatort
• collect_static_symbols() : instrument_spec_assignst
• collect_typedefs() : dump_ct
• collect_typedefs_rec() : dump_ct
• collect_uncaught_exceptions() : uncaught_exceptions_analysist
• column : help_formattert::statet, parsert
• com_graph : event_grapht
• com_in() : event_grapht
• com_out() : event_grapht
• combine() : data_dependency_contextt, write_location_contextt
• combine_fn : write_location_contextt
• combine_results() : string_constraint_generatort
• combine_types() : cpp_declarator_convertert
• coming_from : instrumentert::cfg_visitort, shared_bufferst::cfg_visitort
• command() : console_message_handlert, inlining_decoratort, interpretert, message_handlert, messaget, messaget::commandt, smt2_parsert, ui_message_handlert
• command_line : cmdlinet::option_namest, cmdlinet::option_namest::option_names_iteratort
• command_line_description : smt_piped_solver_processt
• command_log : gdb_apit
• command_sequence() : smt2_parsert
• command_stream : gdb_apit, piped_processt
• commands : smt2_parsert
• commandst : gdb_apit
• commandt() : messaget::commandt
• comment : goto_trace_stept, SSA_stept
• comment_set : document_propertiest::doc_claimt
• common_ancestor : ancestry_resultt
• common_arguments_origins : recursive_initializationt
• compact_output : change_impactt
• compact_trace : trace_optionst
• compare() : dstringt, irept, monomialt, smt_bit_vector_theoryt
• compile() : compilet
• COMPILE_LINK : compilet
• COMPILE_LINK_EXECUTABLE : compilet
• COMPILE_ONLY : compilet
• compilet() : compilet
• complete_goto() : goto_programt::instructiont
• complete_path() : all_paths_enumeratort
• COMPLEX : c_typecastt
• complex_cnt : ansi_c_convert_typet
• complex_exprt() : complex_exprt
• complex_imag_exprt() : complex_imag_exprt
• complex_real_exprt() : complex_real_exprt
• complex_typet() : complex_typet
• complexity_active : complexity_limitert
• complexity_limitert() : complexity_limitert
• complexity_limits_active() : complexity_limitert, symex_configt
• complexity_module : goto_symext
• component() : struct_exprt
• component_identifier : resolve_inherited_componentt::inherited_componentt
• component_name() : field_address_exprt, fieldref_exprt
• component_number() : struct_union_typet
• component_type() : struct_union_typet
• components : identifiert, java_class_typet, labelt, struct_union_typet
• componentst : identifiert, java_class_typet, struct_union_typet
• componentt() : java_class_typet::componentt, struct_union_typet::componentt
• compose() : expr_skeletont
• compound() : member_exprt
• compound_counter : ansi_c_scopet, cpp_idt
• compound_type() : field_address_exprt
• compress_certificate() : qbf_bdd_coret
• compute() : _rw_set_loct, is_threadedt, lexical_loops_templatet< P, T, C >, natural_loops_templatet< P, T, C >, postconditiont, preconditiont
• compute_address_of() : preconditiont
• compute_coverage_lines() : goto_program_coverage_recordt
• compute_dependent_symbols() : enumerative_loop_contracts_synthesizert
• compute_edges() : cfg_baset< T, P, I >
• compute_edges_catch() : cfg_baset< T, P, I >
• compute_edges_function_call() : cfg_baset< T, P, I >, procedure_local_cfg_baset< T, P, I >, procedure_local_cfg_baset< T, java_bytecode_convert_methodt::method_with_amapt, java_bytecode_convert_methodt::method_offsett >
• compute_edges_goto() : cfg_baset< T, P, I >
• compute_edges_start_thread() : cfg_baset< T, P, I >, concurrent_cfg_baset< T, P, I >
• compute_edges_throw() : cfg_baset< T, P, I >
• compute_incoming_edges() : goto_functionst, goto_programt
• compute_lexical_loop() : lexical_loops_templatet< P, T, C >
• compute_location_numbers() : goto_functionst, goto_model_functiont, goto_programt
• compute_loop_numbers() : goto_functionst, goto_programt
• compute_natural_loop() : natural_loops_templatet< P, T, C >
• compute_overall_coverage() : symex_coveraget
• compute_rec() : preconditiont, rw_set_functiont
• compute_sese_regions() : sese_region_analysist
• compute_statistics() : string_containert
• compute_target_numbers() : goto_functionst, goto_programt
• compute_unsafe_pairs() : event_grapht::critical_cyclet
• computed_gotos : goto_convertt::targetst
• computed_gotost : goto_convertt
• con : d_containert< keyT, valueT, equalT >
• concat() : ranget< iteratort >, smt_bit_vector_theoryt
• concat_iteratort() : concat_iteratort< first_iteratort, second_iteratort >
• concatenate() : bv_utilst
• concatenation_exprt() : concatenation_exprt
• concrete_nodes : __CPROVER_jsa_abstract_heap
• concretize() : interval_sparse_arrayt
• concretize_type() : interpretert
• concurrency_aware_ait() : concurrency_aware_ait< domainT >
• concurrency_instrumentationt() : concurrency_instrumentationt
• cond() : code_dowhilet, code_fort, code_ifthenelset, code_whilet, cpp_static_assertt, if_exprt
• cond_expr : goto_trace_stept, SSA_stept
• cond_exprt() : cond_exprt
• cond_handle : SSA_stept
• cond_implies_equal() : bv_utilst
• cond_negate() : bv_utilst
• cond_negate_no_overflow() : bv_utilst
• cond_target_exprt_to_car_mapt : instrument_spec_assignst
• cond_value : goto_trace_stept
• condition() : car_exprt, conditional_target_exprt, conditional_target_group_exprt, cover_goalst::goalt, goto_programt::instructiont, goto_symex_property_decidert::goalt, invariant_failedt, prop_minimizet::objectivet, propertyt, smt_assert_commandt
• condition_nonconst() : goto_programt::instructiont
• conditional_cast() : typecast_exprt
• conditional_output() : messaget
• conditional_target_exprt() : conditional_target_exprt
• conditional_target_group_exprt() : conditional_target_group_exprt
• conditions : goto_program_coverage_recordt::coverage_linet
• cone_map : cone_of_influencet
• cone_mapt : cone_of_influencet
• cone_of_influence() : cone_of_influencet, disjunctive_polynomial_accelerationt, polynomial_acceleratort
• cone_of_influencet() : cone_of_influencet
• config() : variable_sensitivity_object_factoryt
• config_ : bv_refinementt, string_refinementt
• configuration() : abstract_environmentt, expr2ct, variable_sensitivity_dependence_domain_factoryt, variable_sensitivity_domain_factoryt, variable_sensitivity_object_factoryt
• configure_functions() : c_wranglert, contracts_wranglert
• configure_max_array_size() : vsd_configt
• configure_objects() : c_wranglert
• configure_output() : c_wranglert
• configure_sources() : c_wranglert
• configured_with() : variable_sensitivity_object_factoryt
• conflicts_with() : bv_refinementt
• connected_subgraphs() : grapht< N >
• console_message_handler : ui_message_handlert
• console_message_handlert() : console_message_handlert
• const_cast_target() : goto_programt
• const_depth_iterator_range_adaptert() : const_depth_iterator_range_adaptert
• const_depth_iteratort() : const_depth_iteratort
• const_iterator : abstract_object_sett, cfg_baset< T, P, I >::entry_mapt, dense_integer_mapt< K, V, KeyToDenseInteger >, event_grapht::critical_cyclet, expanding_vectort< T >, fixed_keys_map_wrappert< mapt >, forward_list_as_mapt< keyt, mappedt >, guarded_range_domaint, irep_hash_mapt< Key, T >, json_objectt, loop_templatet< T, C >, numberingt< keyt, hasht >, range_domaint, small_mapt< T, Ind, Num >::const_iterator, union_find< T, hasht >, value_set_fit::object_map_dt
• const_iteratort : sparse_vectort< T >, symbol_table_baset
• const_mapped_type : lazy_goto_functions_mapt
• const_pointer : lazy_goto_functions_mapt
• const_post_depth_iterator_range_adaptert() : const_post_depth_iterator_range_adaptert
• const_post_depth_iteratort() : const_post_depth_iteratort
• const_reference : lazy_goto_functions_mapt
• const_removed : goto_program2codet
• const_reverse_iterator : fixed_keys_map_wrappert< mapt >
• const_targetst : goto_programt, goto_programt::instructiont
• const_targett : goto_programt, goto_programt::instructiont
• const_typecast() : cpp_typecheckt
• const_unique_depth_iteratort() : const_unique_depth_iteratort
• const_value_iterator() : small_mapt< T, Ind, Num >::const_value_iterator
• const_var_no() : literalt
• constant() : java_bytecode_parsert
• constant_abstract_valuet() : constant_abstract_valuet
• constant_coefficient : linear_functiont
• constant_domain() : vsd_configt
• constant_exprt() : constant_exprt
• constant_index_ranget() : constant_index_ranget
• constant_interval_exprt() : constant_interval_exprt
• constant_pointer_abstract_objectt() : constant_pointer_abstract_objectt
• constant_pointer_abstract_pointert : constant_pointer_abstract_objectt
• constant_pool : java_bytecode_parsert
• constant_poolt : java_bytecode_parsert
• constant_propagate_assignment_with_side_effects() : goto_symext
• constant_propagate_case_change() : goto_symext
• constant_propagate_delete() : goto_symext
• constant_propagate_delete_char_at() : goto_symext
• constant_propagate_empty_string() : goto_symext
• constant_propagate_integer_to_string() : goto_symext
• constant_propagate_replace() : goto_symext
• constant_propagate_set_char_at() : goto_symext
• constant_propagate_set_length() : goto_symext
• constant_propagate_string_concat() : goto_symext
• constant_propagate_string_substring() : goto_symext
• constant_propagate_trim() : goto_symext
• constant_propagation : scratch_programt, symex_configt
• constant_propagator_ait() : constant_propagator_ait
• constant_propagator_can_forward_propagatet() : constant_propagator_can_forward_propagatet
• constant_propagator_domaint : constant_propagator_ait
• constant_struct_pointert : full_struct_abstract_objectt
• constants_done : smt2_solvert
• constants_evaluator() : constants_evaluator
• constrain() : abstract_value_objectt, bddt, constant_abstract_valuet, interval_abstract_valuet, value_set_abstract_objectt
• constraint() : cover_goalst, prop_minimizet, symex_target_equationt, symex_targett
• constraint_typet : arrayst
• constraints : axiomst, container_encoding_targett, string_builtin_function_with_no_evalt, string_builtin_functiont, string_concat_char_builtin_functiont, string_concatenation_builtin_functiont, string_format_builtin_functiont, string_insertion_builtin_functiont, string_of_int_builtin_functiont, string_set_char_builtin_functiont, string_to_lower_case_builtin_functiont, string_to_upper_case_builtin_functiont
• constraintst : container_encoding_targett
• construct_stack_to_array_index() : write_stackt
• construct_stack_to_lvalue() : write_stackt
• construct_stack_to_pointer() : write_stackt
• constructor : ansi_c_convert_typet
• constructor_type : recursive_initializationt::constructor_keyt
• consume_token() : mini_c_parsert
• container : cfg_baset< T, P, I >::entry_mapt
• container_encoding_targett() : container_encoding_targett
• container_id : generic_parameter_specialization_map_keyst
• container_index : generic_parameter_specialization_mapt::container_paramt
• container_to_specializations : generic_parameter_specialization_mapt
• contains() : constant_interval_exprt, cpp_scopet, gdb_value_extractort::memory_scopet, instrument_spec_assignst::location_intervalt, loop_templatet< T, C >, monomialt, nfat< T >::statet
• contains_cpp_name() : cpp_typecheckt
• contains_extreme() : constant_interval_exprt
• contains_method() : method_bytecodet
• contains_nested_loops() : acceleratet
• contains_shared_array() : instrumentert::cfg_visitort
• contains_zero() : constant_interval_exprt
• content() : array_string_exprt, c_wranglert::assertiont, c_wranglert::function_contract_clauset, c_wranglert::loop_contract_clauset, data, format_textt, refined_string_exprt
• context : api_message_handlert
• context_abstract_object_ptrt : context_abstract_objectt
• context_abstract_objectt() : context_abstract_objectt
• context_literal_counter : prop_conv_solvert
• context_prefix : prop_conv_solvert
• context_size_stack : prop_conv_solvert
• context_tracking : vsd_configt
• continuation_of_block() : cover_basic_blockst
• continuation_stack_storet : write_stackt
• continue_is_allowed : c_typecheck_baset
• continue_set : goto_convertt::break_continue_targetst, goto_convertt::targetst
• continue_stack_node : goto_convertt::targetst
• continue_target : goto_convertt::break_continue_targetst, goto_convertt::targetst
• contract_assigns : __CPROVER_contracts_write_set_t
• contract_cache : dfcc_contract_handlert
• contract_clauses_codegen : dfcc_contract_functionst, dfcc_contract_handlert, dfcc_instrument_loopt, dfcc_instrumentt, dfcct
• contract_clausest() : contract_clausest
• contract_code_type : dfcc_wrapper_programt
• contract_frees : __CPROVER_contracts_write_set_t
• contract_frees_append : __CPROVER_contracts_write_set_t
• contract_functions : dfcc_wrapper_programt
• contract_handler : dfcc_swap_and_wrapt, dfcct
• contract_lambda_parameters : dfcc_wrapper_programt
• contract_mode : dfcc_wrapper_programt
• contract_symbol : dfcc_wrapper_programt
• contract_write_set : dfcc_wrapper_programt
• contracts_wranglert() : contracts_wranglert
• control_dep_call_candidates : variable_sensitivity_dependence_domaint
• control_dep_calls : variable_sensitivity_dependence_domaint
• control_dep_callst : variable_sensitivity_dependence_domaint
• control_dep_candidates : dep_graph_domaint, variable_sensitivity_dependence_domaint
• control_dep_candidatest : variable_sensitivity_dependence_domaint
• control_dependencies() : dep_graph_domaint, variable_sensitivity_dependence_domaint
• control_deps : dep_graph_domaint, variable_sensitivity_dependence_domaint
• control_depst : variable_sensitivity_dependence_domaint
• control_flow_decision_history : local_control_flow_historyt< track_forward_jumps, track_backward_jumps >
• conversion() : float_bvt, float_utilst, format_specifiert
• conversion_check() : goto_check_ct
• conversion_failed() : boolbvt
• conversion_functiont : character_refine_preprocesst, java_string_library_preprocesst
• conversion_inputt : character_refine_preprocesst
• conversion_table : character_refine_preprocesst, java_string_library_preprocesst
• convert() : cpp_declarator_convertert, cpp_typecheckt, expr2ct, expr2javat, expr2stlt, float_bvt, goto_convertt, java_bytecode_convert_classt, java_bytecode_convert_methodt, prop_conv_solvert, prop_convt, show_goto_functions_jsont, show_goto_functions_xmlt, smt2_convt, smt_term_to_string_convertert, symex_target_equationt
• convert_abs() : boolbvt
• convert_add_sub() : boolbvt
• convert_address_of_rec() : bv_pointers_widet, bv_pointerst, smt2_convt
• convert_allocate() : expr2ct
• convert_aload() : java_bytecode_convert_methodt
• convert_and_analyze_method() : ci_lazy_methodst
• convert_annotated_pointer_constant() : expr2ct
• convert_anon_struct_union_member() : cpp_typecheckt
• convert_anonymous_union() : cpp_typecheckt
• convert_array() : boolbvt, expr2ct
• convert_array_comprehension() : boolbvt
• convert_array_list() : expr2ct
• convert_array_member_value() : expr2ct
• convert_array_of() : boolbvt, expr2ct
• convert_array_type() : expr2ct
• convert_asm() : goto_convertt
• convert_assert() : goto_convertt
• convert_assertions() : symex_target_equationt
• convert_assign() : goto_convertt, goto_program2codet
• convert_assign_rec() : goto_program2codet, graphml_witnesst
• convert_assign_varargs() : goto_program2codet
• convert_assignments() : symex_target_equationt
• convert_assume() : goto_convertt
• convert_assumptions() : symex_target_equationt
• convert_astore() : java_bytecode_convert_methodt
• convert_athrow() : java_bytecode_convert_methodt
• convert_atomic_begin() : goto_convertt
• convert_atomic_end() : goto_convertt
• convert_binary() : expr2ct
• convert_binary_overflow() : boolbvt
• convert_binding() : expr2ct
• convert_bitreverse() : boolbvt, expr2ct
• convert_bitvector() : boolbvt, bv_pointers_widet, bv_pointerst
• convert_bitwise() : boolbvt
• convert_block() : goto_convertt
• convert_bool() : prop_conv_solvert
• convert_bool_operand() : expr2stlt
• convert_break() : goto_convertt
• convert_bswap() : boolbvt
• convert_bv() : boolbvt
• convert_bv_reduction() : boolbvt
• convert_bv_rel() : boolbvt
• convert_bv_typecast() : boolbvt
• convert_byte_extract() : boolbvt, expr2ct
• convert_byte_update() : boolbvt, expr2ct
• convert_case() : boolbvt
• convert_catch() : goto_program2codet
• convert_char_count() : character_refine_preprocesst
• convert_char_function() : character_refine_preprocesst
• convert_char_value() : character_refine_preprocesst
• convert_checkcast() : java_bytecode_convert_methodt
• convert_class_template_specialization() : cpp_typecheckt
• convert_cmp() : java_bytecode_convert_methodt
• convert_cmp2() : java_bytecode_convert_methodt
• convert_code() : expr2cppt, expr2ct, expr2javat
• convert_code_array_copy() : expr2ct
• convert_code_array_replace() : expr2ct
• convert_code_array_set() : expr2ct
• convert_code_asm() : expr2ct
• convert_code_assert() : expr2ct
• convert_code_assume() : expr2ct
• convert_code_block() : expr2ct
• convert_code_break() : expr2ct
• convert_code_continue() : expr2ct
• convert_code_cpp_delete() : expr2cppt
• convert_code_cpp_new() : expr2cppt
• convert_code_dead() : expr2ct
• convert_code_decl_block() : expr2ct
• convert_code_dowhile() : expr2ct
• convert_code_expression() : expr2ct
• convert_code_fence() : expr2ct
• convert_code_for() : expr2ct
• convert_code_frontend_assign() : expr2ct
• convert_code_frontend_decl() : expr2ct
• convert_code_function_call() : expr2ct, expr2javat
• convert_code_goto() : expr2ct
• convert_code_ifthenelse() : expr2ct
• convert_code_input() : expr2ct
• convert_code_java_delete() : expr2javat
• convert_code_java_new() : expr2javat
• convert_code_label() : expr2ct
• convert_code_lock() : expr2ct
• convert_code_output() : expr2ct
• convert_code_printf() : expr2ct
• convert_code_return() : expr2ct
• convert_code_switch() : expr2ct
• convert_code_switch_case() : expr2ct
• convert_code_unlock() : expr2ct
• convert_code_while() : expr2ct
• convert_comma() : expr2ct
• convert_compare() : character_refine_preprocesst
• convert_complex() : boolbvt, expr2ct
• convert_complex_imag() : boolbvt
• convert_complex_real() : boolbvt
• convert_compound() : dump_ct
• convert_compound_declaration() : dump_ct
• convert_compound_enum() : dump_ct
• convert_concatenation() : boolbvt, expr2ct
• convert_cond() : boolbvt, expr2ct
• convert_conditional_target_group() : expr2ct
• convert_const() : java_bytecode_convert_methodt
• convert_constant() : boolbvt, expr2cppt, expr2ct, expr2javat, smt2_convt
• convert_constant_bool() : expr2ct
• convert_constraint_select_one() : boolbvt
• convert_constraints() : symex_target_equationt
• convert_continue() : goto_convertt
• convert_cpp_delete() : goto_convertt
• convert_cpp_new() : expr2cppt
• convert_cpp_this() : expr2cppt
• convert_CPROVER_throw() : goto_convertt
• convert_CPROVER_try_catch() : goto_convertt
• convert_CPROVER_try_finally() : goto_convertt
• convert_decl() : goto_program2codet
• convert_decl_type() : goto_convertt
• convert_decls() : symex_target_equationt
• convert_designated_initializer() : expr2ct
• convert_digit_char() : character_refine_preprocesst
• convert_digit_int() : character_refine_preprocesst
• convert_div() : boolbvt, bv_refinementt, smt2_convt
• convert_do_while() : goto_program2codet
• convert_dowhile() : goto_convertt
• convert_dup2() : java_bytecode_convert_methodt
• convert_dup2_x1() : java_bytecode_convert_methodt
• convert_dup2_x2() : java_bytecode_convert_methodt
• convert_empty_union() : boolbvt
• convert_end_thread() : goto_convertt
• convert_equality() : boolbvt
• convert_euclidean_mod() : smt2_convt
• convert_expr() : smt2_convt
• convert_expr_to_smt() : smt2_incremental_decision_proceduret
• convert_expression() : goto_convertt
• convert_exprt_to_string_exprt() : java_string_library_preprocesst
• convert_exprt_to_string_exprt_unit_test : java_string_library_preprocesst
• convert_extractbit() : boolbvt, expr2cppt, expr2ct
• convert_extractbits() : boolbvt, expr2ct
• convert_field_declaration() : shadow_memoryt
• convert_first_non_trivial_operand() : expr2stlt
• convert_floatbv() : smt2_convt
• convert_floatbv_div() : smt2_convt
• convert_floatbv_fma() : boolbvt, smt2_convt
• convert_floatbv_minus() : smt2_convt
• convert_floatbv_mod_rem() : boolbvt
• convert_floatbv_mult() : smt2_convt
• convert_floatbv_op() : boolbvt, bv_refinementt
• convert_floatbv_plus() : smt2_convt
• convert_floatbv_rem() : smt2_convt
• convert_floatbv_round_to_integral() : boolbvt, smt2_convt
• convert_floatbv_typecast() : boolbvt, smt2_convt
• convert_for() : goto_convertt
• convert_for_digit() : character_refine_preprocesst
• convert_from_irep() : json_irept
• convert_from_json() : json_irept
• convert_frontend_decl() : goto_convertt
• convert_function() : cpp_typecheckt, expr2ct, goto_convert_functionst
• convert_function_application() : boolbvt, expr2ct
• convert_function_call() : goto_convertt
• convert_function_calls() : symex_target_equationt
• convert_function_declaration() : dump_ct
• convert_function_group_json() : goto_difft
• convert_function_json() : goto_difft
• convert_gcc_computed_goto() : goto_convertt
• convert_gcc_local_label() : goto_convertt
• convert_gcc_switch_case_range() : goto_convertt
• convert_get_directionality_char() : character_refine_preprocesst
• convert_get_directionality_int() : character_refine_preprocesst
• convert_get_numeric_value_char() : character_refine_preprocesst
• convert_get_numeric_value_int() : character_refine_preprocesst
• convert_get_type_char() : character_refine_preprocesst
• convert_get_type_int() : character_refine_preprocesst
• convert_getstatic() : java_bytecode_convert_methodt
• convert_global_variable() : dump_ct
• convert_goals() : goto_symex_property_decidert
• convert_goto() : goto_convertt, goto_program2codet
• convert_goto_break_continue() : goto_program2codet
• convert_goto_goto() : goto_program2codet
• convert_goto_if() : goto_program2codet
• convert_goto_instructions() : symex_target_equationt
• convert_goto_switch() : goto_program2codet
• convert_goto_while() : goto_program2codet
• convert_guards() : symex_target_equationt
• convert_hash_code() : character_refine_preprocesst
• convert_high_surrogate() : character_refine_preprocesst
• convert_Hoare() : expr2ct
• convert_identifier() : cpp_typecheck_resolvet, smt2_convt
• convert_identifiers() : cpp_typecheck_resolvet
• convert_ieee_float_rel() : boolbvt
• convert_if() : boolbvt, java_bytecode_convert_methodt
• convert_if_cmp() : java_bytecode_convert_methodt
• convert_ifnonull() : java_bytecode_convert_methodt
• convert_ifnull() : java_bytecode_convert_methodt
• convert_ifthenelse() : goto_convertt
• convert_iinc() : java_bytecode_convert_methodt
• convert_index() : boolbvt, expr2ct, smt2_convt
• convert_index_designator() : expr2ct
• convert_initializer() : cpp_typecheckt
• convert_initializer_list() : expr2ct
• convert_instruction() : goto_program2codet
• convert_instructions() : java_bytecode_convert_methodt
• convert_invoke() : java_bytecode_convert_methodt
• convert_invoke_dynamic() : java_bytecode_convert_methodt
• convert_io() : symex_target_equationt
• convert_is_alphabetic() : character_refine_preprocesst
• convert_is_bmp_code_point() : character_refine_preprocesst
• convert_is_defined_char() : character_refine_preprocesst
• convert_is_defined_int() : character_refine_preprocesst
• convert_is_digit_char() : character_refine_preprocesst
• convert_is_digit_int() : character_refine_preprocesst
• convert_is_dynamic_object() : smt2_convt
• convert_is_high_surrogate() : character_refine_preprocesst
• convert_is_identifier_ignorable_char() : character_refine_preprocesst
• convert_is_identifier_ignorable_int() : character_refine_preprocesst
• convert_is_ideographic() : character_refine_preprocesst
• convert_is_ISO_control_char() : character_refine_preprocesst
• convert_is_ISO_control_int() : character_refine_preprocesst
• convert_is_java_identifier_part_char() : character_refine_preprocesst
• convert_is_java_identifier_part_int() : character_refine_preprocesst
• convert_is_java_identifier_start_char() : character_refine_preprocesst
• convert_is_java_identifier_start_int() : character_refine_preprocesst
• convert_is_java_letter() : character_refine_preprocesst
• convert_is_java_letter_or_digit() : character_refine_preprocesst
• convert_is_letter_char() : character_refine_preprocesst
• convert_is_letter_int() : character_refine_preprocesst
• convert_is_letter_or_digit_char() : character_refine_preprocesst
• convert_is_letter_or_digit_int() : character_refine_preprocesst
• convert_is_low_surrogate() : character_refine_preprocesst
• convert_is_lower_case_char() : character_refine_preprocesst
• convert_is_lower_case_int() : character_refine_preprocesst
• convert_is_mirrored_char() : character_refine_preprocesst
• convert_is_mirrored_int() : character_refine_preprocesst
• convert_is_space() : character_refine_preprocesst
• convert_is_space_char() : character_refine_preprocesst
• convert_is_space_char_int() : character_refine_preprocesst
• convert_is_supplementary_code_point() : character_refine_preprocesst
• convert_is_surrogate() : character_refine_preprocesst
• convert_is_surrogate_pair() : character_refine_preprocesst
• convert_is_title_case_char() : character_refine_preprocesst
• convert_is_title_case_int() : character_refine_preprocesst
• convert_is_unicode_identifier_part_char() : character_refine_preprocesst
• convert_is_unicode_identifier_part_int() : character_refine_preprocesst
• convert_is_unicode_identifier_start_char() : character_refine_preprocesst
• convert_is_unicode_identifier_start_int() : character_refine_preprocesst
• convert_is_upper_case_char() : character_refine_preprocesst
• convert_is_upper_case_int() : character_refine_preprocesst
• convert_is_valid_code_point() : character_refine_preprocesst
• convert_is_whitespace_char() : character_refine_preprocesst
• convert_is_whitespace_int() : character_refine_preprocesst
• convert_java_instanceof() : expr2javat
• convert_java_new() : expr2javat
• convert_java_this() : expr2javat
• convert_label() : goto_convertt
• convert_labels() : goto_program2codet
• convert_lazy_method() : java_bytecode_languaget, language_filest, language_filet, languaget
• convert_let() : boolbvt, expr2ct
• convert_literal() : expr2ct, smt2_convt
• convert_load() : java_bytecode_convert_methodt
• convert_loop_contracts() : goto_convertt
• convert_low_surrogate() : character_refine_preprocesst
• convert_member() : boolbvt, expr2ct, smt2_convt
• convert_member_designator() : expr2ct
• convert_minus() : smt2_convt
• convert_mod() : boolbvt, bv_refinementt, smt2_convt
• convert_monitorenterexit() : java_bytecode_convert_methodt
• convert_msc_leave() : goto_convertt
• convert_msc_try_except() : goto_convertt
• convert_msc_try_finally() : goto_convertt
• convert_mult() : boolbvt, bv_refinementt, smt2_convt
• convert_multi_ary() : expr2ct
• convert_multianewarray() : java_bytecode_convert_methodt
• convert_multiary_bool() : expr2stlt
• convert_multiary_bool_operands() : expr2stlt
• convert_named_sub_tree() : json_irept
• convert_new() : java_bytecode_convert_methodt
• convert_new_symbol() : cpp_declarator_convertert
• convert_newarray() : java_bytecode_convert_methodt
• convert_non_template_declaration() : cpp_typecheckt
• convert_nondet() : expr2ct
• convert_nondet_bool() : expr2ct
• convert_nondet_symbol() : expr2ct
• convert_norep() : expr2ct
• convert_not() : boolbvt
• convert_object_descriptor() : expr2ct
• convert_onehot() : boolbvt
• convert_overflow() : expr2ct
• convert_overflow_result() : boolbvt
• convert_parameter() : cpp_typecheckt
• convert_parameter_annotations() : java_bytecode_convert_methodt
• convert_parameters() : cpp_typecheckt
• convert_plus() : smt2_convt
• convert_pmop() : cpp_typecheckt
• convert_pointer_arithmetic() : expr2ct
• convert_pointer_difference() : expr2ct
• convert_pointer_in_range() : expr2ct
• convert_pointer_type() : bv_pointers_widet, bv_pointerst, select_pointer_typet
• convert_pop() : java_bytecode_convert_methodt
• convert_popcount() : boolbvt
• convert_power() : boolbvt
• convert_predicate_next_symbol() : expr2ct
• convert_predicate_passive_symbol() : expr2ct
• convert_predicate_symbol() : expr2ct
• convert_prob_coin() : expr2ct
• convert_prob_uniform() : expr2ct
• convert_prophecy_pointer_in_range() : expr2ct
• convert_prophecy_r_or_w_ok() : expr2ct
• convert_putfield() : java_bytecode_convert_methodt
• convert_putstatic() : java_bytecode_convert_methodt
• convert_quantified_symbol() : expr2ct
• convert_quantifier() : boolbvt
• convert_r_or_w_ok() : expr2ct
• convert_rec() : expr2cppt, expr2ct, expr2javat
• convert_reduction() : boolbvt
• convert_relation() : smt2_convt
• convert_replication() : boolbvt
• convert_rest() : boolbvt, bv_pointers_widet, bv_pointerst, prop_conv_solvert
• convert_ret() : java_bytecode_convert_methodt
• convert_return() : goto_convertt
• convert_reverse_bytes() : character_refine_preprocesst
• convert_rounding_mode_FPA() : smt2_convt
• convert_rox() : expr2ct
• convert_saturating_add_sub() : boolbvt
• convert_set_return_value() : goto_program2codet
• convert_shift() : boolbvt
• convert_shl() : java_bytecode_convert_methodt
• convert_side_effect_expr_function_call() : expr2ct
• convert_single_method() : java_bytecode_languaget
• convert_single_method_code() : java_bytecode_languaget
• convert_sizeof() : expr2ct
• convert_skip() : goto_convertt
• convert_start_thread() : goto_convertt, goto_program2codet
• convert_statement_expression() : expr2ct
• convert_store() : java_bytecode_convert_methodt
• convert_string_literal() : smt2_convt
• convert_struct() : boolbvt, expr2cppt, expr2ct, expr2javat, smt2_convt
• convert_struct_member_value() : expr2ct
• convert_struct_type() : expr2ct
• convert_sub_tree() : json_irept
• convert_switch() : goto_convertt, java_bytecode_convert_methodt
• convert_switch_case() : goto_convertt
• convert_symbol() : boolbvt, expr2ct
• convert_symbols() : compilet
• convert_template_declaration() : cpp_typecheckt
• convert_template_function_or_member_specialization() : cpp_typecheckt
• convert_template_parameter() : cpp_typecheck_resolvet
• convert_throw() : goto_program2codet
• convert_to_chars() : character_refine_preprocesst
• convert_to_lower_case_char() : character_refine_preprocesst
• convert_to_lower_case_int() : character_refine_preprocesst
• convert_to_title_case_char() : character_refine_preprocesst
• convert_to_title_case_int() : character_refine_preprocesst
• convert_to_upper_case_char() : character_refine_preprocesst
• convert_to_upper_case_int() : character_refine_preprocesst
• convert_trinary() : expr2ct
• convert_try_catch() : goto_convertt
• convert_type() : smt2_convt
• convert_typecast() : boolbvt, expr2ct, smt2_convt
• convert_unary() : expr2ct
• convert_unary_minus() : boolbvt
• convert_unary_overflow() : boolbvt
• convert_unary_post() : expr2ct
• convert_union() : boolbvt, expr2ct, smt2_convt
• convert_update() : boolbvt, expr2ct, smt2_convt
• convert_update_bit() : boolbvt, smt2_convt
• convert_update_bits() : boolbvt, smt2_convt
• convert_update_rec() : boolbvt
• convert_ushr() : java_bytecode_convert_methodt
• convert_vector() : expr2ct
• convert_verilog_case_equality() : boolbvt
• convert_while() : goto_convertt
• convert_with() : boolbvt, expr2ct, smt2_convt
• convert_with_array() : boolbvt
• convert_with_bv() : boolbvt
• convert_with_identifier() : expr2ct
• convert_with_precedence() : expr2cppt, expr2ct, expr2javat
• convert_with_struct() : boolbvt
• convert_with_union() : boolbvt
• convert_without_assertions() : symex_target_equationt
• converted : SSA_stept
• converted_compound : dump_ct
• converted_enum : dump_ct
• converted_function_arguments : SSA_stept
• converted_global : dump_ct
• converted_instructiont() : java_bytecode_convert_methodt::converted_instructiont
• converted_io_args : SSA_stept
• convertedt : dump_ct
• converter : dfcc_wrapper_programt
• converters : smt2_convt
• converterst : smt2_convt
• copied_symbol_table : dump_ct
• copy() : ai_domain_factory_baset, ai_domain_factoryt< domainT >, goto_convertt, small_mapt< T, Ind, Num >
• copy_and_erase() : small_mapt< T, Ind, Num >
• copy_and_insert() : small_mapt< T, Ind, Num >
• copy_assignment_from() : cnf_clause_list_assignmentt
• copy_cnf() : satcheck_zchaff_baset
• copy_from() : goto_functionst, goto_functiont, goto_inlinet::goto_inline_logt, goto_programt, reference_counting< T, empty >
• copy_item() : ansi_c_parsert
• copy_on_write_pointeet() : copy_on_write_pointeet< Num >
• copy_on_writet() : copy_on_writet< T >
• copy_segment() : event_grapht, goto_unwindt
• copy_source_location() : goto_program2codet
• copy_symbols() : linkingt
• copy_to() : cnf_clause_listt, qdimacs_cnft
• copy_to_operands() : exprt, nullary_exprt
• copy_to_subtypes() : type_with_subtypest
• correct_format : invalid_function_contract_pair_exceptiont, invalid_restriction_exceptiont
• correct_input : invalid_command_line_argument_exceptiont
• corresponding_primitive_type : java_boxed_type_infot
• cost : cpp_typecheck_resolvet::matcht, instrumentert
• count() : dense_integer_mapt< K, V, KeyToDenseInteger >, fixed_keys_map_wrappert< mapt >, framet::loop_infot, letifyt::let_count_idt, unsigned_union_find, unsigned_union_find::nodet
• count_assertions() : symex_target_equationt
• count_ignored_SSA_steps() : symex_target_equationt
• count_leading_zeros_exprt() : count_leading_zeros_exprt
• count_rec() : frequency_mapt
• count_roots() : unsigned_union_find
• count_trailing_zeros_exprt() : count_trailing_zeros_exprt
• count_transitions() : automatont
• count_type_leaves() : interpretert
• count_unmarked_nodes() : sharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >
• counter : ascii_encoding_targett
• counterexample_beautificationt() : counterexample_beautificationt
• counters : axiomst, frequency_mapt
• counterst : frequency_mapt
• cout_message_handlert() : cout_message_handlert
• cover_assertion_instrumentert() : cover_assertion_instrumentert
• cover_assume_instrumentert() : cover_assume_instrumentert
• cover_basic_blocks_javat() : cover_basic_blocks_javat
• cover_basic_blockst() : cover_basic_blockst
• cover_branch_instrumentert() : cover_branch_instrumentert
• cover_condition_instrumentert() : cover_condition_instrumentert
• cover_cover_instrumentert() : cover_cover_instrumentert
• cover_decision_instrumentert() : cover_decision_instrumentert
• cover_failed_assertions : cover_configt
• cover_goals_verifier_with_trace_storaget() : cover_goals_verifier_with_trace_storaget< incremental_goto_checkerT >
• cover_goalst() : cover_goalst
• cover_instrumenter_baset() : cover_instrumenter_baset
• cover_instrumenters : cover_configt
• cover_location_instrumentert() : cover_location_instrumentert
• cover_mcdc_instrumentert() : cover_mcdc_instrumentert
• cover_path_instrumentert() : cover_path_instrumentert
• coverage : symex_coveraget
• coverage_conditiont() : goto_program_coverage_recordt::coverage_conditiont
• coverage_criterion : cover_instrumenter_baset
• coverage_infot() : symex_coveraget::coverage_infot
• coverage_innert : symex_coveraget
• coverage_lines_mapt : goto_program_coverage_recordt
• coverage_linet() : goto_program_coverage_recordt::coverage_linet
• coverage_recordt() : coverage_recordt
• coveraget : symex_coveraget
• covered() : symex_coveraget
• covered_locationst : instrument_spec_assignst
• cpool_index : java_bytecode_parse_treet::methodt::verification_type_infot
• cpp : configt
• cpp11 : ansi_c_parsert, Parser
• cpp98 : ansi_c_parsert
• cpp_constructor() : cpp_typecheckt
• cpp_convert_typet() : cpp_convert_typet
• cpp_declarationt() : cpp_declarationt
• cpp_declarator_convertert() : cpp_declarator_convertert, cpp_typecheckt
• cpp_declaratort() : cpp_declaratort
• cpp_destructor() : cpp_typecheckt
• cpp_enum_typet() : cpp_enum_typet
• cpp_id_mapt : cpp_idt
• cpp_idt() : cpp_idt
• cpp_is_pod() : cpp_typecheckt
• cpp_languaget() : cpp_languaget
• cpp_linkage_spect() : cpp_linkage_spect
• cpp_member_spect() : cpp_member_spect
• cpp_namespace_spect() : cpp_namespace_spect
• cpp_namet() : cpp_namet
• cpp_new_initializer() : goto_convertt
• cpp_parse_tree : cpp_languaget, cpp_typecheckt
• cpp_parsert() : cpp_parsert
• cpp_root_scopet() : cpp_root_scopet
• cpp_save_scopet() : cpp_save_scopet
• cpp_saved_template_mapt() : cpp_saved_template_mapt
• cpp_scopes : cpp_save_scopet, cpp_typecheckt
• cpp_scopest() : cpp_scopest
• cpp_scopet() : cpp_scopet
• cpp_standard : configt::cppt
• cpp_standardt : configt::cppt
• cpp_static_assertt() : cpp_static_assertt
• cpp_storage_spect() : cpp_storage_spect
• cpp_template_args_baset() : cpp_template_args_baset
• cpp_token_buffert() : cpp_token_buffert
• cpp_typecastt() : cpp_typecastt
• cpp_typecheck : cpp_declarator_convertert, cpp_typecastt, cpp_typecheck_resolvet
• cpp_typecheck_fargst() : cpp_typecheck_fargst
• cpp_typecheck_resolvet() : cpp_typecheck_resolvet, cpp_typecheckt
• cpp_typecheckt() : cpp_typecheckt
• cpp_usingt() : cpp_usingt
• cprover_equivalent_to_java_assign_and_return_function : java_string_library_preprocesst
• cprover_equivalent_to_java_assign_function : java_string_library_preprocesst
• cprover_equivalent_to_java_constructor : java_string_library_preprocesst
• cprover_equivalent_to_java_function : java_string_library_preprocesst
• cprover_equivalent_to_java_string_returning_function : java_string_library_preprocesst
• cprover_exception_baset() : cprover_exception_baset
• cprover_macro_arities() : compilet
• cprover_parse_optionst() : cprover_parse_optionst
• crangler_parse_optionst() : crangler_parse_optionst
• crbegin() : fixed_keys_map_wrappert< mapt >
• create() : api_optionst
• create_car_expr() : instrument_spec_assignst
• create_car_from_heap_alloc() : instrument_spec_assignst
• create_car_from_spec_assigns() : instrument_spec_assignst
• create_car_from_stack_alloc() : instrument_spec_assignst
• create_car_from_static_local() : instrument_spec_assignst
• create_child_stream_array() : json_streamt
• create_child_stream_object() : json_streamt
• create_declarations() : is_fresh_baset, is_fresh_enforcet, is_fresh_replacet
• create_ensures_fn_call() : is_fresh_baset, is_fresh_enforcet, is_fresh_replacet
• create_flag() : free_form_cmdlinet
• create_from_root_function() : call_grapht
• create_gdb_process() : gdb_apit, gdb_value_extractort
• create_instance_data_block_type() : statement_list_typecheckt
• create_method_stub() : java_simple_method_stubst
• create_method_stub_at() : java_simple_method_stubst
• create_new_parameter_symbol() : dfcc_utilst
• create_requires_fn_call() : is_fresh_baset, is_fresh_enforcet, is_fresh_replacet
• create_small_shared_n_way_ptr() : small_shared_n_way_ptrt< Ts >
• create_snapshot() : instrument_spec_assignst
• create_stack_tmp_var() : java_bytecode_convert_methodt
• create_static_symbol() : dfcc_utilst
• create_stub_global_initializer_symbols() : stub_global_initializer_factoryt
• create_symbol() : dfcc_utilst
• created_strings() : array_poolt
• crend() : fixed_keys_map_wrappert< mapt >
• critical_cyclet() : event_grapht::critical_cyclet
• cscannert() : cscannert
• cse_ptrt : call_stack_historyt
• cstate_ptrt : ai_baset, ai_storage_baset
• cstrlen_exprt() : cstrlen_exprt
• ctokenitt() : ctokenitt
• ctokent() : ctokent
• ctrace_set_ptrt : ai_baset, ai_storage_baset
• cudd : bdd_managert
• cumulative : index_set_pairt
• cur : value_set_index_ranget, value_set_value_ranget
• current : ahistoricalt, empty_index_ranget, empty_value_ranget, index_range_implementationt, index_set_pairt, interval_index_ranget, map_iteratort< iteratort, outputt >, prop_minimizet, single_value_index_ranget, single_value_value_ranget, value_range_implementationt, value_set_index_ranget, value_set_value_ranget, xml_parsert, zip_iteratort< first_iteratort, second_iteratort, same_size >
• current_bindings : smt2_convt
• current_constraints : string_refinementt
• current_equation_converted : single_loop_incremental_symex_checkert
• current_function : goto_program_dereferencet, Parser
• current_hardness : solver_hardnesst
• current_linkage_spec : cpp_typecheckt
• current_loc : local_control_flow_historyt< track_forward_jumps, track_backward_jumps >
• current_location() : ahistoricalt, ai_history_baset, call_stack_historyt::call_stack_entryt, call_stack_historyt, local_control_flow_historyt< track_forward_jumps, track_backward_jumps >
• current_method : java_bytecode_convert_methodt
• current_names : symex_level1t, symex_level2t
• current_node : scope_treet
• current_pos : cpp_token_buffert
• current_scope() : ansi_c_parsert, cpp_scopest, Parser
• current_scope_ptr : cpp_scopest
• current_ssa_key : solver_hardnesst
• current_stack : call_stack_historyt
• current_symbol : c_typecheck_baset
• current_target : goto_check_ct, goto_program_dereferencet
• current_thread : instrumentert::cfg_visitort, shared_bufferst::cfg_visitort
• current_token() : cpp_parsert, cpp_token_buffert
• cursorup() : consolet
• custom_bitvector_domaint : custom_bitvector_analysist, custom_bitvector_domaint
• cw_modet() : cw_modet
• cyan() : consolet, messaget
• cycle_nb : event_grapht::graph_explorert
• cycles : shared_bufferst
• cycles_loc : shared_bufferst
• cycles_r_loc : shared_bufferst