- 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 , cpp_typecheck_resolvet::matcht , datat , event_grapht::critical_cyclet , interpretert::function_assignmentt , new_scopet , object_idt , operator_entryt , saj_tablet , taint_parse_treet::rulet
id2cycloc : instrumentert
id2loc : instrumentert
id_class : ansi_c_identifiert , cpp_idt
id_map : cpp_scopest , new_scopet , smt2_parsert
id_maps : java_string_library_preprocesst
ID_nondet_padding : nondet_padding_exprt
id_nr : bv_refinementt::approximationt
id_r : mm_iot
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 , value_set_fit::entryt , value_sett::entryt
identifier_map : smt2_convt
identifier_table : smt2_incremental_decision_proceduret
identifiers : sorted_variablest
identity : goto_check_ct
idx : small_mapt< T, Ind, Num >::const_iterator
if_then_else : smt_core_theoryt
ignore : SSA_stept
ignore_arrays : event_grapht
ignore_assertions : goto_symext
ignore_manifest_main_class : java_bytecode_language_optionst
ii : small_mapt< T, Ind, Num >::const_iterator , small_mapt< T, Ind, Num >::const_value_iterator
impact_mode : change_impactt
implementation : api_sessiont
implements : java_bytecode_parse_treet::classt
implications : framet
implies : smt_core_theoryt
in : cscannert , elf_readert , graph_nodet< E > , osx_mach_o_readert , parsert , preprocessort , smt2_tokenizert
in_core : satcheck_minisat1_coret , satcheck_zcoret
in_file : goto_harness_parse_optionst::goto_harness_configt
in_invariant_clause_map : enumerative_loop_contracts_synthesizert
in_pos : instrumentert::cfg_visitort
in_progress : language_modulet
in_scc : grapht< N >::tarjant
in_use : cpp_typecheck_fargst
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_struct_padding_components : expr2c_configurationt
include_typedefs : dump_c_configurationt
included_prefixes : prefix_filtert
includes : c_wranglert
incoming : state_encodingt
incoming_edges : goto_programt::instructiont
incr_loop_id : symex_bmc_incremental_one_loopt
incr_max_unwind : symex_bmc_incremental_one_loopt
incr_min_unwind : symex_bmc_incremental_one_loopt
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 >
IND : small_mapt< T, Ind, Num >
ind : small_mapt< T, Ind, Num >
indent : json_streamt
index : __CPROVER_jsa_iterator , acceleration_utilst::polynomial_array_assignmentt , check_call_sequencet::statet , cmdlinet::option_namest::option_names_iteratort , designatort::entryt , format_specifiert , frame_reft , 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
index_list : designatort
index_map : arrayst
index_sequence : smt2_incremental_decision_proceduret
index_sets : string_refinementt
index_to_bdd : bdd_managert
index_to_block : cover_basic_blocks_javat
index_type : java_string_library_preprocesst
indexed_by_object_id : __CPROVER_contracts_obj_set_t
infinity : float_bvt::unpacked_floatt , float_utilst::unpacked_floatt
infinity_flag : ieee_floatt
init_state : automatont
initial_equation_generated : single_loop_incremental_symex_checkert
initial_goto_location_line : memory_snapshot_harness_generatort
initial_source_location_line : memory_snapshot_harness_generatort
initial_state_exprs : axiomst
initialization : string_abstractiont
initialization_config : recursive_initializationt
initialized : dirtyt , flow_insensitive_analysis_baset , interpretert::memory_cellt , lazy_class_to_declared_symbols_mapt
initializer : c_declarationt
inline_log : goto_inlinet
inlined : dfcc_libraryt
inner_loops : dfcc_loop_infot
inner_name : java_bytecode_parse_treet::classt
input : string_transformation_builtin_functiont
input1 : string_insertion_builtin_functiont
input2 : string_insertion_builtin_functiont
input_vars : interpretert
inputs : string_format_builtin_functiont
inserted : journalling_symbol_tablet , memory_snapshot_harness_generatort::preordert< Key >
inside_bit_string : expr2stlt
instance_count : statement_list_parsert , xml_parsert
instances : goto_symex_property_decidert::goalt
instantiated_classes : ci_lazy_methods_neededt
instantiation_stack : cpp_typecheckt::instantiation_levelt , cpp_typecheckt , cpp_typecheckt::method_bodyt
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
instructions : assembler_parsert , dfcc_loop_nesting_graph_nodet , goto_programt , java_bytecode_parse_treet::methodt , statement_list_parse_treet::networkt
instrument : dfcc_contract_functionst , dfcc_contract_handlert , dfcc_lift_memory_predicatest , dfcc_swap_and_wrapt , dfcc_wrapper_programt , dfcct
instrument_loop : dfcc_instrumentt
instrumentations : shared_bufferst
instrumenter : instrumentert::cfg_visitort
instrumenters : cover_instrumenterst
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_width : configt::ansi_ct
integer_bits : fixedbv_spect
internal : goto_trace_stept
internal_symbol_base_map : symbol_tablet
internal_symbol_module_map : symbol_tablet
internal_symbols : dfcc_instrumentt , symbol_tablet
interval : interval_abstract_valuet , interval_index_ranget
intervals : interval_uniont
invalid_object : pointer_logict
invariant : dfcc_loop_infot , workt , xml_graph_nodet
invariant_candidates : cegis_verifiert
invariant_expr : contract_clausest
invariant_propagationt : location_sensitive_storaget
invariant_scope : xml_graph_nodet
invariant_set : invariant_set_domaint
invariant_set_domain_factoryt : invariant_propagationt
invariants : framet , loop_contracts_clauset
invariants_set : framet
inverse_memory_map : interpretert
io_args : goto_trace_stept , SSA_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_full_hash_container : irep_serializationt::ireps_containert
irep_store : merge_full_irept , merge_irept
ireps_container : irep_serializationt
ireps_on_read : irep_serializationt::ireps_containert
ireps_on_write : irep_serializationt::ireps_containert
is_a_tty : console_message_handlert
is_abstract : class_hierarchyt::entryt , java_bytecode_parse_treet::classt , java_bytecode_parse_treet::methodt
is_always_simplified : guard_bddt , guard_exprt
is_annotation : java_bytecode_parse_treet::classt
is_anonymous_class : java_bytecode_parse_treet::classt
is_atomic : c_qualifierst
is_auxiliary : symbolt
is_bottom : constant_propagator_domaint::valuest
is_bound : smt2_convt::identifiert
is_bridge : java_bytecode_parse_treet::methodt
is_code : cpp_declarator_convertert
is_constant : c_qualifierst , havoc_utilst , inv_object_storet::entryt
is_constructor : cpp_idt
is_cstring_exprs : axiomst
is_decimal : parse_floatt
is_dirty : function_cfg_infot , loop_cfg_infot , reaching_definitions_analysist
is_dynamic : decision_procedure_objectt
is_dynamic_object_exprs : axiomst
is_dynamic_object_function : smt2_incremental_decision_proceduret
is_empty : __CPROVER_contracts_obj_set_t
is_enum : java_bytecode_parse_treet::classt , java_bytecode_parse_treet::fieldt
is_exchangeable : binary_functional_enumeratort
is_exported : symbolt
is_extern : c_storage_spect , symbolt
is_false : invariant_sett
is_file_local : symbolt
is_final : java_bytecode_parse_treet::classt , java_bytecode_parse_treet::membert
is_float : 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_fresh_set : dfcc_wrapper_programt
is_friend : cpp_declarator_convertert
is_good : eval_index_resultt
is_good_partition : non_leaf_enumeratort
is_imaginary : parse_floatt
is_infile_name : goto_cc_cmdlinet::argt
is_inline : c_storage_spect
is_inner_class : java_bytecode_parse_treet::classt
is_input : symbolt
is_interface : java_bytecode_parse_treet::classt
is_long : parse_floatt
is_lower_widened : widened_ranget
is_lvalue : symbolt
is_macro : symbolt
is_member : cpp_idt
is_method : cpp_idt
is_native : java_bytecode_parse_treet::methodt
is_nodiscard : c_qualifierst
is_nondet : nondet_instruction_infot
is_noreturn : c_qualifierst
is_nullable : nondet_instruction_infot , recursive_initializationt::constructor_keyt
is_object_bits_default : configt::bv_encodingt
is_output : symbolt
is_parameter : java_bytecode_convert_methodt::local_variable_with_holest , java_bytecode_convert_methodt::variablet , symbolt
is_po : event_grapht::critical_cyclet::delayt
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_public : java_bytecode_parse_treet::classt , java_bytecode_parse_treet::membert
is_recursion : framet::loop_infot
is_reference : expr2stlt
is_register : c_storage_spect
is_restricted : c_qualifierst
is_root : clauset
is_scope : cpp_idt
is_sentinel_dll_exprs : axiomst
is_signed : bv_spect
is_state_var : symbolt
is_static : c_storage_spect , java_bytecode_parse_treet::membert
is_static_class : java_bytecode_parse_treet::classt
is_static_lifetime : symbolt
is_static_member : cpp_idt
is_synchronized : java_bytecode_parse_treet::methodt
is_synthetic : java_bytecode_parse_treet::classt , java_bytecode_parse_treet::methodt
is_template : cpp_declarator_convertert
is_template_parameter : cpp_declarator_convertert
is_thread_local : c_storage_spect , symbolt
is_threaded : is_threaded_domaint , reaching_definitions_analysist
is_threaded_set : is_threadedt
is_transparent_union : c_qualifierst
is_type : symbolt
is_typedef : c_storage_spect , cpp_declarator_convertert
is_upper_widened : widened_ranget
is_used : c_storage_spect
is_varargs : java_bytecode_parse_treet::methodt
is_violation : xml_graph_nodet
is_volatile : c_qualifierst , symbolt
is_weak : c_storage_spect , symbolt
is_writable : __CPROVER_contracts_car_t
islong : cmdlinet::optiont
isset : cmdlinet::optiont
it : symbol_table_baset::iteratort
italic : messaget
items : ansi_c_parse_treet , cpp_parse_treet
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 >
iterator_count : __CPROVER_jsa_abstract_heap
iterators : __CPROVER_jsa_abstract_heap