- a -
- abs()
: constant_interval_exprt
, float_bvt
, float_utilst
- abs_exprt()
: abs_exprt
- absolute_value()
: bv_utilst
- abstract()
: string_abstractiont
- abstract_arrays()
: acceleration_utilst
- abstract_assign()
: string_abstractiont
- abstract_char_assign()
: string_abstractiont
- abstract_eventt()
: abstract_eventt
- abstract_function_call()
: string_abstractiont
- abstract_pointer_assign()
: string_abstractiont
- abstract_state_after()
: ai_baset
- abstract_state_before()
: ai_baset
, ai_storage_baset
, history_sensitive_storaget
, location_sensitive_storaget
- abstract_traces_after()
: ai_baset
- abstract_traces_before()
: ai_baset
, ai_storage_baset
, trace_map_storaget
- accelerate()
: disjunctive_polynomial_accelerationt
, enumerating_loop_accelerationt
, polynomial_acceleratort
- accelerate_loop()
: acceleratet
- accelerate_loops()
: acceleratet
- accelerate_path()
: acceleratet
- acceleratet()
: acceleratet
- acceleration_utilst()
: acceleration_utilst
- accept_states()
: trace_automatont
- accumulate_overflow()
: overflow_instrumentert
- active_loop_infot()
: framet::active_loop_infot
- add()
: array_list_exprt
, bv_utilst
, call_grapht
, code_blockt
, code_with_references_listt
, cover_goalst
, dep_edget
, destructor_treet
, equation_symbol_mappingt
, float_utilst
, forward_list_as_mapt< keyt, mappedt >
, function_filterst
, goal_filterst
, goto_programt
, guard_bddt
, guard_exprt
, inv_object_storet
, invariant_sett
, irept
, linear_functiont
, method_bytecodet
, multi_namespacet
, polynomialt
, rw_guarded_range_set_value_sett
, rw_range_sett
, shared_bufferst
, sparse_bitvector_analysist< V >
, symbol_table_baset
- add_addr()
: bv_pointerst
- add_all_needed_classes()
: ci_lazy_methods_neededt
- add_anonymous_members_to_scope()
: cpp_typecheckt
- add_approximation()
: bv_refinementt
- add_arbitrary_transition()
: nfat< T >
- add_arg()
: goto_cc_cmdlinet
- add_argument()
: string_abstractiont
- add_array_Ackermann_constraints()
: arrayst
- add_array_constraint()
: arrayst
- add_array_constraints()
: arrayst
- add_array_constraints_array_constant()
: arrayst
- add_array_constraints_array_of()
: arrayst
- add_array_constraints_comprehension()
: arrayst
- add_array_constraints_equality()
: arrayst
- add_array_constraints_if()
: arrayst
- add_array_constraints_update()
: arrayst
- add_array_constraints_with()
: arrayst
- add_array_symbols()
: concurrency_instrumentationt
- add_assertions()
: uninitializedt
- add_assignment()
: gdb_value_extractort
- add_assignments_to_globals()
: memory_snapshot_harness_generatort
- add_axioms_for_char_at()
: string_constraint_generatort
- add_axioms_for_char_literal()
: string_constraint_generatort
- add_axioms_for_characters_in_integer_string()
: string_constraint_generatort
- add_axioms_for_code_point()
: string_constraint_generatort
- add_axioms_for_code_point_at()
: string_constraint_generatort
- add_axioms_for_code_point_before()
: string_constraint_generatort
- add_axioms_for_code_point_count()
: string_constraint_generatort
- add_axioms_for_compare_to()
: string_constraint_generatort
- add_axioms_for_concat()
: string_constraint_generatort
- add_axioms_for_concat_code_point()
: string_constraint_generatort
- add_axioms_for_concat_substr()
: string_constraint_generatort
- add_axioms_for_constant()
: string_constraint_generatort
- add_axioms_for_constrain_characters()
: string_constraint_generatort
- add_axioms_for_contains()
: string_constraint_generatort
- add_axioms_for_copy()
: string_constraint_generatort
- add_axioms_for_cprover_string()
: string_constraint_generatort
- add_axioms_for_delete()
: string_constraint_generatort
- add_axioms_for_delete_char_at()
: string_constraint_generatort
- add_axioms_for_empty_string()
: string_constraint_generatort
- add_axioms_for_equals()
: string_constraint_generatort
- add_axioms_for_equals_ignore_case()
: string_constraint_generatort
- add_axioms_for_fractional_part()
: string_constraint_generatort
- add_axioms_for_function_application()
: string_constraint_generatort
- add_axioms_for_index_of()
: string_constraint_generatort
- add_axioms_for_index_of_string()
: string_constraint_generatort
- add_axioms_for_insert()
: string_constraint_generatort
- add_axioms_for_is_empty()
: string_constraint_generatort
- add_axioms_for_is_prefix()
: string_constraint_generatort
- add_axioms_for_is_suffix()
: string_constraint_generatort
- add_axioms_for_is_valid_int()
: string_constraint_generatort
- add_axioms_for_last_index_of()
: string_constraint_generatort
- add_axioms_for_last_index_of_string()
: string_constraint_generatort
- add_axioms_for_length()
: string_constraint_generatort
- add_axioms_for_offset_by_code_point()
: string_constraint_generatort
- add_axioms_for_parse_int()
: string_constraint_generatort
- add_axioms_for_replace()
: string_constraint_generatort
- add_axioms_for_set_length()
: string_constraint_generatort
- add_axioms_for_string_of_float()
: string_constraint_generatort
- add_axioms_for_string_of_int()
: string_constraint_generatort
- add_axioms_for_string_of_int_with_radix()
: string_constraint_generatort
- add_axioms_for_substring()
: string_constraint_generatort
- add_axioms_for_trim()
: string_constraint_generatort
- add_axioms_from_bool()
: string_constraint_generatort
- add_axioms_from_char()
: string_constraint_generatort
- add_axioms_from_double()
: string_constraint_generatort
- add_axioms_from_float_scientific_notation()
: string_constraint_generatort
- add_axioms_from_int_hex()
: string_constraint_generatort
- add_axioms_from_literal()
: string_constraint_generatort
- add_axioms_from_long()
: string_constraint_generatort
- add_base()
: struct_typet
- add_base_components()
: cpp_typecheckt
- add_bias()
: float_bvt
, float_utilst
- add_bounds()
: invariant_sett
- add_call_with_nondet_arguments()
: memory_snapshot_harness_generatort
- add_case()
: cond_exprt
- add_catch()
: code_try_catcht
- add_child()
: sharing_nodet< keyT, valueT, equalT >
- add_classpath_entry()
: java_class_loader_baset
- add_clinit_call()
: ci_lazy_methods_neededt
- add_com_edge()
: event_grapht
- add_compiler_specific_defines()
: compilet
- add_constraint()
: partial_order_concurrencyt
- add_constraint_from_goals()
: goto_symex_property_decidert
- add_constraint_on_characters()
: string_constraint_generatort
- add_constraints()
: string_dependenciest
- add_constraints_to_prop()
: prop_conv_solvert
- add_contract_check()
: code_contractst
- add_cprover_nondet_initialize_if_it_exists()
: ci_lazy_methods_neededt
- add_created_symbol()
: allocate_objectst
, java_object_factoryt
, symbol_factoryt
- add_decl_dead()
: full_slicert
- add_declarator()
: ansi_c_parsert
, jsil_declarationt
- add_dep()
: dependence_grapht
- add_dependencies()
: full_slicert
- add_dependency()
: string_dependenciest
- add_dirty_checks()
: acceleratet
- add_dstate()
: trace_automatont
- add_dtrans()
: trace_automatont
- add_dummy_symbol_and_value()
: string_abstractiont
- add_edge()
: grapht< N >
- add_epsilon_transition()
: nfat< T >
- add_eq()
: invariant_sett
- add_equality_constraints()
: equalityt
- add_exception_dispatch_sequence()
: remove_exceptionst
- add_existential_quantifier()
: qdimacs_cnft
- add_expr()
: exprt
- add_expr_instrumentation()
: java_bytecode_instrumentt
- add_field()
: java_bytecode_parse_treet::classt
- add_file()
: language_filest
- add_files_from_archive()
: compilet
- add_flag()
: free_form_cmdlinet
- add_fresh_id()
: smt2_parsert
- add_fresh_var()
: shared_bufferst
- add_from_criterion()
: cover_instrumenterst
- add_function()
: dirtyt
, statement_list_parse_treet
, statement_list_parsert
- add_function_block()
: statement_list_parse_treet
, statement_list_parsert
- add_function_calls()
: full_slicert
- add_function_constraints()
: functionst
- add_function_loops()
: path_storaget
- add_guarded_property()
: goto_checkt
- add_harness_function_to_goto_model()
: function_call_harness_generatort::implt
- add_id()
: Parser
- add_implicit_dereference()
: cpp_typecheckt
- add_in()
: graph_nodet< E >
- add_infile_arg()
: goto_cc_cmdlinet
- add_init_section()
: memory_snapshot_harness_generatort
- add_init_writes()
: partial_order_concurrencyt
- add_initialization()
: shared_bufferst
, w_guardst
- add_initialization_code()
: shared_bufferst
- add_initializer()
: ansi_c_declarationt
- add_input_file()
: compilet
- add_instr_to_interleaving()
: instrumentert
- add_instruction()
: goto_programt
, java_bytecode_parse_treet::methodt
, statement_list_parse_treet::networkt
- add_item_if_not_shared()
: sharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >
- add_jar()
: jar_poolt
- add_jumps()
: full_slicert
- add_lambda_method_handle()
: java_class_typet
- add_language_file()
: lazy_goto_modelt
- add_le()
: invariant_sett
- add_lemma()
: string_refinementt
- add_linker_script_definitions()
: linker_script_merget
- add_load_classes()
: java_class_loadert
- add_local_types()
: goto_program2codet
- add_location()
: cpp_parsert
- add_loop_unwind_handler()
: symex_bmct
- add_method()
: java_bytecode_parse_treet::classt
- add_method_body()
: cpp_typecheckt
- add_method_handle()
: java_bytecode_parse_treet::classt
- add_ne()
: invariant_sett
- add_needed_class()
: ci_lazy_methods_neededt
- add_needed_method()
: ci_lazy_methods_neededt
- add_network()
: statement_list_parse_treet::tia_modulet
- add_node()
: event_grapht
, grapht< N >
- add_node_if_not_exists()
: graphmlt
- add_object()
: cpp_typecheck_fargst
, goto_symex_statet
, pointer_logict
- add_objective()
: bv_minimizet
- add_objects()
: invariant_propagationt
- add_option()
: free_form_cmdlinet
- add_out()
: graph_nodet< E >
- add_over_assumption()
: bv_refinementt::approximationt
- add_overflow_checks()
: overflow_instrumentert
- add_path()
: trace_automatont
- add_po_back_edge()
: event_grapht
- add_po_edge()
: event_grapht
- add_pointer_checks()
: code_contractst
- add_pragma()
: source_locationt
- add_prefix()
: jsil_typecheckt
- add_quantifier()
: qbf_squolem_coret
, qbf_squolemt
, qdimacs_cnft
- add_recursion_unwind_handler()
: symex_bmct
- add_reference()
: mini_bdd_nodet
- add_return()
: goto_convert_functionst
- add_returns()
: jsil_declarationt
- add_rounding_mode()
: c_typecheck_baset
- add_secondary_scope()
: cpp_scopet
- add_segment()
: goto_inlinet::goto_inline_logt
- add_source_location()
: cpp_namet::namet
, exprt
, typet
- add_state()
: automatont
- add_step()
: goto_tracet
- add_str_arguments()
: string_abstractiont
- add_string_type()
: java_string_library_preprocesst
- add_sub()
: bv_utilst
, float_bvt
, float_utilst
- add_sub_no_overflow()
: bv_utilst
- add_tag_list()
: statement_list_parsert
- add_tag_with_body()
: ansi_c_parsert
- add_temp_rlo()
: statement_list_typecheckt
- add_this_to_method_type()
: cpp_typecheckt
- add_throws()
: jsil_declarationt
- add_throws_exception()
: java_method_typet
- add_to_front()
: code_with_references_listt
- add_to_offset()
: pointer_arithmetict
- add_to_operands()
: exprt
- add_to_or_rlo_wrapper()
: statement_list_typecheckt
- add_to_queue()
: full_slicert
- add_to_system_library()
: system_library_symbolst
- add_token()
: assembler_parsert
, statement_list_parse_treet::instructiont
- add_trans()
: automatont
- add_transition()
: nfat< T >
- add_type()
: typet
- add_type_bounds()
: invariant_sett
- add_under_assumption()
: bv_refinementt::approximationt
- add_undirected_com_edge()
: event_grapht
- add_undirected_edge()
: grapht< N >
- add_unique_id()
: smt2_parsert
- add_universal_quantifier()
: qdimacs_cnft
- add_unknown_lambda_method_handle()
: java_class_typet
- add_using_scope()
: cpp_scopet
- add_value()
: jsil_declarationt
- add_var()
: value_set_fit
, value_set_fivrnst
, value_set_fivrt
- add_var_constant_entry()
: statement_list_parse_treet::tia_modulet
- add_var_inout_entry()
: statement_list_parse_treet::tia_modulet
- add_var_input_entry()
: statement_list_parse_treet::tia_modulet
- add_var_output_entry()
: statement_list_parse_treet::tia_modulet
- add_var_static_entry()
: statement_list_parse_treet::function_blockt
- add_var_temp_entry()
: statement_list_parse_treet::tia_modulet
- add_variable()
: mathematical_function_typet
- add_variables()
: satcheck_glucose_baset< T >
, satcheck_minisat1_baset
, satcheck_minisat2_baset< T >
- add_vars()
: value_set_analysis_fit
, value_set_analysis_fivrnst
, value_set_analysis_fivrt
, value_set_fit
, value_set_fivrnst
, value_set_fivrt
- add_written_cprover_symbols()
: compilet
- adder()
: bv_utilst
- adder_no_overflow()
: bv_utilst
- address()
: partial_order_concurrencyt
- address2size_t()
: gdb_value_extractort::memory_scopet
- address_arithmetic()
: goto_symext
- address_check()
: goto_checkt
- address_of_exprt()
: address_of_exprt
- address_to_object_record()
: interpretert
- address_to_offset()
: interpretert
- address_to_symbol()
: interpretert
- adjust()
: bv_arithmetict
- adjust_assign_rhs_values()
: value_sett
- adjust_float_rel()
: c_typecheck_baset
- adjust_function_parameter()
: c_typecheck_baset
- adjust_object_type()
: linkingt
- adjust_object_type_rec()
: linkingt
- adjust_type_infot()
: linkingt::adjust_type_infot
- advance()
: dense_integer_mapt< K, V, KeyToDenseInteger >::iterator_templatet< UnderlyingIterator, UnderlyingValue >
- advance_column()
: parsert
- affected_by_delay()
: shared_bufferst
- aggressive_slicert()
: aggressive_slicert
- ahistoricalt()
: ahistoricalt
- ai_baset()
: ai_baset
- ai_domain_baset()
: ai_domain_baset
- ai_history_baset()
: ai_history_baset
- ai_recursive_interproceduralt()
: ai_recursive_interproceduralt
- ai_simplify()
: ai_domain_baset
, constant_propagator_domaint
, interval_domaint
- ai_simplify_lhs()
: ai_domain_baset
- ai_storage_baset()
: ai_storage_baset
- ait()
: ait< domainT >
- alias()
: cpp_namespace_spect
- aliases()
: custom_bitvector_analysist
, local_may_aliast
- align()
: ieee_floatt
- all()
: goto_trace_storaget
- all_cycles_in_lexical_loop_form()
: lexical_loops_templatet< P, T >
- all_integers()
: interval_uniont
- all_paths_enumeratort()
: all_paths_enumeratort
- all_properties_verifier_with_fault_localizationt()
: all_properties_verifier_with_fault_localizationt< incremental_goto_checkerT >
- all_properties_verifier_with_trace_storaget()
: all_properties_verifier_with_trace_storaget< incremental_goto_checkerT >
- all_properties_verifiert()
: all_properties_verifiert< incremental_goto_checkerT >
- allocate()
: interpretert
, small_mapt< T, Ind, Num >
- allocate_automatic_local_object()
: allocate_objectst
- allocate_dynamic_object()
: allocate_objectst
- allocate_dynamic_object_symbol()
: allocate_objectst
- allocate_fresh_string()
: java_string_library_preprocesst
- allocate_non_dynamic_object()
: allocate_objectst
- allocate_object()
: allocate_objectst
- allocate_objectst()
: allocate_objectst
- allocate_static_global_object()
: allocate_objectst
- already_typechecked_exprt()
: already_typechecked_exprt
- already_typechecked_typet()
: already_typechecked_typet
- analysis_exceptiont()
: analysis_exceptiont
- analyze_symbol()
: gdb_value_extractort
- analyze_symbols()
: gdb_value_extractort
- ancestry_resultt()
: ancestry_resultt
- and_exprt()
: and_exprt
- ansi_c_convert_typet()
: ansi_c_convert_typet
- ansi_c_declarationt()
: ansi_c_declarationt
- ansi_c_declaratort()
: ansi_c_declaratort
- ansi_c_identifiert()
: ansi_c_identifiert
- ansi_c_languaget()
: ansi_c_languaget
- ansi_c_parsert()
: ansi_c_parsert
- ansi_c_scopet()
: ansi_c_scopet
- ansi_c_typecheckt()
: ansi_c_typecheckt
- APP_non_rec()
: mini_bdd_applyt
- APP_rec()
: mini_bdd_applyt
- append()
: code_blockt
, code_with_references_listt
, guard_bddt
, guard_exprt
, scratch_programt
- append_loop()
: scratch_programt
- append_multiply_expression()
: constant_interval_exprt
- append_multiply_expression_max()
: constant_interval_exprt
- append_multiply_expression_min()
: constant_interval_exprt
- append_path()
: scratch_programt
- apply()
: expr_skeletont
, field_sensitivityt
, goto_programt::instructiont
, template_mapt
- apply_asm_label()
: c_typecheck_baset
- apply_assign_side_effects()
: value_sett
- apply_code()
: invariant_sett
, value_set_fit
, value_set_fivrnst
, value_set_fivrt
, value_sett
- apply_code_rec()
: value_sett
- apply_condition()
: goto_statet
- apply_contract()
: code_contractst
- apply_goto_condition()
: goto_symext
- apply_template_args()
: cpp_typecheck_resolvet
- approx_union_with()
: interval_templatet< T >
- approximationt()
: bv_refinementt::approximationt
- are_loop_children_too_complicated()
: complexity_limitert
- are_po_ordered()
: event_grapht
- arg()
: array_comprehension_exprt
- arg_is_type_compatible()
: remove_function_pointerst
- argt()
: goto_cc_cmdlinet::argt
- arguments()
: code_function_callt
, cpp_template_args_baset
, function_application_exprt
, side_effect_expr_function_callt
- arguments_equal()
: functionst
- armcc_cmdlinet()
: armcc_cmdlinet
- armcc_modet()
: armcc_modet
- array()
: index_exprt
- array_assignments2polys()
: acceleration_utilst
, polynomial_acceleratort
- array_comprehension_exprt()
: array_comprehension_exprt
- array_exprt()
: array_exprt
- array_list_exprt()
: array_list_exprt
- array_name()
: goto_checkt
- array_of_exprt()
: array_of_exprt
- array_poolt()
: array_poolt
- array_typet()
: array_typet
- arrays_overapproximated()
: bv_refinementt
- arrayst()
: arrayst
- as()
: expr_queryt< T >
- as86_cmdlinet()
: as86_cmdlinet
- as_cmdlinet()
: as_cmdlinet
- as_expr()
: bdd_exprt
, cpp_namet
, goto_symex_property_decidert::goalt
, guard_bddt
, guard_exprt
- as_hybrid_binary()
: as_modet
- as_modet()
: as_modet
- as_singleton()
: interval_uniont
- as_string()
: bv_refinementt::approximationt
, c_qualifierst
, dstringt
, identifiert
, java_qualifierst
, printf_formattert
, qualifierst
, source_locationt
- as_string_with_cwd()
: source_locationt
- as_type()
: cpp_namet
- ashr_exprt()
: ashr_exprt
- asm_output()
: gcc_modet
- asm_text()
: code_asm_gcct
- assembler_parsert()
: assembler_parsert
- assert_for_values()
: disjunctive_polynomial_accelerationt
, polynomial_acceleratort
- assertion()
: code_assertt
, symex_target_equationt
, symex_targett
- assign()
: _rw_set_loct
, interpretert
, interval_domaint
, scratch_programt
, uninitialized_domaint
, value_set_fit
, value_set_fivrnst
, value_set_fivrt
, value_sett
- assign_array()
: acceleration_utilst
, symex_assignt
- assign_byte_extract()
: symex_assignt
- assign_element()
: java_object_factoryt
- assign_from()
: messaget::mstreamt
- assign_from_struct()
: symex_assignt
- assign_if()
: symex_assignt
- assign_lhs()
: custom_bitvector_domaint
, local_bitvector_analysist
, local_may_aliast
- assign_lhs_aliases()
: escape_domaint
, global_may_alias_domaint
- assign_lhs_cleanup()
: escape_domaint
- assign_non_struct_symbol()
: symex_assignt
- assign_rec()
: constant_propagator_domaint
, symex_assignt
, value_set_fit
, value_set_fivrnst
, value_set_fivrt
, value_sett
- assign_string_constant()
: goto_symext
- assign_struct_member()
: symex_assignt
- assign_struct_rec()
: custom_bitvector_domaint
- assign_symbol()
: symex_assignt
- assign_typecast()
: symex_assignt
- assignment()
: goto_symex_statet
, invariant_sett
, shared_bufferst
, symex_target_equationt
, symex_targett
- associate_array_to_pointer()
: goto_symext
, string_constraint_generatort
- associate_length_to_array()
: string_constraint_generatort
- assume()
: interval_domaint
, scratch_programt
- assume_rec()
: interval_domaint
- assumption()
: code_assumet
, symex_target_equationt
, symex_targett
- at()
: cfg_baset< T, P, I >::entry_mapt
, dense_integer_mapt< K, V, KeyToDenseInteger >
, fixed_keys_map_wrappert< mapt >
, interval_sparse_arrayt
, lazy_goto_functions_mapt
, template_numberingt< Map >
- atomic_begin()
: symex_target_equationt
, symex_targett
- atomic_end()
: symex_target_equationt
, symex_targett
- automatic()
: format_spect
- automatont()
: automatont
- auxiliary_symbolt()
: auxiliary_symbolt