Here is a list of all class members with links to the classes they belong to:
- 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_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
- 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 : flow_insensitive_abstract_domain_baset, simplify_exprt
- CHANGED : simplify_exprt::resultt< T >
- changed : 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_typet, binary_exprt, binary_overflow_exprt, binary_predicate_exprt, binary_relation_exprt, bitvector_typet, bv_typet, c_bit_field_typet, c_bool_typet, 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_check_ct, goto_symex_fault_localizert, if_exprt, java_instanceof_exprt, member_exprt, nullary_exprt, overflow_result_exprt, pointer_typet, reference_typet, signedbv_typet, ssa_exprt, ternary_exprt, type_with_subtypet, typet, unary_exprt, unary_minus_overflow_exprt, unary_overflow_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_rec_member() : 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_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 : linear_functiont
- 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
- comp_remaining : mz_zip_reader_extract_iter_state
- 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 >
- 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
- conditionst : goto_check_ct
- conditiont() : goto_check_ct::conditiont
- 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_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_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, 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_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_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
- cur_file_ofs : mz_zip_reader_extract_iter_state
- 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