Here is a list of all class members with links to the classes they belong to:

- i -

i : smt_bit_vector_theoryt::extractt, smt_bit_vector_theoryt::repeatt, smt_bit_vector_theoryt::rotate_leftt, smt_bit_vector_theoryt::rotate_rightt, smt_bit_vector_theoryt::sign_extendt, smt_bit_vector_theoryt::zero_extendt
id : abstract_eventt, ansi_c_languaget, bdd_nodet, cpp_languaget, cpp_typecheck_resolvet::matcht, datat, event_grapht::critical_cyclet, gdb_value_extractort::memory_scopet, interpretert::function_assignmentt, irept, java_bytecode_languaget, json_symtab_languaget, languaget, new_scopet, object_idt, operator_entryt, partial_order_concurrencyt, saj_tablet, statement_list_languaget, taint_parse_treet::rulet
id2cycloc : instrumentert
id2loc : instrumentert
id2node_pairt : instrumentert::cfg_visitort
id2nodet : instrumentert::cfg_visitort
id_class : ansi_c_identifiert, cpp_idt
id_classt : cpp_idt
id_listt : goto_program2codet
id_map : cpp_scopest, new_scopet, smt2_parsert
id_maps : java_string_library_preprocesst
id_mapt : cpp_scopest, java_string_library_preprocesst, new_scopet, smt2_parsert
ID_nondet_padding : nondet_padding_exprt
id_nr : bv_refinementt::approximationt
id_r : mm_iot
id_sett : cpp_scopest, cpp_scopet
id_shorthand() : expr2ct, expr2stlt
id_string() : irept
id_type_mapt : c_typecheck_baset
id_w : mm_iot
identifier : c_wranglert::assertiont, c_wranglert::loop_contract_clauset, cpp_idt, cpp_typecheckt::instantiationt, loop_contracts_clauset, reaching_definitiont, recursive_enumerator_placeholdert, smt_array_theoryt::selectt, smt_array_theoryt::storet, smt_bit_vector_theoryt::addt, smt_bit_vector_theoryt::andt, smt_bit_vector_theoryt::arithmetic_shift_rightt, smt_bit_vector_theoryt::comparet, smt_bit_vector_theoryt::concatt, smt_bit_vector_theoryt::extractt, smt_bit_vector_theoryt::logical_shift_rightt, smt_bit_vector_theoryt::multiplyt, smt_bit_vector_theoryt::nandt, smt_bit_vector_theoryt::negatet, smt_bit_vector_theoryt::nort, smt_bit_vector_theoryt::nott, smt_bit_vector_theoryt::ort, smt_bit_vector_theoryt::repeatt, smt_bit_vector_theoryt::rotate_leftt, smt_bit_vector_theoryt::rotate_rightt, smt_bit_vector_theoryt::shift_leftt, smt_bit_vector_theoryt::sign_extendt, smt_bit_vector_theoryt::signed_dividet, smt_bit_vector_theoryt::signed_greater_than_or_equalt, smt_bit_vector_theoryt::signed_greater_thant, smt_bit_vector_theoryt::signed_less_than_or_equalt, smt_bit_vector_theoryt::signed_less_thant, smt_bit_vector_theoryt::signed_remaindert, smt_bit_vector_theoryt::subtractt, smt_bit_vector_theoryt::unsigned_dividet, smt_bit_vector_theoryt::unsigned_greater_than_or_equalt, smt_bit_vector_theoryt::unsigned_greater_thant, smt_bit_vector_theoryt::unsigned_less_than_or_equalt, smt_bit_vector_theoryt::unsigned_less_thant, smt_bit_vector_theoryt::unsigned_remaindert, smt_bit_vector_theoryt::xnort, smt_bit_vector_theoryt::xort, smt_bit_vector_theoryt::zero_extendt, smt_command_functiont, smt_core_theoryt::andt, smt_core_theoryt::distinctt, smt_core_theoryt::equalt, smt_core_theoryt::if_then_elset, smt_core_theoryt::impliest, smt_core_theoryt::nott, smt_core_theoryt::ort, smt_core_theoryt::xort, smt_declare_function_commandt, smt_define_function_commandt, smt_identifier_termt, smt_symbol_indext, value_set_fit::entryt, value_sett::entryt
identifier_map : smt2_convt
identifier_mapt : smt2_convt
identifier_table : smt2_incremental_decision_proceduret
identifiers : sorted_variablest
identifiert : ansi_c_parsert, identifiert, smt2_convt::identifiert
identity : goto_check_ct
ids_and_types() : smt2_parsert::signature_with_parameter_idst
ids_from_indices() : class_hierarchy_grapht
idst : class_hierarchy_grapht, class_hierarchyt
idt : bdd_nodet, smt2_parsert::idt, value_set_fit
idx : small_mapt< T, Ind, Num >::const_iterator
ieee_equal() : ieee_float_valuet
ieee_float_equal_exprt() : ieee_float_equal_exprt
ieee_float_notequal_exprt() : ieee_float_notequal_exprt
ieee_float_op_exprt() : ieee_float_op_exprt
ieee_float_spect() : ieee_float_spect
ieee_float_valuet() : ieee_float_valuet
ieee_floatt() : ieee_floatt
ieee_not_equal() : ieee_float_valuet
if_exprt() : if_exprt
if_then_else : smt_core_theoryt
ignore : SSA_stept
ignore_arrays : event_grapht
ignore_assertions : goto_symext
ignore_command() : smt2_parsert
ignore_function_call_transform() : variable_sensitivity_domaint
ignore_manifest_main_class : java_bytecode_language_optionst
ignoring() : prop_conv_solvert
ii : small_mapt< T, Ind, Num >::const_iterator, small_mapt< T, Ind, Num >::const_value_iterator
imag() : complex_exprt
impact_mode : change_impactt
implementation : api_sessiont
implementationt : forward_list_as_mapt< keyt, mappedt >
implements : java_bytecode_parse_treet::classt
implements_function() : java_string_library_preprocesst
implements_java_char_sequence() : java_string_library_preprocesst
implements_java_char_sequence_pointer() : java_string_library_preprocesst
implementst : java_bytecode_parse_treet::classt
implications : framet
implicationt() : framet::implicationt
implicit_conversion_sequence() : cpp_typecheckt
implicit_generic_types() : java_implicitly_generic_class_typet
implicit_generic_typest : java_implicitly_generic_class_typet
implicit_typecast() : c_typecastt, c_typecheck_baset, cpp_typecastt, cpp_typecheckt
implicit_typecast_arithmetic() : c_typecastt, c_typecheck_baset, cpp_typecastt
implicit_typecast_bool() : c_typecheck_baset
implicit_typecast_followed() : c_typecastt, cpp_typecastt
implies() : invariant_sett, smt_core_theoryt
implies_exprt() : implies_exprt
implies_rec() : invariant_sett
in : cscannert, elf_readert, graph_nodet< E >, grapht< N >, osx_mach_o_readert, parsert, preprocessort, smt2_tokenizert
in_alphabet() : trace_automatont
in_blacklisted_loop() : complexity_limitert
in_core : satcheck_minisat1_coret, satcheck_zcoret
in_file : goto_harness_parse_optionst::goto_harness_configt
in_function_criteriont() : in_function_criteriont
in_interval_expr() : character_refine_preprocesst
in_invariant_clause_map : enumerative_loop_contracts_synthesizert
in_list() : goto_cc_cmdlinet
in_list_expr() : character_refine_preprocesst
in_pos : instrumentert::cfg_visitort
in_progress : language_modulet
in_scc : grapht< N >::tarjant
in_state_expr() : state_encodingt
in_use : cpp_typecheck_fargst
inc() : bv_utilst
inc_line_no() : parsert
include_array_size : expr2c_configurationt
include_comments : json_irept
include_compounds : dump_c_configurationt
include_files : configt::ansi_ct
include_function_bodies : dump_c_configurationt
include_function_decls : dump_c_configurationt
include_global_decls : dump_c_configurationt
include_global_vars : dump_c_configurationt
include_headers : dump_c_configurationt
include_paths : configt::ansi_ct, configt::verilogt
include_pattern_filtert() : include_pattern_filtert
include_struct_padding_components : expr2c_configurationt
include_typedefs : dump_c_configurationt
included_prefixes : prefix_filtert
includes : c_wranglert, range_typet
inclusion_check_assertion() : instrument_spec_assignst
inclusion_check_full() : instrument_spec_assignst
inclusion_check_single() : instrument_spec_assignst
incoming : state_encodingt
incoming_edges : goto_programt::instructiont
incoming_post : instrumentert::cfg_visitort
incoming_symbols() : state_encodingt
incomingt : state_encodingt
incorrect_goto_program_exceptiont() : incorrect_goto_program_exceptiont
incr_loop_id : symex_bmc_incremental_one_loopt
incr_max_unwind : symex_bmc_incremental_one_loopt
incr_min_unwind : symex_bmc_incremental_one_loopt
increase_generation() : symex_level2t
increment() : constant_interval_exprt, ieee_float_valuet
increment_designator() : c_typecheck_baset
increment_use_count() : copy_on_write_pointeet< Num >, small_shared_n_way_pointee_baset< N, Num >, small_shared_pointeet< Num >
incremental_cache : arrayst
incremental_goto_checker : all_properties_verifier_with_fault_localizationt< incremental_goto_checkerT >, all_properties_verifier_with_trace_storaget< incremental_goto_checkerT >, all_properties_verifiert< incremental_goto_checkerT >, cover_goals_verifier_with_trace_storaget< incremental_goto_checkerT >, stop_on_fail_verifier_with_fault_localizationt< incremental_goto_checkerT >, stop_on_fail_verifiert< incremental_goto_checkerT >
incremental_goto_checkert() : incremental_goto_checkert
incrementer() : bv_utilst
ind : small_mapt< T, Ind, Num >
IND : small_mapt< T, Ind, Num >
indent() : dump_ct, json_streamt
indent_str() : expr2ct
indeterminate_index_ranget() : indeterminate_index_ranget
index : __CPROVER_jsa_iterator, acceleration_utilst::polynomial_array_assignmentt, bdd_nodet, check_call_sequencet::statet, cmdlinet::option_namest::option_names_iteratort, designatort::entryt, element_address_exprt, extractbit_exprt, extractbits_exprt, format_specifiert, frame_reft, index_designatort, index_exprt, interval_index_ranget, java_bytecode_parse_treet::methodt::local_variablet, polynomial_acceleratort::polynomial_array_assignment, string_dependenciest::builtin_function_nodet, string_dependenciest::nodet, string_dependenciest::string_nodet, update_bit_exprt, update_bits_exprt
index_designatort() : index_designatort
index_exprt() : index_exprt
index_fieldt : small_mapt< T, Ind, Num >
index_is_set() : dense_integer_mapt< K, V, KeyToDenseInteger >
index_list : designatort
index_listt : designatort
index_map : arrayst
index_mapt : arrayst
index_range() : abstract_value_objectt
index_range_implementation() : abstract_value_objectt, constant_abstract_valuet, interval_abstract_valuet, value_set_abstract_objectt
index_range_iteratort() : index_range_iteratort
index_ranget : index_range_iteratort, index_ranget
index_sequence : smt2_incremental_decision_proceduret
index_sets : string_refinementt
index_sett : arrayst
index_sort() : smt_array_sortt
index_to_bdd : bdd_managert
index_to_block : cover_basic_blocks_javat
index_type() : array_typet, java_string_library_preprocesst, vector_typet
index_type_nonconst() : array_typet, vector_typet
indexed_by_object_id : __CPROVER_contracts_obj_set_t
indext : bdd_nodet
indicator_mask() : small_mapt< T, Ind, Num >
indices() : shuffle_vector_exprt, smt_bit_vector_theoryt::extractt, smt_bit_vector_theoryt::repeatt, smt_bit_vector_theoryt::rotate_leftt, smt_bit_vector_theoryt::rotate_rightt, smt_bit_vector_theoryt::sign_extendt, smt_bit_vector_theoryt::zero_extendt, smt_function_application_termt, smt_identifier_termt
INDUCTIVE : inductiveness_resultt
inductive() : inductiveness_resultt
inductiveness_resultt() : inductiveness_resultt
ineq_sett : invariant_sett
infinity : float_bvt::unpacked_floatt, float_utilst::unpacked_floatt
infinity_exprt() : infinity_exprt
infinity_flag : ieee_float_valuet
inflator : mz_zip_reader_extract_iter_state
inherited_componentt() : resolve_inherited_componentt::inherited_componentt
inhibit_front_end_builtins() : dfcc_libraryt
init() : code_fort, consolet
INIT : satcheck_zchaff_baset
init() : transt
init_args() : cpp_declaratort
init_candidates() : enumerative_loop_contracts_synthesizert
init_nta() : trace_automatont
init_state : automatont, trace_automatont
init_system_library_map() : system_library_symbolst
initial_equation_generated : single_loop_incremental_symex_checkert
initial_filtering() : event_grapht::graph_conc_explorert
initial_goto_location_line : memory_snapshot_harness_generatort
initial_source_location_line : memory_snapshot_harness_generatort
initial_state() : axiomst, nfat< T >
initial_state_exprs : axiomst
initial_state_exprt() : initial_state_exprt
initial_value() : code_frontend_declt
initialise() : cfg_dominators_templatet< P, T, post_dom >
initialization : string_abstractiont
initialization_config : recursive_initializationt
initialize() : ai_baset, bv_refinementt, custom_bitvector_analysist, dependence_grapht, escape_analysist, flow_insensitive_abstract_domain_baset, flow_insensitive_analysis_baset, global_may_alias_analysist, interpretert, invariant_propagationt, lazy_goto_modelt, reaching_definitions_analysist, recursive_initializationt, value_set_analysis_fit, value_set_domain_fit, variable_sensitivity_dependence_grapht
initialize_array_elements() : smt2_incremental_decision_proceduret
initialize_auto_object() : goto_symext
initialize_bit_expression() : statement_list_typecheckt
initialize_class_loader() : java_bytecode_languaget
initialize_conversion_table() : character_refine_preprocesst, java_string_library_preprocesst
initialize_entry_point_state() : goto_symext, scratch_program_symext
initialize_entry_via_goto() : memory_snapshot_harness_generatort
initialize_entry_via_source() : memory_snapshot_harness_generatort
initialize_file_index() : jar_filet
initialize_instantiated_classes() : ci_lazy_methodst
initialize_instantiated_classes_from_pointer() : ci_lazy_methods_neededt
initialize_known_type_table() : java_string_library_preprocesst
initialize_path_storage_from_entry_point_of() : goto_symext
initialize_selected_member() : recursive_initializationt
initialize_shadow_memory() : shadow_memoryt
initialize_source_location() : cover_instrumenter_baset
initialize_worklist() : single_path_symex_only_checkert
initialized : dirtyt, flow_insensitive_analysis_baset, interpretert::memory_cellt, lazy_class_to_declared_symbols_mapt
initializedt : interpretert::memory_cellt
initializer : c_declarationt
inline_and_check_warnings() : dfcc_contract_clauses_codegent
inline_function() : dfcc_utilst
inline_functions() : dfcc_libraryt
inline_log : goto_inlinet
inline_mapt : goto_inlinet
inline_program() : dfcc_utilst
inlined : dfcc_libraryt
inlining_decoratort() : inlining_decoratort
inner_loops : dfcc_loop_infot
inner_mapt : sparse_bitvector_analysist< V >
inner_name : java_bytecode_parse_treet::classt
inner_symbol() : replacement_predicatet
innert : d_internalt< keyT, valueT, equalT >
input : string_transformation_builtin_functiont, symex_target_equationt, symex_targett
input1 : string_insertion_builtin_functiont
input2 : string_insertion_builtin_functiont
input_entryt : interpretert
input_valuest : interpretert
input_vars : interpretert
inputs() : code_asm_gcct, string_format_builtin_functiont
insert() : abstract_object_sett, array_poolt, cpp_scopet
Insert() : cpp_token_buffert
insert() : dense_integer_mapt< K, V, KeyToDenseInteger >, generic_parameter_specialization_map_keyst, generic_parameter_specialization_mapt, goto_trace_storaget, goto_unwindt::unwind_logt, guarded_range_domaint, irep_hash_mapt< Key, T >, journalling_symbol_tablet, json_objectt, rename_symbolt, replace_symbolt, sharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >, source_linest, symbol_table_baset, symbol_table_buildert, symbol_tablet, symex_level1t, unchecked_replace_symbolt, value_set_fit, value_set_fit::object_map_dt, value_sett
insert_accelerator() : acceleratet
insert_actiont : value_sett
insert_add_decl_call() : dfcc_instrumentt
insert_after() : goto_programt
insert_all() : goto_trace_storaget
insert_automaton() : acceleratet
insert_before() : goto_programt
insert_before_swap() : goto_programt
insert_cleanup() : escape_analysist
insert_data_deps() : data_dependency_contextt
insert_entry() : recursion_set_entryt
insert_expr() : rename_symbolt
insert_final_assert_falset() : insert_final_assert_falset
insert_function_body() : goto_inlinet
insert_harness_function_into_goto_model() : memory_snapshot_harness_generatort
insert_instruction() : loop_templatet< T, C >
insert_local_static_decls() : dump_ct
insert_local_type_decls() : dump_ct
insert_looping_path() : acceleratet
insert_or_replace() : sharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >, symex_level1t
insert_record_dead_call() : dfcc_instrumentt
insert_type() : rename_symbolt
insert_view_item() : sharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >
inserted : journalling_symbol_tablet, memory_snapshot_harness_generatort::preordert< Key >
inside_bit_string : expr2stlt
INST_INDEX : java_bytecode_convert_methodt
INST_INDEX_CONST : java_bytecode_convert_methodt
instance_count : statement_list_parsert, xml_parsert
instances : goto_symex_property_decidert::goalt
instantiate() : binary_functional_enumeratort, binding_exprt, non_leaf_enumeratort
instantiate_gcc_polymorphic_builtin() : c_typecheck_baset
instantiate_not_contains() : string_refinementt
instantiate_template() : cpp_typecheckt
instantiated_classes : ci_lazy_methods_neededt
instantiation_levelt() : cpp_typecheckt::instantiation_levelt
instantiation_stack : cpp_typecheckt::instantiation_levelt, cpp_typecheckt, cpp_typecheckt::method_bodyt
instantiation_stackt : cpp_typecheckt
instruction : memory_snapshot_harness_generatort::source_location_matcht, scope_treet::declaration_statet
instruction_arguments : require_parse_tree::expected_instructiont
instruction_local_symbols : goto_symext
instruction_mnemoic : require_parse_tree::expected_instructiont
instruction_of() : cover_basic_blocks_javat, cover_basic_blockst, cover_blocks_baset
instruction_sizet : java_bytecode_convert_methodt
instructions : assembler_parsert, dfcc_loop_nesting_graph_nodet, goto_programt, java_bytecode_parse_treet::methodt, statement_list_parse_treet::networkt
instructions_equal() : unified_difft
instructionst : goto_programt, java_bytecode_convert_methodt, java_bytecode_parse_treet::methodt, statement_list_parse_treet
instructiont : assembler_parsert, goto_programt::instructiont, java_bytecode_convert_methodt, java_bytecode_parsert
instrument() : concurrency_instrumentationt, cover_assertion_instrumentert, cover_assume_instrumentert, cover_branch_instrumentert, cover_condition_instrumentert, cover_cover_instrumentert, cover_decision_instrumentert, cover_instrumenter_baset, cover_location_instrumentert, cover_mcdc_instrumentert, cover_path_instrumentert, custom_bitvector_analysist, dfcc_contract_functionst, dfcc_contract_handlert, dfcc_lift_memory_predicatest, dfcc_swap_and_wrapt, dfcc_wrapper_programt, dfcct, escape_analysist, string_instrumentationt, taint_analysist
instrument_all_inserter() : instrumentert
instrument_assign() : dfcc_instrumentt
instrument_assign_statement() : instrument_spec_assignst
instrument_call_instruction() : dfcc_instrumentt
instrument_call_statement() : instrument_spec_assignst
instrument_code() : java_bytecode_instrumentt
instrument_dead() : dfcc_instrumentt
instrument_deallocate_call() : dfcc_instrumentt
instrument_decl() : dfcc_instrumentt
instrument_exception_handler() : remove_exceptionst
instrument_exceptions() : remove_exceptionst
instrument_expr() : java_bytecode_instrumentt
instrument_fptr_call_instruction_dynamic_lookup() : dfcc_instrumentt
instrument_function() : dfcc_instrumentt
instrument_function_call() : dfcc_instrumentt, remove_exceptionst
instrument_goto_function() : dfcc_instrumentt
instrument_goto_program() : dfcc_instrumentt, goto_instrument_parse_optionst
instrument_harness_function() : dfcc_instrumentt, dfcct
instrument_instructions() : dfcc_instrumentt, instrument_spec_assignst
instrument_lhs() : dfcc_instrumentt
instrument_loop : dfcc_instrumentt
instrument_minimum_interference_inserter() : instrumentert
instrument_my_events() : instrumentert
instrument_my_events_inserter() : instrumentert
instrument_one_event_per_cycle_inserter() : instrumentert
instrument_one_read_per_cycle_inserter() : instrumentert
instrument_one_write_per_cycle_inserter() : instrumentert
instrument_other() : dfcc_instrumentt
instrument_other_functions() : dfcct
instrument_spec_assignst() : instrument_spec_assignst
instrument_throw() : remove_exceptionst
instrument_with_strategy() : instrumentert
instrument_without_loop_contracts_check_no_pointer_contracts() : dfcc_contract_functionst
instrument_wrapped_function() : dfcc_instrumentt
instrumentation_resultt : remove_exceptionst
instrumentations : shared_bufferst
instrumenter : instrumentert::cfg_visitort
instrumenter_pensievet() : instrumenter_pensievet
instrumenters : cover_instrumenterst
instrumentert() : instrumentert
INT : c_typecastt
int16_cnt : ansi_c_convert_typet
int32_cnt : ansi_c_convert_typet
int64_cnt : ansi_c_convert_typet
int8_cnt : ansi_c_convert_typet
int_cnt : ansi_c_convert_typet
int_map : interval_domaint
int_mapt : interval_domaint
int_width : configt::ansi_ct
INTEGER : c_typecastt, java_bytecode_parse_treet::methodt::verification_type_infot
integer_bits : fixedbv_spect
integer_bitvector_typet() : integer_bitvector_typet
integer_overflow_check() : goto_check_ct
integer_typet() : integer_typet
integral_conversion() : cpp_typecastt
integral_resultt : write_stackt
interfaces() : language_filest, languaget
internal : goto_trace_stept, location_sensitive_storaget
internal_abstract_object_pointert : abstract_objectt
internal_equality() : abstract_objectt, constant_abstract_valuet, interval_abstract_valuet
internal_hash() : abstract_objectt, constant_abstract_valuet, interval_abstract_valuet
internal_sharing_ptrt : abstract_objectt
internal_symbol_base_map : symbol_tablet
internal_symbol_module_map : symbol_tablet
internal_symbols : dfcc_instrumentt, symbol_tablet
interpreter_testt : interpretert
interpretert() : interpretert
interrupt() : satcheck_minisat2_baset< T >
intersect_with() : interval_templatet< T >
intersection() : invariant_sett, unsigned_union_find
interval : interval_abstract_valuet, interval_index_ranget
interval_abstract_value_pointert : interval_evaluator
interval_abstract_valuet() : interval_abstract_valuet
interval_domaint() : interval_domaint
interval_evaluator() : interval_evaluator
interval_index_ranget() : interval_index_ranget
interval_sparse_arrayt() : interval_sparse_arrayt
interval_templatet() : interval_templatet< T >
interval_uniont() : interval_uniont
intervals : interval_uniont, vsd_configt
intervalt : interval_uniont
inv_object_storet() : inv_object_storet
invalid_command_line_argument_exceptiont() : invalid_command_line_argument_exceptiont
invalid_function_contract_pair_exceptiont() : invalid_function_contract_pair_exceptiont
invalid_input_exceptiont() : invalid_input_exceptiont
invalid_object : pointer_logict
invalid_restriction_exceptiont() : invalid_restriction_exceptiont
invalid_source_file_exceptiont() : invalid_source_file_exceptiont
invalidate() : goto_check_ct
invalidate_buffer() : string_instrumentationt
invalidate_car() : instrument_spec_assignst
invalidate_heap_and_spec_aliases() : instrument_spec_assignst
invalidate_stack_allocated() : instrument_spec_assignst
invar() : transt
invariant : dfcc_loop_infot, workt, xml_graph_nodet
invariant_candidates : cegis_verifiert
invariant_expr : contract_clausest
invariant_failedt() : invariant_failedt
invariant_failure_containingt() : invariant_failure_containingt
invariant_propagationt() : invariant_propagationt, location_sensitive_storaget
invariant_scope : xml_graph_nodet
invariant_set : invariant_set_domaint
invariant_set_domain_factoryt : invariant_propagationt, invariant_set_domain_factoryt
invariant_set_domaint() : invariant_set_domaint
invariant_sett() : invariant_sett
invariant_with_diagnostics_failedt() : invariant_with_diagnostics_failedt
invariants : framet, loop_contracts_clauset
invariants_set : framet
inverse_memory_map : interpretert
inverse_memory_mapt : interpretert
invert() : literalt, rationalt
inverted() : bv_utilst
io_args : goto_trace_stept, SSA_stept
io_argst : goto_trace_stept
io_count : symex_target_equationt
io_id : goto_trace_stept, SSA_stept
ip : invariant_set_domain_factoryt
irep : irep_hash_container_baset::irep_entryt, irep_pretty_diagnosticst
irep_entryt() : irep_hash_container_baset::irep_entryt
irep_full_hash_container : irep_serializationt::ireps_containert
irep_full_hash_containert() : irep_full_hash_containert
irep_hash_container_baset() : irep_hash_container_baset
irep_hash_containert() : irep_hash_containert
irep_pretty_diagnosticst() : irep_pretty_diagnosticst
irep_serializationt() : irep_serializationt
irep_store : merge_full_irept, merge_irept
irep_storet : merge_full_irept, merge_irept
ireps_container : irep_serializationt
ireps_on_read : irep_serializationt::ireps_containert
ireps_on_readt : irep_serializationt::ireps_containert
ireps_on_write : irep_serializationt::ireps_containert
ireps_on_writet : irep_serializationt::ireps_containert
irept() : irept, smt_check_sat_response_kindt, smt_commandt, smt_indext, smt_logict, smt_responset, smt_sortt
is_a_tty : console_message_handlert
is_abstract : class_hierarchyt::entryt, class_typet, java_bytecode_parse_treet::classt, java_bytecode_parse_treet::methodt
is_accepting() : automatont
is_all() : cnft
is_all_ones() : bv_utilst
is_always_simplified : guard_bddt, guard_exprt
is_annotation : java_bytecode_parse_treet::classt
is_anonymous_class : java_bytecode_parse_treet::classt
is_array() : jsont
is_array_size_parameter() : recursive_initializationt
is_asm() : cpp_storage_spect
is_assert() : goto_programt::instructiont, goto_trace_stept, SSA_stept
is_assign() : goto_programt::instructiont
is_assignment() : goto_trace_stept, SSA_stept
is_assume() : goto_programt::instructiont, goto_trace_stept, SSA_stept
is_at_least() : gcc_versiont, ms_cl_versiont
is_atomic : c_qualifierst
is_atomic_begin() : goto_programt::instructiont, goto_trace_stept, SSA_stept
is_atomic_end() : goto_programt::instructiont, goto_trace_stept, SSA_stept
is_auto() : cpp_storage_spect
is_auxiliary : symbolt
is_backwards_goto() : goto_programt::instructiont
is_bitvector() : constant_interval_exprt
is_boolean() : exprt, jsont
is_bot() : constant_propagator_domaint::valuest
is_bottom() : abstract_environmentt, abstract_objectt, ai_domain_baset, constant_interval_exprt, constant_propagator_domaint, constant_propagator_domaint::valuest, context_abstract_objectt, custom_bitvector_domaint, dep_graph_domaint, escape_domaint, global_may_alias_domaint, interval_domaint, interval_templatet< T >, invariant_set_domaint, is_threaded_domaint, rd_range_domaint, uninitialized_domaint, value_set_domain_templatet< VST >, variable_sensitivity_dependence_domaint, variable_sensitivity_domaint
is_bound : smt2_convt::identifiert
is_bridge : java_bytecode_parse_treet::methodt
is_buffered() : shared_bufferst
is_buffered_in_general() : shared_bufferst
is_built_in() : source_locationt
is_catch() : goto_programt::instructiont
is_cfg_spurious() : instrumentert
is_char_type() : string_abstractiont
is_class() : cpp_idt, struct_typet, struct_union_typet
is_class_template() : cpp_declarationt
is_code : cpp_declarator_convertert
is_code_type() : cpp_declarator_convertert
is_comment() : irept
is_commutative() : binary_functional_enumeratort
is_compile_time_constantt() : is_compile_time_constantt
is_compiled() : symbolt
is_complement() : bdd_nodet
is_complete() : array_typet
is_complete_type() : c_typecheck_baset
is_const_expression() : remove_const_function_pointerst
is_const_type() : remove_const_function_pointerst
is_constant() : bdd_nodet, bv_utilst, c_qualifierst, can_forward_propagatet, constant_propagator_can_forward_propagatet, constant_propagator_domaint::valuest, exprt, goto_symex_can_forward_propagatet, havoc_utils_can_forward_propagatet, havoc_utilst, inv_object_storet::entryt, inv_object_storet, is_compile_time_constantt, literalt, mini_bddt
is_constant_address() : inv_object_storet
is_constant_address_of() : can_forward_propagatet, is_compile_time_constantt
is_constant_address_rec() : inv_object_storet
is_constant_value() : value_set_evaluator
is_constraint() : goto_trace_stept, SSA_stept
is_constructor() : cpp_declarationt, cpp_idt
is_container() : sharing_nodet< keyT, valueT, equalT >
is_corresponding_fence() : abstract_eventt
is_cstring_exprs : axiomst
is_cstring_exprt() : is_cstring_exprt
is_cstring_fc() : axiomst
is_cumul() : abstract_eventt
is_cycle() : event_grapht::critical_cyclet
is_dag() : grapht< N >
is_dead() : goto_programt::instructiont, goto_trace_stept
is_decimal : parse_floatt
is_decl() : goto_programt::instructiont, goto_trace_stept, SSA_stept
is_declaration() : cpp_itemt
is_default() : code_switch_caset
is_defined_container() : sharing_nodet< keyT, valueT, equalT >
is_defined_internal() : sharing_nodet< keyT, valueT, equalT >
is_defined_leaf() : sharing_nodet< keyT, valueT, equalT >
is_definitely_false() : constant_interval_exprt
is_definitely_true() : constant_interval_exprt
is_derived() : small_shared_n_way_pointee_baset< N, Num >, small_shared_n_way_ptrt< Ts >
is_destructor() : cpp_declarationt, cpp_namet
is_dfcc_library_symbol() : dfcc_libraryt
is_direct() : abstract_eventt
is_dirty : function_cfg_infot, loop_cfg_infot, reaching_definitions_analysist
is_divisible() : field_sensitivityt
is_double() : ieee_float_valuet
is_dynamic : decision_procedure_objectt
is_dynamic_heap() : local_bitvector_analysist::flagst
is_dynamic_local() : local_bitvector_analysist::flagst
is_dynamic_object() : pointer_logict
is_dynamic_object_exprs : axiomst
is_dynamic_object_exprt() : is_dynamic_object_exprt
is_dynamic_object_fc() : axiomst
is_dynamic_object_function : smt2_incremental_decision_proceduret
is_eliminated() : satcheck_glucose_simplifiert, satcheck_minisat_simplifiert
is_empty : __CPROVER_contracts_obj_set_t, constant_interval_exprt, constant_propagator_domaint::valuest, cpp_declarationt, cpp_member_spect, cpp_storage_spect, interval_uniont
is_end_function() : goto_programt::instructiont
is_end_thread() : goto_programt::instructiont
is_enum() : cpp_idt, java_bytecode_parse_treet::classt, java_bytecode_parse_treet::fieldt
is_eq() : invariant_sett
is_equal() : float_bvt
is_equivalence_class_representation() : binary_functional_enumeratort, non_leaf_enumeratort
is_error() : main_function_resultt
is_exchangeable : binary_functional_enumeratort
is_explicit() : cpp_member_spect
is_exported : symbolt
is_extern : c_storage_spect, cpp_storage_spect, symbolt
is_extreme() : constant_interval_exprt
is_false() : bddt, constant_interval_exprt, exprt, guard_bddt, guard_exprt, invariant_sett, jsont, literalt, mini_bddt, tvt
is_fence() : abstract_eventt
is_file_local : symbolt
is_final : java_bytecode_parse_treet::classt, java_bytecode_parse_treet::membert
is_float() : constant_interval_exprt, ieee_float_valuet, interval_domaint, parse_floatt
is_float128 : parse_floatt
is_float128x : parse_floatt
is_float16 : parse_floatt
is_float32 : parse_floatt
is_float32x : parse_floatt
is_float64 : parse_floatt
is_float64x : parse_floatt
is_float80 : parse_floatt
is_format_specifier() : format_elementt
is_format_text() : format_elementt
is_fresh_baset() : is_fresh_baset
is_fresh_calls() : find_is_fresh_calls_visitort
is_fresh_enforcet() : is_fresh_enforcet
is_fresh_replacet() : is_fresh_replacet
is_friend : cpp_declarator_convertert, cpp_member_spect
is_front_end_builtin() : dfcc_libraryt
is_function() : c_declarationt, symbolt
is_function_call() : goto_programt::instructiont, goto_trace_stept, SSA_stept
is_function_return() : goto_trace_stept, SSA_stept
is_ge() : invariant_sett
is_global_scope() : cpp_scopet
is_good : eval_index_resultt
is_good_partition : non_leaf_enumeratort
is_goto() : goto_programt::instructiont, goto_trace_stept, SSA_stept
is_goto_binary() : api_sessiont
is_gt() : invariant_sett
is_hidden() : goto_functiont
is_ignored() : goto_inlinet
is_ignored_method() : java_bytecode_convert_classt
is_imaginary : parse_floatt
is_in_both_maps() : sharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >::delta_view_itemt
is_in_bounds_of_some_explicit_allocation() : goto_check_ct
is_in_conflict() : conflict_providert, dimacs_cnft, external_satt, prop_conv_solvert, propt, satcheck_cadical_baset, satcheck_glucose_baset< T >, satcheck_ipasirt, satcheck_lingelingt, satcheck_minisat1_baset, satcheck_minisat2_baset< T >, satcheck_picosatt
is_in_core() : qbf_bdd_coret, qbf_qube_coret, qbf_skizzo_coret, qbf_squolem_coret, qdimacs_coret, satcheck_booleforce_coret, satcheck_minisat1_coret, satcheck_zcoret
is_incomplete() : array_typet, c_enum_typet, struct_union_typet
is_incomplete_goto() : goto_programt::instructiont
is_infile_name : goto_cc_cmdlinet::argt
is_infinity() : float_utilst, ieee_float_valuet
is_initialization_allowed() : recursive_initializationt
is_initialized() : mini_bddt
is_inline : c_storage_spect, cpp_member_spect
is_inner_class : java_bytecode_parse_treet::classt
is_input() : goto_trace_stept, symbolt
is_instruction_in_transformed_loop() : cegis_verifiert
is_instruction_in_transformed_loop_condition() : cegis_verifiert
is_int() : constant_interval_exprt, interval_domaint
is_int_min() : bv_utilst
is_integer_address() : local_bitvector_analysist::flagst
is_interface : java_bytecode_parse_treet::classt
is_internal() : sharing_nodet< keyT, valueT, equalT >
is_internal_symbol() : dfcc_instrumentt
is_invalid_pointer_exprt() : is_invalid_pointer_exprt
is_java_char_array_pointer_type() : java_string_library_preprocesst
is_java_char_array_type() : java_string_library_preprocesst
is_java_char_sequence_pointer_type() : java_string_library_preprocesst
is_java_char_sequence_type() : java_string_library_preprocesst
is_java_string_buffer_pointer_type() : java_string_library_preprocesst
is_java_string_buffer_type() : java_string_library_preprocesst
is_java_string_builder_pointer_type() : java_string_library_preprocesst
is_java_string_builder_type() : java_string_library_preprocesst
is_java_string_pointer_type() : java_string_library_preprocesst
is_java_string_type() : java_string_library_preprocesst
is_known() : tvt
is_known_string_type() : java_string_library_preprocesst
is_KnR() : code_typet
is_le() : invariant_sett
is_leaf() : sharing_nodet< keyT, valueT, equalT >, structured_data_entryt
is_less_than() : interval_templatet< T >
is_less_than_eq() : interval_templatet< T >
is_lifted_function() : dfcc_lift_memory_predicatest
is_linear_arithmetic_expr() : string_constraintt
is_linkage_spec() : cpp_itemt
is_local() : cfg_infot, event_grapht, function_cfg_infot, goto_program_cfg_infot, localst, loop_cfg_infot
is_local_composite_access() : cfg_infot
is_location() : goto_programt::instructiont, goto_trace_stept, SSA_stept
is_long : parse_floatt
is_loop_header() : loop_analysist< T, C >
is_looping() : all_paths_enumeratort
is_lower_widened : widened_ranget
is_lt() : invariant_sett
is_lte() : instrument_spec_assignst::location_intervalt
is_lvalue : symbolt
is_macro : symbolt
is_max() : constant_interval_exprt
is_member : cpp_idt
is_memory_barrier() : goto_trace_stept, SSA_stept
is_method : cpp_idt
is_method_inherited() : java_bytecode_convert_methodt
is_min() : constant_interval_exprt
is_minus_inf() : float_utilst
is_mutable() : cpp_storage_spect
is_named_scope() : new_scopet
is_namespace() : cpp_idt
is_namespace_spec() : cpp_itemt
is_NaN() : float_utilst, ieee_float_valuet
is_native : java_bytecode_parse_treet::methodt
is_ne() : invariant_sett
is_negative() : constant_interval_exprt, ieee_float_valuet, rationalt
is_nil() : irept, lispexprt
is_nodiscard : c_qualifierst
is_non_cover_assertion() : cover_instrumenter_baset
is_non_null_at_program_point() : local_safe_pointerst
is_nondet : nondet_instruction_infot
is_nondett : nondet_instruction_infot
is_noreturn : c_qualifierst
is_normal() : float_utilst, ieee_float_valuet
is_not_local_or_dirty_local() : cfg_infot, function_cfg_infot, goto_program_cfg_infot, loop_cfg_infot
is_not_nil() : irept
is_not_thin_air() : event_grapht::critical_cyclet
is_not_uniproc() : event_grapht::critical_cyclet
is_not_weak_uniproc() : event_grapht::critical_cyclet
is_not_zero() : bv_utilst
is_null() : gdb_apit::memory_addresst, jsont, local_bitvector_analysist::flagst
is_null_pointer() : constant_exprt
is_nullable : nondet_instruction_infot, recursive_initializationt::constructor_keyt
is_nullablet : nondet_instruction_infot
is_number() : jsont
is_numeric() : constant_interval_exprt
is_numeric_type() : c_typecheck_baset
is_object() : jsont
is_object_bits_default : configt::bv_encodingt
is_one() : bv_utilst, exprt, rationalt
is_opaque_function_call() : remove_calls_no_bodyt
is_operator() : cpp_namet
is_other() : goto_programt::instructiont
is_output() : goto_trace_stept, SSA_stept, symbolt
is_overlay_method() : java_bytecode_convert_classt
is_parameter() : java_bytecode_convert_methodt, java_bytecode_convert_methodt::local_variable_with_holest, java_bytecode_convert_methodt::variablet, symbolt
is_path_merge_history() : local_control_flow_historyt< track_forward_jumps, track_backward_jumps >
is_plus_inf() : float_utilst
is_po : event_grapht::critical_cyclet::delayt
is_positive() : constant_interval_exprt
is_predecessor_oft() : is_predecessor_oft
is_prefix_of() : struct_typet
is_printable_xml() : xmlt
is_private : java_bytecode_parse_treet::classt, java_bytecode_parse_treet::membert
is_property : symbolt
is_protected : java_bytecode_parse_treet::classt, java_bytecode_parse_treet::membert
is_ptr32 : c_qualifierst
is_ptr64 : c_qualifierst
is_ptr_string_struct() : string_abstractiont
is_public : java_bytecode_parse_treet::classt, java_bytecode_parse_treet::membert
is_qualified() : cpp_namet
is_quantified() : qdimacs_cnft
is_read_only_object() : goto_symex_statet
is_ready_to_decide() : single_path_symex_checkert, single_path_symex_only_checkert
is_recursion : framet::loop_infot
is_reference : expr2stlt
is_register : c_storage_spect, cpp_storage_spect
is_restricted : c_qualifierst
is_root : clauset, union_find< T, hasht >, unsigned_union_find
is_root_number() : union_find< T, hasht >
is_root_scope() : cpp_scopet
is_safe_dereference() : local_safe_pointerst
is_same_target() : reachability_slicert
is_same_type() : small_shared_n_way_pointee_baset< N, Num >, small_shared_n_way_ptrt< Ts >
is_sanitizer() : taint_parse_treet::rulet
is_scope : cpp_idt
is_sentinel_dll() : axiomst
is_sentinel_dll_exprs : axiomst
is_set() : optionst
is_set_return_value() : goto_programt::instructiont
is_shareable() : copy_on_write_pointeet< Num >
is_shared() : symbolt
is_shared_read() : goto_trace_stept, SSA_stept
is_shared_write() : goto_trace_stept, SSA_stept
is_signed : bv_spect, constant_interval_exprt
is_simple_name() : cpp_namet
is_single_value_interval() : constant_interval_exprt
is_sink() : taint_parse_treet::rulet
is_skip() : goto_programt::instructiont
is_source() : taint_parse_treet::rulet
is_spawn() : goto_trace_stept, SSA_stept
is_start_thread() : goto_programt::instructiont
is_state_var : symbolt
is_static : c_storage_spect, cpp_storage_spect, java_bytecode_parse_treet::membert
is_static_assert() : cpp_declarationt, cpp_itemt
is_static_class : java_bytecode_parse_treet::classt
is_static_lifetime() : decorated_symbol_exprt, local_bitvector_analysist::flagst, symbolt
is_static_member : cpp_idt
is_storage_class() : mini_c_parsert
is_string() : jsont
is_string_type() : string_instrumentationt
is_subset_of() : c_qualifierst, java_qualifierst
is_success() : main_function_resultt
is_symbol_internal_symbol() : system_library_symbolst
is_synchronized : java_bytecode_parse_treet::methodt
is_synthetic : java_bytecode_parse_treet::classt, java_bytecode_parse_treet::methodt, java_method_typet
is_target() : goto_programt::instructiont
is_template() : cpp_declarationt, cpp_declarator_convertert, new_scopet
is_template_parameter : cpp_declarator_convertert
is_template_scope() : cpp_idt
is_terminal() : consolet
is_thread_local : c_storage_spect, cpp_storage_spect, decorated_symbol_exprt, symbolt
is_threaded : is_threaded_domaint, reaching_definitions_analysist
is_threaded_domaint() : is_threaded_domaint
is_threaded_set : is_threadedt
is_threaded_sett : is_threadedt
is_threadedt() : is_threadedt
is_throw() : goto_programt::instructiont
is_top() : abstract_environmentt, abstract_objectt, ai_domain_baset, constant_interval_exprt, constant_propagator_domaint, constant_propagator_domaint::valuest, context_abstract_objectt, custom_bitvector_domaint, dep_graph_domaint, escape_domaint, global_may_alias_domaint, interval_domaint, interval_templatet< T >, invariant_set_domaint, is_threaded_domaint, rd_range_domaint, uninitialized_domaint, value_set_domain_templatet< VST >, variable_sensitivity_dependence_domaint, variable_sensitivity_domaint
is_top_level_id() : dfcc_cfg_infot
is_top_value() : write_stackt
is_tracked() : escape_domaint, local_bitvector_analysist
is_transparent_union : c_qualifierst
is_true() : bddt, constant_interval_exprt, exprt, guard_bddt, guard_exprt, jsont, literalt, mini_bddt, tvt
is_type() : new_scopet, symbolt
is_type_at_least_as_const_as() : does_remove_constt
is_type_qualifier() : mini_c_parsert
is_typedef : c_storage_spect, cpp_declarationt, cpp_declarator_convertert, cpp_idt
is_typename() : cpp_namet
is_unbounded_array() : arrayst, boolbvt
is_underapproximate() : acceleratet
is_uninitialized() : local_bitvector_analysist::flagst
is_unknown() : local_bitvector_analysist::flagst, range_spect, tvt
is_unknown_handle() : java_bytecode_parse_treet::classt::lambda_method_handlet
is_unsafe() : event_grapht::critical_cyclet
is_unsafe_asm() : event_grapht::critical_cyclet
is_unsafe_fast() : event_grapht::critical_cyclet
is_unsigned() : constant_interval_exprt
is_upper_widened : widened_ranget
is_used : c_storage_spect, postconditiont
is_used_address_of() : postconditiont
is_uses_offset() : local_bitvector_analysist::flagst
is_using() : cpp_itemt
is_valid_bound() : constant_interval_exprt
is_valid_index() : cmdlinet::option_namest::option_names_iteratort
is_valid_loop_id() : dfcc_cfg_infot
is_valid_loop_or_top_level_id() : dfcc_cfg_infot
is_valid_string_constraint() : string_constraintt
is_varargs : java_bytecode_parse_treet::methodt
is_violation : xml_graph_nodet
is_virtual() : cpp_member_spect
is_volatile : c_qualifierst, nondet_volatilet, symbolt
is_weak : c_storage_spect, cpp_storage_spect, symbolt
is_well_formed() : constant_interval_exprt, symbolt
is_writable : __CPROVER_contracts_car_t
is_zero() : bv_arithmetict, bv_utilst, constant_interval_exprt, exprt, fixedbvt, float_bvt, float_utilst, ieee_float_valuet, rationalt
isAllocateExpr() : Parser
isConstructorDecl() : Parser
isfinite() : float_bvt
isfinite_exprt() : isfinite_exprt
isinf() : float_bvt
isinf_exprt() : isinf_exprt
islong : cmdlinet::optiont
isnan() : float_bvt
isnan_exprt() : isnan_exprt
isnormal() : float_bvt
isnormal_exprt() : isnormal_exprt
isolate() : union_find< T, hasht >, unsigned_union_find
isPtrToMember() : Parser
isset() : cmdlinet, cmdlinet::optiont
isTypeSpecifier() : Parser
it : symbol_table_baset::iteratort
italic : messaget
ITEM_NULL : java_bytecode_parse_treet::methodt::verification_type_infot
items : ansi_c_parse_treet, cpp_linkage_spect, cpp_namespace_spect, cpp_parse_treet
itemst : ansi_c_parse_treet, cpp_linkage_spect, cpp_namespace_spect, cpp_parse_treet
iter() : code_fort
iterate() : sharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >
iterations : all_properties_verifier_with_fault_localizationt< incremental_goto_checkerT >, all_properties_verifier_with_trace_storaget< incremental_goto_checkerT >, all_properties_verifiert< incremental_goto_checkerT >, cover_goals_verifier_with_trace_storaget< incremental_goto_checkerT >, cover_goalst, prop_minimizet
iterator : 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, numberingt< keyt, hasht >, range_domaint, union_find< T, hasht >, value_set_fit::object_map_dt
iterator_category : cmdlinet::option_namest::option_names_iteratort, concat_iteratort< first_iteratort, second_iteratort >, dense_integer_mapt< K, V, KeyToDenseInteger >::iterator_templatet< UnderlyingIterator, UnderlyingValue >, depth_iterator_baset< depth_iterator_t >, filter_iteratort< iteratort >, map_iteratort< iteratort, outputt >, symbol_table_baset::iteratort, zip_iteratort< first_iteratort, second_iteratort, same_size >
iterator_count : __CPROVER_jsa_abstract_heap
iterator_templatet() : dense_integer_mapt< K, V, KeyToDenseInteger >::iterator_templatet< UnderlyingIterator, UnderlyingValue >
iterators : __CPROVER_jsa_abstract_heap
iteratort : sparse_vectort< T >, symbol_table_baset::iteratort