cprover
|
Base class for tree-like data structures with sharing. More...
#include <irep.h>
Classes | |
class | dt |
Public Types | |
typedef std::vector< irept > | subt |
typedef std::map< irep_namet, irept > | named_subt |
Public Member Functions | |
bool | is_nil () const |
bool | is_not_nil () const |
irept (const irep_idt &_id) | |
irept () | |
irept (const irept &irep) | |
irept (irept &&irep) | |
irept & | operator= (const irept &irep) |
irept & | operator= (irept &&irep) |
~irept () | |
const irep_idt & | id () const |
const std::string & | id_string () const |
void | id (const irep_idt &_data) |
const irept & | find (const irep_namet &name) const |
irept & | add (const irep_namet &name) |
irept & | add (const irep_namet &name, const irept &irep) |
const std::string & | get_string (const irep_namet &name) const |
const irep_idt & | get (const irep_namet &name) const |
bool | get_bool (const irep_namet &name) const |
signed int | get_int (const irep_namet &name) const |
unsigned int | get_unsigned_int (const irep_namet &name) const |
std::size_t | get_size_t (const irep_namet &name) const |
long long | get_long_long (const irep_namet &name) const |
void | set (const irep_namet &name, const irep_idt &value) |
void | set (const irep_namet &name, const irept &irep) |
void | set (const irep_namet &name, const long long value) |
void | remove (const irep_namet &name) |
void | move_to_sub (irept &irep) |
void | move_to_named_sub (const irep_namet &name, irept &irep) |
bool | operator== (const irept &other) const |
bool | operator!= (const irept &other) const |
void | swap (irept &irep) |
bool | operator< (const irept &other) const |
defines ordering on the internal representation More... | |
bool | ordering (const irept &other) const |
defines ordering on the internal representation More... | |
int | compare (const irept &i) const |
defines ordering on the internal representation More... | |
void | clear () |
void | make_nil () |
subt & | get_sub () |
const subt & | get_sub () const |
named_subt & | get_named_sub () |
const named_subt & | get_named_sub () const |
named_subt & | get_comments () |
const named_subt & | get_comments () const |
std::size_t | hash () const |
std::size_t | full_hash () const |
bool | full_eq (const irept &other) const |
std::string | pretty (unsigned indent=0, unsigned max_indent=0) const |
const dt & | read () const |
dt & | write () |
Protected Member Functions | |
void | detach () |
Static Protected Member Functions | |
static bool | is_comment (const irep_namet &name) |
static void | remove_ref (dt *old_data) |
static void | nonrecursive_destructor (dt *old_data) |
Does the same as remove_ref, but using an explicit stack instead of recursion. More... | |
Protected Attributes | |
dt * | data |
Static Protected Attributes | |
static dt | empty_d |
typedef std::map<irep_namet, irept> irept::named_subt |
typedef std::vector<irept> irept::subt |
|
inlineexplicit |
|
inline |
Definition at line 115 of file irep.h.
Referenced by clear(), and code_push_catcht::code_push_catcht().
|
inline |
|
inline |
Definition at line 178 of file irep.h.
References remove_ref().
irept & irept::add | ( | const irep_namet & | name | ) |
Definition at line 306 of file irep.cpp.
References get_comments(), get_named_sub(), and is_comment().
Referenced by c_typecheck_baset::add_argc_argv(), jsil_declarationt::add_declarator(), exprt::add_expr(), jsil_declarationt::add_returns(), cpp_namet::namet::add_source_location(), typet::add_source_location(), exprt::add_source_location(), jsil_declarationt::add_throws(), typet::add_type(), jsil_declarationt::add_value(), cpp_namespace_spect::alias(), template_mapt::apply(), cpp_template_args_baset::arguments(), class_typet::bases(), cpp_enum_typet::body(), cpp_typecheckt::clean_up(), code_typet::code_typet(), struct_union_typet::components(), cpp_typecheckt::convert_anonymous_union(), cpp_typecheckt::convert_class_template_specialization(), dump_ct::convert_compound_enum(), convert_decl(), json_irept::convert_from_json(), cpp_typecheckt::convert_initializer(), expr2cppt::convert_rec(), copy_array(), copy_member(), cpp_typecheckt::cpp_constructor(), cpp_typecheckt::cpp_destructor(), cpp_namespace_spect::cpp_namespace_spect(), jsil_declarationt::declarator(), template_parametert::default_argument(), cpp_typecheckt::default_assignop(), cpp_typecheckt::default_cpctor(), cpp_typecheckt::default_ctor(), cpp_typecheckt::default_dtor(), enumeration_typet::elements(), exprt::exprt(), cpp_typecheckt::full_member_initialization(), java_generic_typet::generic_type_arguments(), java_generic_class_typet::generic_types(), java_generic_symbol_typet::generic_types(), annotated_typet::get_annotations(), java_implicitly_generic_class_typet::implicit_generic_types(), cpp_declaratort::init_args(), cpp_typecheckt::instantiate_template(), goto_symex_statet::l2_thread_read_encoding(), java_class_typet::lambda_method_handles(), cpp_linkage_spect::linkage(), cpp_storage_spect::location(), boolbvt::make_bv_expr(), code_typet::make_ellipsis(), java_string_library_preprocesst::make_string_format_code(), cpp_declaratort::member_initializers(), cpp_declarationt::member_spec(), cpp_declaratort::method_qualifier(), class_typet::methods(), move_to_named_sub(), cpp_usingt::name(), cpp_declaratort::name(), cpp_typecheckt::new_temporary(), dump_ct::operator()(), cpp_typecheckt::operator_is_overloaded(), Parser::optIntegralTypeOrClassSpec(), code_typet::parameters(), cpp_declarationt::partial_specialization_args(), Parser::rAlignofExpr(), Parser::rAllocateExpr(), Parser::rAttribute(), Parser::rBaseSpecifiers(), Parser::rClassSpec(), Parser::rConstructorDecl(), Parser::rDeclarator(), cpp_convert_typet::read_function_type(), irep_serializationt::read_irep(), cpp_convert_typet::read_template(), cpp_typecheckt::reference_binding(), code_typet::remove_ellipsis(), rename_symbolt::rename(), Parser::rEnumBody(), Parser::rEnumSpec(), replace_symbolt::replace(), Parser::rMemberInit(), Parser::rMSCuuidof(), Parser::rName(), Parser::rPostfixExpr(), Parser::rPtrToMember(), Parser::rSizeofExpr(), Parser::rTemplateDecl(), Parser::rTemplateDecl2(), Parser::rTypePredicate(), set(), Parser::set_location(), array_typet::size(), vector_typet::size(), ssa_exprt::ssa_exprt(), cpp_typecheckt::static_and_dynamic_initialization(), cpp_typecheckt::static_typecast(), cpp_declarationt::storage_spec(), cpp_enum_typet::tag(), template_typet::template_parameters(), cpp_declarationt::template_type(), cpp_declaratort::throw_decl(), exprt::type(), mathematical_function_typet::variablet::type(), java_generic_parametert::type_variables(), c_typecheck_baset::typecheck_c_bit_field_type(), c_typecheck_baset::typecheck_c_enum_tag_type(), c_typecheck_baset::typecheck_c_enum_type(), cpp_typecheckt::typecheck_class_template_member(), cpp_typecheckt::typecheck_compound_bases(), cpp_typecheckt::typecheck_compound_declarator(), c_typecheck_baset::typecheck_declaration(), cpp_typecheckt::typecheck_enum_body(), cpp_typecheckt::typecheck_expr_address_of(), c_typecheck_baset::typecheck_expr_alignof(), c_typecheck_baset::typecheck_expr_builtin_offsetof(), cpp_typecheckt::typecheck_expr_cpp_name(), c_typecheck_baset::typecheck_expr_cw_va_arg_typeof(), c_typecheck_baset::typecheck_expr_main(), cpp_typecheckt::typecheck_expr_new(), jsil_typecheckt::typecheck_expr_side_effect_throw(), c_typecheck_baset::typecheck_expr_sizeof(), cpp_typecheckt::typecheck_friend_declaration(), c_typecheck_baset::typecheck_side_effect_function_call(), cpp_typecheckt::typecheck_side_effect_function_call(), c_typecheck_baset::typecheck_spec_expr(), cpp_typecheckt::typecheck_template_parameters(), c_typecheck_baset::typecheck_type(), cpp_typecheckt::typecheck_type(), ssa_exprt::update_type(), cpp_typecheckt::user_defined_conversion_sequence(), ansi_c_declaratort::value(), cpp_declaratort::value(), and jsil_declarationt::value().
irept & irept::add | ( | const irep_namet & | name, |
const irept & | irep | ||
) |
Definition at line 324 of file irep.cpp.
References get_comments(), get_named_sub(), and is_comment().
|
inline |
Definition at line 241 of file irep.h.
References irept().
Referenced by mm_parsert::clear(), parsert::clear(), goto_functiont::clear(), messaget::eom(), move_to_named_sub(), Parser::operator()(), Parser::optMemberSpec(), Parser::rAllocateInitializer(), Parser::rArgDeclList(), Parser::rDeclarator(), irep_serializationt::read_irep(), Parser::rEnumBody(), cpp_convert_typet::write(), and ansi_c_convert_typet::write().
int irept::compare | ( | const irept & | i | ) | const |
defines ordering on the internal representation
Definition at line 498 of file irep.cpp.
References dstringt::compare(), get_named_sub(), get_sub(), id(), INVARIANT, r, and size_type().
Referenced by ordering().
|
protected |
Definition at line 64 of file irep.cpp.
References empty_d, POSTCONDITION, and remove_ref().
Referenced by move_to_named_sub(), move_to_sub(), and write().
const irept & irept::find | ( | const irep_namet & | name | ) | const |
Definition at line 285 of file irep.cpp.
References find(), get_comments(), get_named_sub(), get_nil_irep(), and is_comment().
Referenced by cpp_typecheckt::add_base_components(), add_padding_gcc(), add_to_json(), cpp_namespace_spect::alias(), alignment(), code_contractst::apply_contract(), cpp_template_args_baset::arguments(), class_typet::bases(), cpp_enum_typet::body(), goto_checkt::bounds_check(), string_abstractiont::build_abstraction_type_rec(), build_sizeof_expr(), c_sizeof_type_rec(), cpp_typecheckt::check_component_access(), cpp_typecheckt::check_member_initializers(), cpp_typecheckt::class_template_symbol(), clean_identifier(), goto_program2codet::cleanup_expr(), cpp_declarator_convertert::combine_types(), struct_union_typet::components(), interpretert::concretize_type(), cpp_declarator_convertert::convert(), boolbvt::convert_bv_literals(), dump_ct::convert_compound(), dump_ct::convert_compound_enum(), expr2ct::convert_constant(), goto_convertt::convert_cpp_delete(), expr2cppt::convert_cpp_new(), convert_decl(), expr2ct::convert_Hoare(), cpp_typecheckt::convert_initializer(), expr2javat::convert_java_new(), goto_convertt::convert_loop_invariant(), cpp_typecheckt::convert_non_template_declaration(), cpp_typecheckt::convert_pmop(), expr2ct::convert_pointer_object_has_type(), expr2ct::convert_rec(), expr2cppt::convert_rec(), expr2ct::convert_sizeof(), convert_string_literal(), cpp_typecheckt::convert_template_declaration(), cpp_typecheckt::cpp_constructor(), cpp_typecheckt::cpp_destructor(), cpp_exception_list_rec(), cpp_typecheckt::cpp_is_pod(), goto_convertt::cpp_new_initializer(), jsil_declarationt::declarator(), template_parametert::default_argument(), cpp_typecheckt::default_assignop_value(), cpp_typecheckt::default_cpctor(), goto_convertt::do_cpp_new(), c_typecheck_baset::do_designated_initializer(), cpp_typecheckt::dtor(), cpp_typecheckt::dynamic_typecast(), cpp_typecheckt::elaborate_class_template(), enumeration_typet::elements(), code_blockt::end_location(), code_push_catcht::exception_list(), find(), cpp_typecheckt::find_dtor(), exprt::find_expr(), cpp_typecheckt::find_parent(), find_symbols(), typet::find_type(), cpp_typecheckt::full_member_initialization(), java_object_factoryt::gen_nondet_array_init(), java_generic_typet::generic_type_arguments(), java_generic_class_typet::generic_types(), java_generic_symbol_typet::generic_types(), annotated_typet::get_annotations(), cpp_typecheckt::get_bases(), java_bytecode_parsert::get_class_refs_rec(), get_destructor(), java_bytecode_convert_methodt::get_or_create_block_for_pcrange(), ssa_exprt::get_original_expr(), cpp_declarator_convertert::get_pretty_name(), interpretert::get_size(), java_annotationt::get_type(), interpretert::get_value(), value_set_fit::get_value_set_rec(), value_sett::get_value_set_rec(), cpp_typecheckt::get_virtual_bases(), cpp_typecheck_resolvet::guess_function_template_args(), cpp_enum_typet::has_body(), template_parametert::has_default_argument(), code_typet::has_ellipsis(), cpp_enum_typet::has_tag(), rename_symbolt::have_to_rename(), replace_symbolt::have_to_replace(), java_implicitly_generic_class_typet::implicit_generic_types(), cpp_declaratort::init_args(), cpp_typecheckt::instantiate_template(), java_class_typet::lambda_method_handles(), cpp_linkage_spect::linkage(), list_calls_and_arguments(), cpp_storage_spect::location(), remove_java_newt::lower_java_new_array(), linker_script_merget::ls_data2instructions(), cpp_typecheck_resolvet::make_constructors(), cpp_declaratort::member_initializers(), cpp_declarationt::member_spec(), c_enum_typet::members(), constant_propagator_domaint::valuest::merge(), cpp_declaratort::method_qualifier(), class_typet::methods(), cpp_typecheckt::move_member_initializers(), cpp_usingt::name(), cpp_declaratort::name(), cpp_declarationt::name_anon_struct_union(), dump_ct::operator()(), class_hierarchyt::operator()(), jsil_declarationt::output(), goto_programt::output_instruction(), code_typet::parameters(), symex_slice_by_tracet::parse_events(), parse_loop_ids(), cpp_declarationt::partial_specialization_args(), cpp_typecheckt::put_compound_into_scope(), Parser::rClassSpec(), ansi_c_convert_typet::read_rec(), cpp_typecheckt::reference_binding(), goto_convertt::remove_cpp_delete(), goto_convertt::remove_side_effect(), goto_convertt::remove_temporary_object(), replace_symbolt::replace(), replace_location(), jsil_declarationt::returns_label(), jsil_declarationt::returns_value(), simplify_exprt::simplify_typecast(), array_typet::size(), vector_typet::size(), symex_slice_by_tracet::slice_by_trace(), cpp_namet::namet::source_location(), typet::source_location(), exprt::source_location(), cpp_itemt::source_location(), select_pointer_typet::specialize_generics(), cpp_typecheckt::standard_conversion_pointer(), cpp_typecheckt::standard_conversion_pointer_to_member(), cpp_typecheckt::standard_conversion_sequence(), cpp_typecheckt::static_typecast(), cpp_declarationt::storage_spec(), goto_symext::symex_catch(), goto_symext::symex_cpp_new(), goto_symext::symex_throw(), cpp_enum_typet::tag(), template_typet::template_parameters(), cpp_declarationt::template_type(), cpp_declaratort::throw_decl(), jsil_declarationt::throws_label(), jsil_declarationt::throws_value(), jsil_declarationt::to_symbol(), uncaught_exceptions_domaint::transform(), exprt::type(), mathematical_function_typet::variablet::type(), java_generic_parametert::type_variables(), c_typecheck_baset::typecheck_c_enum_tag_type(), c_typecheck_baset::typecheck_c_enum_type(), cpp_typecheckt::typecheck_class_template(), cpp_typecheckt::typecheck_compound_declarator(), c_typecheck_baset::typecheck_compound_type(), cpp_typecheckt::typecheck_compound_type(), c_typecheck_baset::typecheck_custom_type(), c_typecheck_baset::typecheck_declaration(), cpp_typecheckt::typecheck_expr_dereference(), cpp_typecheckt::typecheck_expr_main(), cpp_typecheckt::typecheck_expr_member(), cpp_typecheckt::typecheck_expr_sizeof(), cpp_typecheckt::typecheck_friend_declaration(), cpp_typecheckt::typecheck_function_template(), cpp_typecheckt::typecheck_member_initializer(), cpp_typecheckt::typecheck_side_effect_function_call(), c_typecheck_baset::typecheck_side_effect_statement_expression(), c_typecheck_baset::typecheck_spec_expr(), c_typecheck_baset::typecheck_symbol_type(), c_typecheck_baset::typecheck_type(), cpp_typecheckt::typecheck_type(), c_typecheck_baset::typecheck_typeof_type(), cpp_typecheckt::user_defined_conversion_sequence(), ansi_c_declaratort::value(), cpp_declaratort::value(), jsil_declarationt::value(), yyansi_clex(), and cpp_typecheckt::zero_initializer().
bool irept::full_eq | ( | const irept & | other | ) | const |
Definition at line 380 of file irep.cpp.
References data, get_comments(), get_named_sub(), get_sub(), and id().
Referenced by c_typecastt::implicit_typecast_followed(), and irep_full_eq::operator()().
std::size_t irept::full_hash | ( | ) | const |
Definition at line 606 of file irep.cpp.
References forall_irep, forall_named_irep, get_comments(), get_named_sub(), get_sub(), hash_combine, hash_finalize, and hash_string().
Referenced by irep_full_hash::operator()().
const irep_idt & irept::get | ( | const irep_namet & | name | ) | const |
Definition at line 213 of file irep.cpp.
References get_comments(), get_named_sub(), and is_comment().
Referenced by string_abstractiont::abstract_function_call(), cpp_typecheckt::add_base_components(), add_failed_symbol_if_needed(), ansi_c_parsert::add_tag_with_body(), linkingt::adjust_object_type_rec(), invariant_sett::apply_code(), value_set_fit::apply_code(), value_set_fivrnst::apply_code(), value_set_fivrt::apply_code(), value_set_fit::assign_rec(), base_type_eqt::base_type_eq_rec(), ansi_c_declaratort::build(), inv_object_storet::build_string(), template_mapt::build_template_args(), template_mapt::build_unassigned(), cpp_typecheckt::check_component_access(), cpp_typecheckt::check_member_initializers(), goto_program2codet::cleanup_code(), goto_program2codet::cleanup_expr(), dump_ct::cleanup_expr(), dump_ct::cleanup_type(), dump_ct::collect_typedefs_rec(), cpp_declarator_convertert::convert(), cpp_typecheckt::convert(), cpp_typecheckt::convert_anonymous_union(), expr2javat::convert_code(), expr2cppt::convert_code(), expr2ct::convert_code_goto(), expr2ct::convert_code_switch(), dump_ct::convert_compound(), smt2_convt::convert_constant(), expr2ct::convert_constant(), expr2cppt::convert_cpp_new(), smt2_convt::convert_expr(), cpp_typecheckt::convert_function(), cpp_typecheckt::convert_initializer(), java_bytecode_convert_methodt::convert_instructions(), java_bytecode_convert_methodt::convert_invoke(), expr2javat::convert_java_new(), expr2ct::convert_member(), java_bytecode_convert_methodt::convert_putfield(), expr2ct::convert_rec(), expr2cppt::convert_rec(), boolbvt::convert_symbol(), expr2ct::convert_symbol(), goto_convertt::convert_try_catch(), boolbvt::convert_update_rec(), smt2_convt::convert_with(), expr2javat::convert_with_precedence(), expr2cppt::convert_with_precedence(), expr2ct::convert_with_precedence(), boolbvt::convert_with_struct(), cpp_typecheckt::cpp_constructor(), cpp_typecheckt::cpp_destructor(), cpp_exception_list_rec(), cpp_type2name(), stub_global_initializer_factoryt::create_stub_global_initializer_symbols(), goto_program_dereferencet::dereference_instruction(), cpp_typecheck_resolvet::disambiguate_functions(), cpp_typecheck_resolvet::disambiguate_template_classes(), goto_convertt::do_cpp_new(), c_typecheck_baset::do_designated_initializer(), flow_insensitive_analysis_baset::do_function_call_rec(), c_typecheck_baset::do_initializer_list(), c_typecheck_baset::do_initializer_rec(), c_typecastt::do_typecast(), cpp_typecheckt::do_virtual_table(), cpp_typecheckt::elaborate_class_template(), cpp_typecheck_resolvet::filter_for_named_scopes(), filter_out(), cpp_typecheckt::find_assignop(), cpp_typecheckt::find_cpctor(), find_macros(), find_symbols(), goto_convertt::finish_gotos(), value_set_fit::flatten_rec(), value_set_fivrt::flatten_rec(), cpp_typecheckt::full_member_initialization(), dump_ct::gather_global_typedefs(), c_typecheck_baset::gcc_types_compatible_p(), boolbvt::get(), custom_bitvector_analysist::get_bit_nr(), java_bytecode_parsert::get_class_refs_rec(), get_clinit_wrapper_body(), get_failed_symbol(), get_inherited_component(), get_ldc_result(), get_or_create_string_literal_symbol(), value_set_fit::get_reference_set(), value_set_fivrt::get_reference_set(), value_set_fivrnst::get_reference_set_rec(), value_sett::get_reference_set_rec(), value_set_fit::get_reference_set_sharing_rec(), value_set_fivrt::get_reference_set_sharing_rec(), java_bytecode_convert_methodt::get_static_field(), goto_convertt::get_string_constant(), stub_global_initializer_factoryt::get_stub_initializer_body(), get_thread_safe_clinit_wrapper_body(), value_set_fit::get_value_set_rec(), value_sett::get_value_set_rec(), cpp_typecheckt::get_virtual_bases(), ci_lazy_methodst::get_virtual_method_targets(), goto_checkt::goto_check(), cpp_typecheck_resolvet::guess_function_template_args(), symex_dereference_statet::has_failed_symbol(), goto_program_dereferencet::has_failed_symbol(), goto_convertt::has_function_call(), has_symbol(), infer_opaque_type_fields(), generic_parameter_specialization_map_keyst::insert_pairs_for_pointer(), cpp_typecheckt::instantiate_template(), is_java_main(), java_enum_static_init_unwind_handler(), json(), boolbvt::literal(), remove_java_newt::lower_java_new(), c_typecheck_baset::make_designator(), cpp_typecheckt::new_temporary(), simplify_exprt::objects_equal(), syntactic_difft::operator()(), java_syntactic_difft::operator()(), dump_ct::operator()(), cpp_typecheckt::operator_is_overloaded(), cpp_typecheckt::put_compound_into_scope(), Parser::rAttribute(), java_bytecode_parsert::rClassFile(), c_storage_spect::read(), ansi_c_convert_typet::read_rec(), _rw_set_loct::read_write_rec(), value_set_fivrt::recursive_find(), cpp_typecheckt::reference_binding(), cpp_typecheckt::reference_related(), goto_convertt::remove_function_call(), goto_convertt::remove_statement_expression(), goto_convertt::remove_temporary_object(), Parser::rEnumBody(), goto_symext::replace_nondet(), cpp_typecheck_resolvet::resolve(), cpp_typecheck_resolvet::resolve_with_arguments(), jsil_declarationt::returns_label(), jsil_declarationt::returns_value(), Parser::rName(), Parser::rNamespaceSpec(), Parser::rPtrToMember(), Parser::rStatement(), Parser::rTempArgDeclaration(), Parser::rTypedefUsing(), Parser::rTypeNameOrFunctionType(), Parser::rVarNameCore(), goto_program2codet::scan_for_varargs(), template_mapt::set(), cpp_typecheck_resolvet::show_identifiers(), cpp_languaget::show_parse(), simplify_exprt::simplify_bitwise(), simplify_exprt::simplify_byte_update(), simplify_exprt::simplify_dynamic_object(), simplify_exprt::simplify_extractbit(), simplify_exprt::simplify_index(), simplify_exprt::simplify_inequality_constant(), simplify_exprt::simplify_invalid_pointer(), simplify_exprt::simplify_member(), simplify_exprt::simplify_object_size(), simplify_exprt::simplify_shifts(), simplify_exprt::simplify_with(), cpp_typecheckt::standard_conversion_pointer_to_member(), cpp_typecheckt::standard_conversion_sequence(), string_from_ns(), cpp_typecheckt::subtype_typecast(), goto_symext::symex_cpp_delete(), goto_symext::symex_cpp_new(), goto_symext::symex_macro(), jsil_declarationt::throws_label(), jsil_declarationt::throws_value(), to_member(), to_reference_type(), to_side_effect_expr_function_call(), to_side_effect_expr_throw(), jsil_declarationt::to_symbol(), type2name_symbol(), dereferencet::type_compatible(), c_typecheck_baset::typecheck_c_enum_tag_type(), c_typecheck_baset::typecheck_c_enum_type(), cpp_typecheckt::typecheck_compound_declarator(), c_typecheck_baset::typecheck_compound_type(), c_typecheck_baset::typecheck_expr_address_of(), cpp_typecheckt::typecheck_expr_address_of(), cpp_typecheckt::typecheck_expr_cpp_name(), cpp_typecheckt::typecheck_expr_delete(), cpp_typecheckt::typecheck_expr_explicit_constructor_call(), cpp_typecheckt::typecheck_expr_function_identifier(), c_typecheck_baset::typecheck_expr_main(), cpp_typecheckt::typecheck_expr_main(), c_typecheck_baset::typecheck_expr_member(), cpp_typecheckt::typecheck_expr_member(), cpp_typecheckt::typecheck_expr_new(), c_typecheck_baset::typecheck_expr_operands(), c_typecheck_baset::typecheck_expr_pointer_arithmetic(), cpp_typecheckt::typecheck_expr_side_effect(), java_bytecode_typecheckt::typecheck_expr_symbol(), c_typecheck_baset::typecheck_expr_symbol(), cpp_typecheckt::typecheck_expr_trinary(), c_typecheck_baset::typecheck_function_call_arguments(), c_typecheck_baset::typecheck_ifthenelse(), cpp_typecheckt::typecheck_member_initializer(), c_typecheck_baset::typecheck_redefinition_non_type(), cpp_typecheckt::typecheck_side_effect_assignment(), cpp_typecheckt::typecheck_side_effect_function_call(), cpp_typecheckt::typecheck_side_effect_inc_dec(), c_typecheck_baset::typecheck_type(), cpp_typecheckt::user_defined_conversion_sequence(), validate_type(), xml(), and cpp_typecheckt::zero_initializer().
bool irept::get_bool | ( | const irep_namet & | name | ) | const |
Definition at line 240 of file irep.cpp.
Referenced by add_padding(), add_padding_gcc(), add_padding_msvc(), goto_symext::address_arithmetic(), adjust_byte_extract_rec(), alignment(), cpp_typecheck_resolvet::apply_template_args(), goto_checkt::bounds_check(), check_c_implicit_typecast(), check_renaming(), check_renaming_l1(), cpp_typecheckt::class_template_symbol(), cpp_typecheckt::clean_up(), goto_program2codet::cleanup_expr(), dump_ct::cleanup_expr(), cpp_declarator_convertert::combine_types(), cpp_typecheckt::const_typecast(), cpp_declarator_convertert::convert(), expr2ct::convert_array(), expr2ct::convert_code_fence(), dump_ct::convert_compound(), dump_ct::convert_compound_enum(), cpp_typecheck_resolvet::convert_identifier(), cpp_declarator_convertert::convert_new_symbol(), cpp_typecheckt::convert_pmop(), expr2cppt::convert_rec(), cpp_typecheckt::cpp_constructor(), cpp_exception_list_rec(), cpp_type2name(), stub_global_initializer_factoryt::create_stub_global_initializer_symbols(), cpp_typecheck_resolvet::disambiguate_functions(), cpp_typecheck_resolvet::disambiguate_template_classes(), c_typecheck_baset::do_initializer_rec(), cpp_typecheckt::do_not_typechecked(), cpp_typecheckt::do_virtual_table(), linkingt::duplicate_code_symbol(), linkingt::duplicate_object_symbol(), cpp_typecheckt::dynamic_typecast(), cpp_typecheckt::elaborate_class_template(), cpp_typecheck_resolvet::filter_for_named_scopes(), cpp_typecheckt::find_assignop(), cpp_typecheckt::find_cpctor(), ieee_float_spect::from_type(), cpp_typecheckt::function_identifier(), struct_union_typet::componentt::get_anonymous(), get_any_incomplete_ancestor_for_stub_static_field(), java_class_typet::get_final(), source_locationt::get_hide(), code_typet::get_inlined(), ansi_c_declarationt::get_is_always_inline(), code_typet::get_is_constructor(), ansi_c_declarationt::get_is_enum_constant(), ansi_c_declarationt::get_is_extern(), ansi_c_declarationt::get_is_global(), cpp_namespace_spect::get_is_inline(), ansi_c_declarationt::get_is_inline(), ansi_c_declarationt::get_is_member(), struct_union_typet::componentt::get_is_padding(), ansi_c_declarationt::get_is_parameter(), ansi_c_declarationt::get_is_register(), ansi_c_declarationt::get_is_static(), ansi_c_declarationt::get_is_static_assert(), ansi_c_declarationt::get_is_thread_local(), ansi_c_declarationt::get_is_typedef(), ansi_c_declarationt::get_is_used(), ansi_c_declarationt::get_is_weak(), goto_symex_statet::get_l1_name(), cpp_usingt::get_namespace(), side_effect_expr_nondett::get_nullable(), goto_symex_statet::get_original_name(), get_symbol(), cpp_enum_typet::get_tag_only_declaration(), code_typet::parametert::get_this(), goto_checkt::goto_check(), cpp_typecheck_resolvet::guess_function_template_args(), code_typet::has_ellipsis(), symex_dereference_statet::has_failed_symbol(), goto_program_dereferencet::has_failed_symbol(), c_typecastt::implicit_typecast_followed(), infer_opaque_type_fields(), generic_parameter_specialization_map_keyst::insert_pairs_for_pointer(), generic_parameter_specialization_map_keyst::insert_pairs_for_symbol(), java_bytecode_instrumentt::instrument_expr(), remove_exceptionst::instrument_function_call(), class_typet::is_abstract(), cpp_storage_spect::is_asm(), cpp_storage_spect::is_auto(), class_typet::is_class(), remove_const_function_pointerst::is_const_type(), is_constant_or_has_constant_components(), code_switch_caset::is_default(), pointer_logict::is_dynamic_object(), cpp_member_spect::is_explicit(), cpp_storage_spect::is_extern(), is_fence(), cpp_member_spect::is_friend(), goto_functiont::is_hidden(), cpp_member_spect::is_inline(), goto_functiont::is_inlined(), is_java_generic_class_type(), is_java_generic_parameter(), is_java_generic_symbol_type(), is_java_generic_type(), is_java_implicitly_generic_class_type(), is_jsil_builtin_code_type(), is_jsil_spec_code_type(), code_typet::is_KnR(), is_lwfence(), cpp_storage_spect::is_mutable(), is_reference(), cpp_storage_spect::is_register(), is_rvalue_reference(), is_ssa_expr(), cpp_storage_spect::is_static(), cpp_declarationt::is_static_assert(), decorated_symbol_exprt::is_static_lifetime(), cpp_declarationt::is_template(), cpp_storage_spect::is_thread_local(), decorated_symbol_exprt::is_thread_local(), does_remove_constt::is_type_at_least_as_const_as(), cpp_declarationt::is_typedef(), cpp_namet::is_typename(), postconditiont::is_used(), cpp_member_spect::is_virtual(), is_volatile(), java_static_lifetime_init(), load_java_class(), remove_java_newt::lower_java_new_array(), cpp_typecheck_resolvet::make_constructors(), make_member_expr(), dump_ct::operator()(), class_hierarchyt::operator()(), cpp_typecheckt::operator_is_overloaded(), pointer_offset_bits(), print_global_state_size(), goto_symext::process_array_expr(), memory_model_tsot::program_order(), cpp_typecheckt::put_compound_into_scope(), c_qualifierst::read(), cpp_convert_typet::read_rec(), cpp_convert_typet::read_template(), cpp_typecheckt::reference_binding(), cpp_typecheckt::reference_related(), cpp_typecheckt::reinterpret_typecast(), goto_program2codet::remove_const(), remove_internal_symbols(), goto_symex_statet::rename(), goto_symex_statet::rename_address(), cpp_typecheck_resolvet::resolve(), constant_propagator_domaint::valuest::set_dirty_to_top(), set_internal_dynamic_object(), should_init_symbol(), cpp_typecheck_resolvet::show_identifiers(), size_of_expr(), cpp_typecheckt::standard_conversion_boolean(), cpp_typecheckt::standard_conversion_floating_integral_conversion(), cpp_typecheckt::standard_conversion_floating_point_conversion(), cpp_typecheckt::standard_conversion_floating_point_promotion(), cpp_typecheckt::standard_conversion_function_to_pointer(), cpp_typecheckt::standard_conversion_integral_conversion(), cpp_typecheckt::standard_conversion_integral_promotion(), cpp_typecheckt::standard_conversion_lvalue_to_rvalue(), cpp_typecheckt::standard_conversion_pointer(), cpp_typecheckt::standard_conversion_pointer_to_member(), cpp_typecheckt::standard_conversion_qualification(), cpp_typecheckt::static_typecast(), goto_symext::symex_assign_rec(), to_jsil_builtin_code_type(), to_jsil_spec_code_type(), to_reference_type(), to_ssa_expr(), goto_symext::trigger_auto_object(), type2name(), c_typecheck_baset::typecheck_array_type(), c_typecheck_baset::typecheck_c_enum_type(), cpp_typecheckt::typecheck_compound_bases(), cpp_typecheckt::typecheck_compound_body(), cpp_typecheckt::typecheck_compound_declarator(), cpp_typecheckt::typecheck_compound_type(), cpp_typecheckt::typecheck_decl(), cpp_typecheckt::typecheck_enum_type(), cpp_typecheckt::typecheck_expr(), c_typecheck_baset::typecheck_expr_address_of(), cpp_typecheckt::typecheck_expr_address_of(), c_typecheck_baset::typecheck_expr_comma(), c_typecheck_baset::typecheck_expr_index(), c_typecheck_baset::typecheck_expr_main(), c_typecheck_baset::typecheck_expr_member(), cpp_typecheckt::typecheck_expr_member(), c_typecheck_baset::typecheck_expr_side_effect(), cpp_typecheckt::typecheck_expr_trinary(), c_typecheck_baset::typecheck_expr_typecast(), c_typecheck_baset::typecheck_function_call_arguments(), cpp_typecheckt::typecheck_member_function(), cpp_typecheckt::typecheck_member_initializer(), cpp_typecheckt::typecheck_method_application(), c_typecheck_baset::typecheck_redefinition_non_type(), c_typecheck_baset::typecheck_side_effect_assignment(), c_typecheck_baset::typecheck_side_effect_function_call(), cpp_typecheckt::typecheck_side_effect_function_call(), c_typecheck_baset::typecheck_symbol_type(), cpp_typecheckt::typecheck_template_args(), cpp_typecheckt::typecheck_template_parameters(), c_typecheck_baset::typecheck_type(), cpp_typecheckt::typecheck_type(), c_typecheck_baset::typecheck_typeof_type(), cpp_typecheckt::user_defined_conversion_sequence(), value_set_dereferencet::valid_check(), instrumentert::cfg_visitort::visit_cfg_asm_fence(), shared_bufferst::cfg_visitort::weak_memory(), and cpp_typecheckt::zero_initializer().
|
inline |
Definition at line 249 of file irep.h.
References irept::dt::comments, and write().
Referenced by add(), convert(), json_irept::convert_from_irep(), find(), full_eq(), full_hash(), get(), irep2lisp(), irep2name(), merge_irept::merged(), merge_full_irept::merged(), irep_hash_container_baset::pack(), pretty(), remove(), and irep_serializationt::write_irep().
|
inline |
Definition at line 250 of file irep.h.
References irept::dt::comments, and read().
int irept::get_int | ( | const irep_namet & | name | ) | const |
Definition at line 245 of file irep.cpp.
References get_string(), and unsafe_string2int().
Referenced by boolbvt::convert_bv_reduction(), java_bytecode_convert_methodt::convert_invoke_dynamic(), boolbvt::convert_not(), c_typecastt::get_c_type(), overflow_instrumentert::overflow_expr(), c_typecheck_baset::typecheck_c_bit_field_type(), and underlying_width().
long long irept::get_long_long | ( | const irep_namet & | name | ) | const |
Definition at line 260 of file irep.cpp.
References get_string(), and unsafe_string2signedlonglong().
Referenced by literal_exprt::get_literal().
|
inline |
Definition at line 247 of file irep.h.
References irept::dt::named_sub, and write().
Referenced by add(), compare(), convert(), json_irept::convert_from_irep(), fallback_format_rec(), find(), full_eq(), full_hash(), get(), to_be_merged_irept::hash(), hash(), irep2lisp(), irep2name(), source_locationt::merge(), merged_irepst::merged(), merge_irept::merged(), merge_full_irept::merged(), to_be_merged_irept::operator==(), operator==(), irep_hash_container_baset::pack(), pretty(), remove(), and irep_serializationt::write_irep().
|
inline |
Definition at line 248 of file irep.h.
References irept::dt::named_sub, and read().
std::size_t irept::get_size_t | ( | const irep_namet & | name | ) | const |
Definition at line 255 of file irep.cpp.
References get_string(), and unsafe_string2size_t().
Referenced by java_bytecode_convert_methodt::convert_ushr(), bswap_exprt::get_bits_per_byte(), union_exprt::get_component_number(), member_exprt::get_component_number(), bitvector_typet::get_width(), c_typecastt::implicit_typecast_arithmetic(), and java_enum_static_init_unwind_handler().
|
inline |
Definition at line 202 of file irep.h.
References id2string().
Referenced by ansi_c_parsert::add_tag_with_body(), array_name(), as_vcd_binary(), value_set_fit::assign_rec(), value_sett::assign_rec(), inv_object_storet::build_string(), boolbvt::bv_get_rec(), java_bytecode_convert_methodt::convert_getstatic(), java_bytecode_convert_methodt::convert_instructions(), expr2ct::convert_literal(), expr2ct::convert_member(), expr2ct::convert_member_designator(), expr2ct::convert_predicate_next_symbol(), expr2ct::convert_predicate_passive_symbol(), expr2ct::convert_predicate_symbol(), java_bytecode_convert_methodt::convert_putstatic(), expr2ct::convert_quantified_symbol(), expr2ct::convert_rec(), expr2ct::convert_struct_member_value(), expr2ct::convert_symbol(), boolbvt::convert_typecast(), expr2ct::convert_union(), expr2javat::convert_with_precedence(), expr2ct::convert_with_precedence(), cpp_exception_list_rec(), string_instrumentationt::do_format_string_read(), string_instrumentationt::do_format_string_write(), document_propertiest::doit(), bv_arithmetict::from_expr(), bv_spect::from_type(), cpp_namet::get_base_name(), boolbv_widtht::get_entry(), range_typet::get_from(), get_int(), get_long_long(), get_size_t(), get_string_argument_rec(), range_typet::get_to(), get_unsigned_int(), value_set_fit::get_value_set_rec(), value_sett::get_value_set_rec(), exprt::is_one(), json(), format_constantt::operator()(), dump_ct::operator()(), cpp_typecheckt::put_compound_into_scope(), _rw_set_loct::read_write_rec(), simplify_exprt::simplify_bitnot(), simplify_exprt::simplify_concatenation(), simplify_exprt::simplify_if_implies(), cpp_typecheckt::template_suffix(), string_constantt::to_array_expr(), to_rational(), jsil_declarationt::to_symbol(), trace_value_binary(), type2name(), linkingt::type_to_string_verbose(), cpp_typecheckt::typecheck_compound_declarator(), cpp_typecheckt::typecheck_side_effect_function_call(), and xml().
|
inline |
Definition at line 245 of file irep.h.
References irept::dt::sub, and write().
Referenced by cpp_typecheckt::add_base_components(), Parser::add_id(), template_mapt::apply(), cpp_template_args_baset::arguments(), class_typet::bases(), cpp_typecheckt::check_component_access(), cpp_typecheckt::check_member_initializers(), cpp_typecheckt::clean_up(), compare(), struct_union_typet::components(), convert(), cpp_declarator_convertert::convert(), cpp_typecheckt::convert_anonymous_union(), boolbvt::convert_bv_literals(), cpp_typecheckt::convert_class_template_specialization(), dump_ct::convert_compound(), dump_ct::convert_compound_enum(), json_irept::convert_from_irep(), json_irept::convert_from_json(), expr2cppt::convert_rec(), cpp_typecheckt::convert_template_function_or_member_specialization(), copy_array(), copy_member(), copy_parent(), cpp_typecheckt::cpp_constructor(), cpp_typecheckt::cpp_destructor(), cpp_exception_list(), cpp_exception_list_rec(), cpp_typecheckt::cpp_is_pod(), cpp_namet::cpp_namet(), cpp_typecheckt::default_assignop(), cpp_typecheckt::default_assignop_value(), cpp_typecheckt::default_cpctor(), cpp_typecheckt::dtor(), enumeration_typet::elements(), code_push_catcht::exception_list(), cpp_typecheckt::find_dtor(), cpp_typecheckt::find_parent(), full_eq(), full_hash(), cpp_typecheckt::full_member_initialization(), cpp_enum_typet::generate_anon_tag(), java_generic_typet::generic_type_arguments(), java_generic_class_typet::generic_types(), java_generic_symbol_typet::generic_types(), annotated_typet::get_annotations(), cpp_namet::get_base_name(), cpp_typecheckt::get_bases(), cpp_declarator_convertert::get_pretty_name(), java_annotationt::valuet::get_value(), java_annotationt::get_values(), cpp_typecheckt::get_virtual_bases(), typet::has_subtype(), typet::has_subtypes(), cpp_namet::has_template_args(), to_be_merged_irept::hash(), hash(), java_implicitly_generic_class_typet::implicit_generic_types(), cpp_typecheckt::instantiate_template(), irep2lisp(), irep2name(), cpp_namet::is_destructor(), cpp_namet::is_operator(), cpp_namet::is_qualified(), cpp_namet::is_simple_name(), java_class_typet::lambda_method_handles(), boolbvt::make_bv_expr(), c_enum_typet::members(), merged_irepst::merged(), merge_irept::merged(), merge_full_irept::merged(), class_typet::methods(), cpp_typecheckt::move_member_initializers(), move_to_sub(), exprt::operands(), class_hierarchyt::operator()(), to_be_merged_irept::operator==(), operator==(), cpp_typecheckt::operator_is_overloaded(), goto_programt::output_instruction(), irep_hash_container_baset::pack(), code_typet::parameters(), smt2_convt::parse_array(), smt2_convt::parse_literal(), smt2_convt::parse_struct(), pretty(), Parser::rArgDeclList(), Parser::rBaseSpecifiers(), cpp_convert_typet::read_function_type(), irep_serializationt::read_irep(), smt2_dect::read_result(), cpp_typecheckt::reference_binding(), typet::remove_subtype(), Parser::rEnumBody(), cpp_typecheck_resolvet::resolve_scope(), Parser::rName(), Parser::rOtherDeclaration(), Parser::rPtrToMember(), Parser::rTempArgDeclaration(), Parser::rTempArgList(), Parser::rTemplateArgs(), Parser::rTemplateDecl2(), Parser::rVarNameCore(), cpp_namet::source_location(), typet::subtype(), typet::subtypes(), goto_symext::symex_catch(), goto_symext::symex_throw(), template_typet::template_parameters(), cpp_namet::to_string(), uncaught_exceptions_domaint::transform(), java_generic_parametert::type_variables(), c_typecheck_baset::typecheck_c_enum_type(), cpp_typecheckt::typecheck_cast_expr(), cpp_typecheckt::typecheck_class_template_member(), cpp_typecheckt::typecheck_compound_bases(), cpp_typecheckt::typecheck_compound_declarator(), cpp_typecheckt::typecheck_enum_body(), cpp_typecheckt::typecheck_expr_cpp_name(), c_typecheck_baset::typecheck_expr_main(), cpp_typecheckt::typecheck_function_expr(), cpp_typecheckt::typecheck_side_effect_assignment(), cpp_typecheckt::typecheck_side_effect_function_call(), cpp_typecheckt::typecheck_side_effect_inc_dec(), cpp_typecheckt::typecheck_type(), cpp_typecheckt::user_defined_conversion_sequence(), java_annotationt::valuet::valuet(), irep_serializationt::write_irep(), and cpp_typecheckt::zero_initializer().
|
inline |
Definition at line 246 of file irep.h.
References read(), and irept::dt::sub.
unsigned int irept::get_unsigned_int | ( | const irep_namet & | name | ) | const |
Definition at line 250 of file irep.cpp.
References get_string(), and unsafe_string2unsigned().
Referenced by from_integer(), get_bytecode_type_width(), boolbv_widtht::get_entry(), and java_local_variable_slots().
std::size_t irept::hash | ( | ) | const |
Definition at line 575 of file irep.cpp.
References forall_irep, forall_named_irep, get_named_sub(), get_sub(), hash_combine, hash_finalize, hash_string(), and read().
Referenced by irep_hash::operator()().
|
inline |
Definition at line 189 of file irep.h.
References irept::dt::data, and read().
Referenced by acceleration_utilst::abstract_arrays(), string_abstractiont::abstract_assign(), string_abstractiont::abstract_char_assign(), string_abstractiont::abstract_function_call(), string_abstractiont::abstract_pointer_assign(), disjunctive_polynomial_accelerationt::accelerate(), polynomial_acceleratort::accelerate(), actuals_replace_map(), guardt::add(), c_typecheck_baset::add_argc_argv(), arrayst::add_array_constraints(), string_constraint_generatort::add_axioms_for_code_point(), string_constraint_generatort::add_axioms_for_code_point_at(), string_constraint_generatort::add_axioms_for_contains(), 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_index_of(), 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_last_index_of(), string_constraint_generatort::add_axioms_from_bool(), string_constraint_generatort::add_axioms_from_int_hex(), string_constraint_generatort::add_axioms_from_int_with_radix(), add_character_set_constraint(), ansi_c_parsert::add_declarator(), string_abstractiont::add_dummy_symbol_and_value(), add_failed_symbol(), goto_program2codet::add_local_types(), pointer_logict::add_object(), bv_minimizet::add_objective(), add_padding_gcc(), add_pointer_to_array_association(), c_typecheck_baset::add_rounding_mode(), add_string_equation_to_symbol_resolution(), add_to_index_set(), goto_symext::add_to_lhs(), pointer_arithmetict::add_to_offset(), invariant_sett::add_type_bounds(), compilet::add_written_cprover_symbols(), goto_symext::address_arithmetic(), adjust_byte_extract_rec(), adjust_float_expressions(), c_typecheck_baset::adjust_float_rel(), c_typecheck_baset::adjust_function_parameter(), linkingt::adjust_object_type_rec(), interval_domaint::ai_simplify(), ai_domain_baset::ai_simplify_lhs(), custom_bitvector_analysist::aliases(), aliasing(), alignment(), allocate_dynamic_object(), template_mapt::apply(), c_typecheck_baset::apply_asm_label(), value_set_fit::apply_code(), value_set_fivrnst::apply_code(), value_set_fivrt::apply_code(), value_sett::apply_code_rec(), code_contractst::apply_contract(), cpp_typecheck_resolvet::apply_template_args(), approximate_nondet_rec(), remove_function_pointerst::arg_is_type_compatible(), array_name(), bv_refinementt::arrays_overapproximated(), as_vcd_binary(), polynomial_acceleratort::assert_for_values(), uninitialized_domaint::assign(), value_set_fit::assign(), value_set_fivrnst::assign(), value_set_fivrt::assign(), value_sett::assign(), acceleration_utilst::assign_array(), local_may_aliast::assign_lhs(), local_bitvector_analysist::assign_lhs(), global_may_alias_domaint::assign_lhs_aliases(), escape_domaint::assign_lhs_aliases(), escape_domaint::assign_lhs_cleanup(), constant_propagator_domaint::assign_rec(), value_set_fit::assign_rec(), value_set_fivrnst::assign_rec(), value_set_fivrt::assign_rec(), value_sett::assign_rec(), custom_bitvector_domaint::assign_struct_rec(), goto_symex_statet::assignment(), interval_domaint::assume_rec(), base_type_eqt::base_type_eq_rec(), base_type_rec(), simplify_exprt::bits2expr(), boolbvt::boolbv_set_equality_to_true(), boolean_negate(), goto_checkt::bounds_check(), value_set_dereferencet::bounds_check(), bracket_subexpression(), ansi_c_declaratort::build(), string_abstractiont::build(), string_abstractiont::build_abstraction_type_rec(), bv_endianness_mapt::build_big_endian(), endianness_mapt::build_big_endian(), build_full_lhs_rec(), interpretert::build_memory_map(), build_object_descriptor_rec(), string_abstractiont::build_pointer(), value_set_dereferencet::build_reference_to(), build_ssa_identifier_rec(), inv_object_storet::build_string(), template_mapt::build_template_args(), template_mapt::build_unassigned(), string_abstractiont::build_wrap(), boolbvt::bv_get_cache(), bv_pointerst::bv_get_rec(), boolbvt::bv_get_rec(), boolbvt::bv_get_unbounded_array(), interpretert::byte_offset_to_memory_offset(), c_bit_field_replacement_type(), c_sizeof_type_rec(), ssa_exprt::can_build_identifier(), cpp_typecheckt::cast_away_constness(), smt2_parsert::cast_bv_to_unsigned(), mm2cppt::check_acyclic(), check_c_implicit_typecast(), cpp_typecheckt::check_fixed_size_array(), escape_domaint::check_lhs(), cpp_typecheckt::check_member_initializers(), java_simple_method_stubst::check_method_stub(), goto_checkt::check_rec(), check_renaming(), check_renaming_l1(), bv_refinementt::check_SAT(), value_set_analysis_fit::check_type(), value_set_analysis_fivrt::check_type(), value_set_analysis_fivrnst::check_type(), invariant_propagationt::check_type(), bv_refinementt::check_UNSAT(), clean_deref(), goto_convertt::clean_expr(), goto_convertt::clean_expr_address_of(), cpp_typecheckt::clean_up(), goto_program2codet::cleanup_code(), goto_program2codet::cleanup_expr(), dump_ct::cleanup_expr(), dump_ct::cleanup_harness(), dump_ct::cleanup_type(), java_string_library_preprocesst::code_assign_java_string_to_string_expr(), code_function_callt::code_function_callt(), goto_checkt::collect_allocations(), arrayst::collect_arrays(), collect_comma_expression(), collect_conditions_rec(), collect_decisions_rec(), collect_deref_expr(), arrayst::collect_indices(), collect_mcdc_controlling_rec(), collect_operands(), goto_convertt::collect_operands(), dump_ct::collect_typedefs_rec(), cpp_declarator_convertert::combine_types(), compare(), compare_components(), complex_member(), preconditiont::compute_address_of(), compute_address_taken_functions(), compute_functions(), compute_pointer_offset(), preconditiont::compute_rec(), interpretert::concretize_type(), cpp_typecheckt::const_typecast(), goto_symex_statet::constant_propagation(), goto_symex_statet::constant_propagation_reference(), monomialt::contains(), float_bvt::conversion(), goto_checkt::conversion_check(), convert(), float_bvt::convert(), cpp_declarator_convertert::convert(), prop_conv_solvert::convert(), smt2_convt::convert(), cpp_typecheckt::convert(), boolbvt::convert_add_sub(), bv_pointerst::convert_address_of_rec(), smt2_convt::convert_address_of_rec(), expr2ct::convert_allocate(), boolbvt::convert_array(), boolbvt::convert_array_of(), goto_convertt::convert_assign(), graphml_witnesst::convert_assign_rec(), goto_program2codet::convert_assign_rec(), goto_program2codet::convert_assign_varargs(), expr2ct::convert_binary(), bv_cbmct::convert_bitvector(), bv_pointerst::convert_bitvector(), boolbvt::convert_bitvector(), boolbvt::convert_bitwise(), prop_conv_solvert::convert_bool(), boolbvt::convert_bv_reduction(), boolbvt::convert_bv_rel(), boolbvt::convert_byte_extract(), boolbvt::convert_byte_update(), smt2_convt::convert_byte_update(), cpp_typecheckt::convert_class_template_specialization(), jsil_convertt::convert_code(), expr2ct::convert_code_decl(), boolbvt::convert_complex(), expr2ct::convert_complex(), dump_ct::convert_compound(), dump_ct::convert_compound_declaration(), dump_ct::convert_compound_enum(), java_bytecode_convert_methodt::convert_const(), expr2javat::convert_constant(), expr2cppt::convert_constant(), smt2_convt::convert_constant(), boolbvt::convert_constant(), expr2ct::convert_constant(), boolbvt::convert_constraint_select_one(), convert_decl(), goto_convertt::convert_decl(), bv_refinementt::convert_div(), smt2_convt::convert_div(), boolbvt::convert_div(), smt2_convt::convert_expr(), goto_convertt::convert_expression(), smt2_convt::convert_floatbv(), smt2_convt::convert_floatbv_div(), smt2_convt::convert_floatbv_minus(), smt2_convt::convert_floatbv_mult(), boolbvt::convert_floatbv_op(), smt2_convt::convert_floatbv_plus(), smt2_convt::convert_floatbv_typecast(), boolbvt::convert_floatbv_typecast(), json_irept::convert_from_irep(), goto_convert_functionst::convert_function(), cpp_typecheckt::convert_function(), java_bytecode_convert_methodt::convert_getstatic(), dump_ct::convert_global_variable(), goto_program2codet::convert_goto_switch(), goto_program2codet::convert_goto_while(), cpp_typecheck_resolvet::convert_identifier(), cpp_typecheck_resolvet::convert_identifiers(), boolbvt::convert_ieee_float_rel(), goto_convertt::convert_ifthenelse(), boolbvt::convert_index(), cpp_typecheckt::convert_initializer(), expr2ct::convert_initializer_list(), java_bytecode_convert_methodt::convert_instructions(), java_bytecode_convert_methodt::convert_invoke(), boolbvt::convert_lambda(), expr2ct::convert_member(), boolbvt::convert_member(), smt2_convt::convert_member(), smt2_convt::convert_minus(), bv_refinementt::convert_mod(), boolbvt::convert_mod(), smt2_convt::convert_mod(), bv_refinementt::convert_mult(), boolbvt::convert_mult(), smt2_convt::convert_mult(), expr2ct::convert_multi_ary(), cpp_declarator_convertert::convert_new_symbol(), java_bytecode_convert_methodt::convert_newarray(), cpp_typecheckt::convert_non_template_declaration(), boolbvt::convert_not(), boolbvt::convert_onehot(), expr2ct::convert_overflow(), boolbvt::convert_overflow(), smt2_convt::convert_plus(), cpp_typecheckt::convert_pmop(), bv_pointerst::convert_pointer_type(), boolbvt::convert_power(), java_bytecode_convert_methodt::convert_putstatic(), expr2ct::convert_rec(), expr2javat::convert_rec(), expr2cppt::convert_rec(), boolbvt::convert_reduction(), smt2_convt::convert_relation(), bv_pointerst::convert_rest(), boolbvt::convert_rest(), goto_program2codet::convert_return(), goto_convertt::convert_return(), smt2_convt::convert_rounding_mode_FPA(), boolbvt::convert_shift(), expr2javat::convert_struct(), expr2cppt::convert_struct(), expr2ct::convert_struct(), expr2ct::convert_symbol(), cpp_typecheckt::convert_template_declaration(), cpp_typecheck_resolvet::convert_template_parameter(), convert_threadblock(), smt2_convt::convert_type(), expr2ct::convert_typecast(), boolbvt::convert_typecast(), smt2_convt::convert_typecast(), boolbvt::convert_unary_minus(), boolbvt::convert_update_rec(), boolbvt::convert_vector(), expr2ct::convert_vector(), boolbvt::convert_verilog_case_equality(), boolbvt::convert_with(), smt2_convt::convert_with(), expr2javat::convert_with_precedence(), expr2cppt::convert_with_precedence(), expr2ct::convert_with_precedence(), copy_array(), ansi_c_parsert::copy_item(), copy_member(), interpretert::count_type_leaves(), cpp_typecheckt::cpp_constructor(), cpp_convert_auto(), cpp_convert_plain_type(), cpp_typecheckt::cpp_destructor(), cpp_exception_list_rec(), cpp_typecheckt::cpp_is_pod(), cpp_type2name(), java_simple_method_stubst::create_method_stub(), java_simple_method_stubst::create_method_stub_at(), create_stub_global_symbol(), cpp_typecheckt::default_assignop(), cpp_typecheckt::default_assignop_value(), cpp_typecheckt::default_cpctor(), cpp_typecheckt::default_ctor(), cpp_typecheckt::default_dtor(), smt2_solvert::define_constants(), smt2_convt::define_object_size(), value_set_dereferencet::dereference(), dereference_exprt::dereference_exprt(), dereferencet::dereference_plus(), dereferencet::dereference_rec(), goto_program_dereferencet::dereference_rec(), goto_symext::dereference_rec(), value_set_fit::dereference_rec(), value_set_fivrnst::dereference_rec(), value_set_fivrt::dereference_rec(), value_sett::dereference_rec(), goto_symext::dereference_rec_address_of(), value_set_dereferencet::dereference_type_compare(), dereferencet::dereference_typecast(), c_typecheck_baset::designator_enter(), linkingt::detailed_conflict_report_rec(), cpp_typecheck_resolvet::disambiguate_functions(), cpp_typecheck_resolvet::disambiguate_template_classes(), cpp_typecheck_resolvet::do_builtin(), c_typecheck_baset::do_designated_initializer(), string_instrumentationt::do_format_string_read(), string_instrumentationt::do_format_string_write(), value_set_fit::do_free(), value_set_fivrnst::do_free(), value_set_fivrt::do_free(), value_sett::do_free(), goto_convertt::do_function_call_symbol(), parameter_assignmentst::do_function_calls(), remove_returnst::do_function_calls(), c_typecheck_baset::do_initializer(), c_typecheck_baset::do_initializer_list(), c_typecheck_baset::do_initializer_rec(), acceleration_utilst::do_nonrecursive(), cpp_typecheckt::do_not_typechecked(), bv_pointerst::do_postponed(), goto_convertt::do_printf(), goto_convertt::do_prob_uniform(), goto_convertt::do_scanf(), c_typecheck_baset::do_special_functions(), c_typecastt::do_typecast(), cpp_typecheckt::do_virtual_table(), does_remove_constt::does_type_preserve_const_correctness(), cpp_typecheckt::dtor(), linkingt::duplicate_code_symbol(), linkingt::duplicate_non_type_symbol(), linkingt::duplicate_object_symbol(), linkingt::duplicate_type_symbol(), dynamic_object_exprt::dynamic_object_exprt(), cpp_typecheckt::dynamic_typecast(), cpp_typecheckt::elaborate_class_template(), simplify_exprt::eliminate_common_addends(), equal_java_types(), equalityt::equality2(), custom_bitvector_domaint::eval(), eval_expr(), value_sett::eval_pointer_offset(), eval_string(), interpretert::evaluate(), interpretert::evaluate_address(), interpretert::execute_assign(), smt2_solvert::expand_function_applications(), goto_inlinet::expand_function_call(), cpp_typecheckt::explicit_typecast_ambiguity(), simplify_exprt::expr2bits(), expr_eq(), expr_initializert< nondet >::expr_initializer_rec(), extract_strings(), extract_strings_from_lhs(), fallback_format_rec(), value_sett::field_sensitive(), cpp_typecheck_resolvet::filter_for_named_scopes(), filter_out(), java_bytecode_parse_treet::find_annotation(), cpp_typecheckt::find_cpctor(), dirtyt::find_dirty(), dirtyt::find_dirty_address_of(), require_goto_statements::find_function_calls(), find_macros(), require_goto_statements::find_pointer_assignments(), require_goto_statements::find_struct_component_assignments(), find_superclass_with_type(), find_symbols(), smt2_convt::find_symbols(), smt2_convt::find_symbols_rec(), require_goto_statements::find_this_component_assignment(), find_used_functions(), goto_convertt::finish_computed_gotos(), fix_types(), smt2_convt::flatten2bv(), flatten_byte_extract(), flatten_byte_operators(), flatten_byte_update(), value_set_fit::flatten_rec(), value_set_fivrt::flatten_rec(), goto_checkt::float_overflow_check(), namespace_baset::follow(), namespace_baset::follow_macros(), namespace_baset::follow_tag(), follow_tags_symbols(), c_typecastt::follow_with_qualifiers(), for_each_atomic_string(), forall_callsites(), format_rec(), string_constantt::from_array_expr(), polynomialt::from_expr(), bdd_exprt::from_expr_rec(), from_integer(), bv_spect::from_type(), full_eq(), cpp_typecheckt::full_member_initialization(), ansi_c_declarationt::full_type(), remove_exceptionst::function_or_callees_may_throw(), acceleration_utilst::gather_array_accesses(), acceleration_utilst::gather_array_assignments(), ci_lazy_methods_neededt::gather_field_types(), ci_lazy_methodst::gather_needed_globals(), cone_of_influencet::gather_rvalues(), acceleration_utilst::gather_rvalues(), gather_symbol_live_ranges(), ci_lazy_methodst::gather_virtual_callsites(), c_typecheck_baset::gcc_types_compatible_p(), c_typecheck_baset::gcc_vector_types_compatible(), java_object_factoryt::gen_nondet_array_init(), symbol_factoryt::gen_nondet_init(), java_object_factoryt::gen_nondet_init(), java_object_factoryt::gen_nondet_pointer_init(), java_object_factoryt::gen_nondet_struct_init(), java_object_factoryt::gen_pointer_target_init(), generate_ansi_c_start_function(), goto_convertt::generate_conditional_branch(), generate_symbol_resolution_from_equations(), boolbvt::get(), prop_conv_solvert::get(), smt2_convt::get(), get_array(), goto_convertt::get_array_argument(), class_typet::get_base(), custom_bitvector_analysist::get_bit_nr(), prop_conv_solvert::get_bool(), invariant_sett::get_bounds(), get_bvtype(), get_bytecode_type_width(), c_typecastt::get_c_type(), ansi_c_parsert::get_class(), get_class_identifier_field(), java_bytecode_parsert::get_class_refs_rec(), interpretert::get_component(), cpp_typecheckt::get_component(), get_component_rec(), invariant_sett::get_constant(), goto_convertt::get_constant(), get_data_type(), get_dependencies_from_generic_parameters_rec(), get_destructor(), value_set_analysis_fit::get_entries_rec(), value_set_analysis_fivrt::get_entries_rec(), value_set_analysis_fivrnst::get_entries_rec(), boolbv_widtht::get_entry(), uncaught_exceptions_domaint::get_exception_symbol(), uncaught_exceptions_domaint::get_exception_type(), escape_domaint::get_function(), get_function_name(), goto_symex_statet::get_l1_name(), get_ldc_result(), get_length_type(), boolbv_mapt::get_map_entry(), counterexample_beautificationt::get_minimization_list(), function_modifiest::get_modifies_lhs(), get_modifies_lhs(), get_module(), get_module_by_name(), java_annotationt::valuet::get_name(), get_nil_irep(), rw_range_sett::get_objects_byte_extract(), rw_range_sett::get_objects_complex(), rw_range_sett::get_objects_index(), rw_range_sett::get_objects_member(), get_objects_rec(), invariant_propagationt::get_objects_rec(), rw_range_sett::get_objects_rec(), rw_range_sett::get_objects_shift(), get_or_create_string_literal_symbol(), goto_symex_statet::get_original_name(), get_quantifier_var_max(), get_quantifier_var_min(), local_may_aliast::get_rec(), local_bitvector_analysist::get_rec(), value_set_fit::get_reference_set(), value_set_fivrt::get_reference_set(), value_set_fivrnst::get_reference_set_rec(), value_sett::get_reference_set_rec(), value_set_fit::get_reference_set_sharing_rec(), value_set_fivrt::get_reference_set_sharing_rec(), custom_bitvector_domaint::get_rhs(), global_may_alias_domaint::get_rhs_aliases(), escape_domaint::get_rhs_aliases(), global_may_alias_domaint::get_rhs_aliases_address_of(), escape_domaint::get_rhs_aliases_address_of(), escape_domaint::get_rhs_cleanup(), get_significand(), interpretert::get_size(), get_string_argument_rec(), goto_convertt::get_string_constant(), get_sub_arrays(), get_subexpression_at_offset(), value_set_dereferencet::get_symbol(), get_symbol(), symex_slicet::get_symbols(), get_symbols_rec(), get_tag(), interpretert::get_value(), value_set_fit::get_value_set_rec(), value_set_fivrnst::get_value_set_rec(), value_set_fivrt::get_value_set_rec(), value_sett::get_value_set_rec(), simplify_exprt::get_values(), ci_lazy_methodst::get_virtual_method_targets(), goto_checkt::goto_check(), goto_partial_inline(), value_sett::guard(), cpp_typecheck_resolvet::guess_function_template_args(), cpp_typecheck_resolvet::guess_template_args(), cpp_declarator_convertert::handle_initializer(), has_and_or(), cpp_typecheckt::has_auto(), has_byte_operator(), cpp_typecheckt::has_const(), symex_dereference_statet::has_failed_symbol(), goto_program_dereferencet::has_failed_symbol(), goto_convertt::has_function_call(), custom_bitvector_domaint::has_get_must_or_may(), has_nondet(), string_abstractiont::has_string_macros(), has_subexpr(), has_subtype(), has_symbol(), cpp_typecheckt::has_volatile(), have_to_adjust_float_expressions(), have_to_remove_complex(), have_to_remove_vector(), rename_symbolt::have_to_rename(), replace_symbolt::have_to_replace(), have_to_rewrite_union(), interval_domaint::havoc_rec(), goto_symext::havoc_rec(), implicit(), cpp_typecheckt::implicit_typecast(), c_typecastt::implicit_typecast_arithmetic(), c_typecastt::implicit_typecast_followed(), symex_slice_by_tracet::implied_guards(), invariant_sett::implies_rec(), c_typecheck_baset::increment_designator(), initial_index_set(), goto_symext::initialize_auto_object(), instantiate(), instantiate_quantifier(), cpp_typecheckt::instantiate_template(), mm2cppt::instruction2cpp(), cover_cover_instrumentert::instrument(), java_bytecode_instrumentt::instrument_code(), java_bytecode_instrumentt::instrument_expr(), remove_exceptionst::instrument_function_call(), goto_checkt::integer_overflow_check(), goto_checkt::invalidate(), string_instrumentationt::invalidate_buffer(), irep2name(), irept(), is_a_bv_type(), is_bitvector(), simplify_exprt::is_bitvector_type(), exprt::is_boolean(), is_char_array_type(), is_char_pointer_type(), is_char_type(), string_abstractiont::is_char_type(), cpp_declarationt::is_class_template(), cpp_declarator_convertert::is_code_type(), c_typecheck_baset::is_complete_type(), is_condition(), remove_const_function_pointerst::is_const_type(), exprt::is_constant(), constant_propagator_domaint::valuest::is_constant(), inv_object_storet::is_constant_address(), constant_propagator_domaint::valuest::is_constant_address_of(), inv_object_storet::is_constant_address_rec(), is_constant_or_has_constant_components(), cpp_declarationt::is_constructor(), cpp_itemt::is_declaration(), is_dereference_integer_object(), cpp_declarationt::is_destructor(), pointer_logict::is_dynamic_object(), exprt::is_false(), interval_domaint::is_float(), symbolt::is_function(), is_index_member_symbol(), goto_symext::is_index_member_symbol_if(), interval_domaint::is_int(), java_string_library_preprocesst::is_java_char_array_pointer_type(), java_string_library_preprocesst::is_java_char_sequence_pointer_type(), is_java_main(), java_string_library_preprocesst::is_java_string_buffer_pointer_type(), java_string_library_preprocesst::is_java_string_builder_pointer_type(), java_string_library_preprocesst::is_java_string_pointer_type(), is_jsil_builtin_code_type(), is_jsil_spec_code_type(), cpp_itemt::is_linkage_spec(), is_lvalue(), cpp_itemt::is_namespace_spec(), is_nil(), is_not_nil(), is_not_zero(), is_number(), c_typecheck_baset::is_numeric_type(), remove_calls_no_bodyt::is_opaque_function_call(), is_ptr_argument(), string_abstractiont::is_ptr_string_struct(), is_reference(), is_refined_string_type(), is_rvalue_reference(), is_signed(), is_skip(), is_ssa_expr(), cpp_itemt::is_static_assert(), string_instrumentationt::is_string_type(), languaget::is_symbol_opaque_function(), is_symbol_with_id(), exprt::is_true(), is_typecast_with_id(), boolbvt::is_unbounded_array(), is_unsigned(), postconditiont::is_used(), postconditiont::is_used_address_of(), cpp_itemt::is_using(), is_valid_java_array(), goto_program_dereferencet::is_valid_object(), is_void_pointer(), is_volatile(), java_add_components_to_class(), java_bytecode_instrument_symbol(), java_char_from_type(), java_entry_point(), java_is_array_type(), java_local_variable_slots(), java_record_outputs(), java_type_from_string(), jsil_is_subtype(), json(), length_constraint_for_concat_substr(), link_functions(), linker_script_merget::linker_script_merget(), lisp2irep(), list_calls_and_arguments(), boolbvt::literal(), prop_conv_solvert::literal(), load_java_class(), look_through_casts(), remove_instanceoft::lower_instanceof(), remove_java_newt::lower_java_new(), remove_java_newt::lower_java_new_array(), lower_popcount(), cpp_declarator_convertert::main_function_rules(), array_poolt::make_char_array_for_char_pointer(), make_clean_pointer_cast(), c_typecheck_baset::make_constant(), c_typecheck_baset::make_constant_index(), cpp_typecheck_resolvet::make_constructors(), cpp_itemt::make_declaration(), c_typecheck_baset::make_designator(), cpp_itemt::make_linkage_spec(), value_sett::make_member(), cpp_itemt::make_namespace_spec(), cpp_typecheckt::make_ptr_typecast(), cpp_itemt::make_static_assert(), Parser::make_subtype(), jsil_typecheckt::make_type_compatible(), cpp_itemt::make_using(), make_va_list(), string_abstractiont::make_val_or_dummy_rec(), map_representation_of_sum(), max_printed_string_length(), max_value(), string_abstractiont::member(), member_offset_expr(), member_type_lazy(), value_set_dereferencet::memory_model(), value_set_dereferencet::memory_model_bytes(), interpretert::memory_offset_to_byte_offset(), cpp_declaratort::merge_type(), Parser::merge_types(), merged_irepst::merged(), merge_irept::merged(), merge_full_irept::merged(), c_typecastt::minimum_promotion(), model_argc_argv(), invariant_sett::modifies(), string_abstractiont::move_lhs_arithmetic(), cpp_typecheckt::move_member_initializers(), mul_expr(), mutex_init_instrumentation(), cpp_declarationt::name_anon_struct_union(), goto_checkt::nan_check(), goto_convertt::needs_cleaning(), linkingt::needs_renaming_type(), invariant_sett::nnf(), nondet_volatile_lhs(), nondet_volatile_rhs(), not_exprt::not_exprt(), custom_bitvector_domaint::object2id(), object_descriptor_exprt::object_descriptor_exprt(), pointer_logict::object_rec(), simplify_exprt::objects_equal(), simplify_exprt::objects_equal_address_of(), objects_read(), objects_written(), bv_pointerst::offset_arithmetic(), format_constantt::operator()(), jsil_convertt::operator()(), dump_ct::operator()(), numeric_castt< mp_integer >::operator()(), dereferencet::operator()(), goto_symex_statet::level0t::operator()(), goto_symex_statet::propagationt::operator()(), operator-=(), to_be_merged_irept::operator==(), operator==(), cpp_typecheckt::operator_is_overloaded(), operator|=(), value_set_fit::output(), value_set_fivrt::output(), value_sett::output(), value_set_fivrnst::output_entry(), output_vcd(), overflow_instrumentert::overflow_expr(), cpp_typecheckt::overloadable(), irep_hash_container_baset::pack(), goto_inlinet::parameter_assignments(), goto_symext::parameter_assignments(), code_typet::parameter_indices(), parse_lhs_read(), smt2_convt::parse_literal(), smt2_convt::parse_rec(), pointer_offset_bits(), pointer_offset_sum(), goto_checkt::pointer_overflow_check(), goto_checkt::pointer_rel_check(), acceleration_utilst::precondition(), polynomial_acceleratort::precondition(), pretty_java_type(), print_global_state_size(), goto_symext::process_array_expr(), printf_formattert::process_format(), acceleration_utilst::push_nondet(), cpp_typecheckt::put_compound_into_scope(), cpp_scopest::put_into_scope(), java_bytecode_parsert::rbytecode(), Parser::rClassMember(), Parser::rDeclaratorWithInit(), pointer_arithmetict::read(), c_storage_spect::read(), read_bin_goto_object_v3(), cpp_convert_typet::read_function_type(), irep_serializationt::read_irep(), dereferencet::read_object(), cpp_convert_typet::read_rec(), ansi_c_convert_typet::read_rec(), smt2_dect::read_result(), _rw_set_loct::read_write_rec(), record_function_outputs(), value_set_fivrt::recursive_find(), cpp_typecheckt::reference_binding(), cpp_typecheckt::reference_related(), cpp_typecheckt::reinterpret_typecast(), goto_convertt::remove_assignment(), remove_complex(), goto_program2codet::remove_const(), goto_convertt::remove_function_call(), remove_function_pointerst::remove_function_pointers(), remove_internal_symbols(), graphml_witnesst::remove_l0_l1(), goto_convertt::remove_post(), goto_convertt::remove_pre(), goto_convertt::remove_statement_expression(), remove_vector(), remove_virtual_functionst::remove_virtual_function(), remove_virtual_functionst::remove_virtual_functions(), rename_symbolt::rename(), goto_symex_statet::rename(), goto_symex_statet::rename_address(), replace_symbolt::replace(), constant_propagator_ait::replace(), character_refine_preprocesst::replace_character_call(), remove_const_function_pointerst::replace_const_symbols(), goto_convertt::replace_new_object(), goto_symext::replace_nondet(), string_abstractiont::replace_string_macros(), require_type::require_code(), require_type::require_complete_class(), require_type::require_incomplete_class(), require_expr::require_index(), require_type::require_java_generic_class(), require_type::require_java_implicitly_generic_class(), require_type::require_java_non_generic_class(), require_expr::require_member(), require_type::require_pointer(), require_expr::require_side_effect_expr(), require_type::require_symbol(), require_expr::require_symbol(), require_expr::require_top_index(), require_expr::require_typecast(), cpp_typecheck_resolvet::resolve(), cpp_typecheck_resolvet::resolve_scope(), cpp_typecheck_resolvet::resolve_with_arguments(), remove_returnst::restore_returns(), rewrite_assignment(), goto_convertt::rewrite_boolean(), goto_symext::rewrite_quantifiers(), rewrite_union(), rewrite_union_address_of(), Parser::rInitializeExpr(), Parser::rIntegralDeclaration(), object_descriptor_exprt::root_object(), Parser::rTemplateArgs(), Parser::rTypeName(), Parser::rTypePredicate(), goto_program2codet::scan_for_varargs(), template_mapt::set(), set(), set_class_identifier(), prop_conv_solvert::set_equality_to_true(), set_internal_dynamic_object(), cpp_declarationt::set_specialization_of(), boolbvt::set_to(), string_refinementt::set_to(), prop_conv_solvert::set_to(), smt2_convt::set_to(), should_init_symbol(), show_call_sequences(), cpp_typecheck_resolvet::show_identifiers(), side_effect_expr_function_callt::side_effect_expr_function_callt(), sign_of_expr(), invariant_sett::simplify(), simplify_exprt::simplify_abs(), simplify_exprt::simplify_address_of_arg(), simplify_exprt::simplify_bitnot(), simplify_exprt::simplify_bitwise(), simplify_exprt::simplify_boolean(), simplify_exprt::simplify_bswap(), simplify_exprt::simplify_byte_extract(), simplify_exprt::simplify_byte_update(), simplify_exprt::simplify_concatenation(), simplify_exprt::simplify_dereference(), simplify_exprt::simplify_div(), simplify_exprt::simplify_dynamic_object(), qdimacs_coret::simplify_extractbits(), simplify_exprt::simplify_extractbits(), simplify_exprt::simplify_floatbv_op(), simplify_exprt::simplify_floatbv_typecast(), simplify_exprt::simplify_ieee_float_relation(), simplify_exprt::simplify_if(), simplify_exprt::simplify_if_branch(), simplify_exprt::simplify_if_cond(), simplify_exprt::simplify_if_implies(), simplify_exprt::simplify_if_preorder(), simplify_exprt::simplify_if_recursive(), simplify_exprt::simplify_index(), simplify_exprt::simplify_inequality(), simplify_exprt::simplify_inequality_address_of(), simplify_exprt::simplify_inequality_constant(), simplify_exprt::simplify_inequality_not_constant(), simplify_exprt::simplify_inequality_pointer_object(), simplify_exprt::simplify_invalid_pointer(), simplify_json_expr(), simplify_exprt::simplify_member(), simplify_exprt::simplify_minus(), simplify_exprt::simplify_mod(), simplify_exprt::simplify_node(), simplify_exprt::simplify_node_preorder(), simplify_exprt::simplify_not(), simplify_exprt::simplify_object(), simplify_exprt::simplify_object_size(), simplify_exprt::simplify_plus(), simplify_exprt::simplify_pointer_object(), simplify_exprt::simplify_pointer_offset(), simplify_exprt::simplify_popcount(), simplify_exprt::simplify_rec(), simplify_exprt::simplify_shifts(), simplify_exprt::simplify_sign(), simplify_exprt::simplify_typecast(), simplify_exprt::simplify_unary_minus(), simplify_exprt::simplify_update(), simplify_exprt::simplify_with(), size_of_expr(), skip_typecast(), symex_slicet::slice_assignment(), symex_slice_by_tracet::slice_by_trace(), symex_slicet::slice_decl(), symex_slice_by_tracet::slice_SSA_steps(), sort_and_join(), select_pointer_typet::specialize_generics(), cpp_typecheckt::standard_conversion_array_to_pointer(), cpp_typecheckt::standard_conversion_boolean(), cpp_typecheckt::standard_conversion_floating_integral_conversion(), cpp_typecheckt::standard_conversion_floating_point_conversion(), cpp_typecheckt::standard_conversion_integral_conversion(), cpp_typecheckt::standard_conversion_integral_promotion(), cpp_typecheckt::standard_conversion_lvalue_to_rvalue(), cpp_typecheckt::standard_conversion_pointer(), cpp_typecheckt::standard_conversion_pointer_to_member(), cpp_typecheckt::standard_conversion_qualification(), cpp_typecheckt::standard_conversion_sequence(), cpp_typecheckt::static_and_dynamic_initialization(), static_lifetime_init(), cpp_typecheckt::static_typecast(), postconditiont::strengthen(), invariant_sett::strengthen_rec(), string_from_ns(), string_identifiers_resolution_from_equations(), string_of_array(), substitute_array_access(), substitute_array_lists(), substitute_rec(), sum_expr(), sum_over_map(), member_exprt::symbol(), goto_symext::symex_allocate(), goto_symext::symex_assign(), goto_symext::symex_assign_array(), goto_symext::symex_assign_byte_extract(), goto_symext::symex_assign_rec(), goto_symext::symex_assign_struct_member(), goto_symext::symex_cpp_new(), goto_symext::symex_dead(), goto_symext::symex_decl(), goto_symext::symex_function_call_symbol(), goto_symext::symex_goto(), goto_symext::symex_macro(), template_subtype(), cpp_typecheckt::template_suffix(), cpp_typecheckt::this_struct_type(), to_abs_expr(), to_address_of_expr(), to_and_expr(), to_ansi_c_declaration(), to_ansi_c_declarator(), string_constantt::to_array_expr(), to_array_expr(), to_array_of_expr(), to_array_string_expr(), to_array_type(), to_bitand_expr(), to_bitnot_expr(), to_bitor_expr(), to_bitvector_type(), to_bitxor_expr(), to_bswap_expr(), to_bv_type(), to_byte_extract_big_endian_expr(), to_byte_extract_little_endian_expr(), to_byte_update_big_endian_expr(), to_byte_update_little_endian_expr(), to_c_bit_field_type(), to_c_bool_type(), to_c_enum_tag_type(), to_c_enum_type(), to_char_pair(), to_class_type(), to_code(), to_code_type(), to_complex_expr(), to_complex_type(), to_concatenation_expr(), to_constant_expr(), to_cpp_declaration(), to_cpp_enum_type(), to_cpp_name(), to_cpp_template_args_non_tc(), to_cpp_template_args_tc(), to_dereference_expr(), to_div_expr(), to_dynamic_object_expr(), to_enumeration_type(), to_equal_expr(), polynomialt::to_expr(), ansi_c_languaget::to_expr(), to_extractbit_expr(), to_extractbits_expr(), to_factorial_expr(), to_factorial_power_expr(), to_fixedbv_type(), to_floatbv_type(), to_floatbv_typecast_expr(), to_function_application_expr(), to_ieee_float_equal_expr(), to_ieee_float_notequal_expr(), to_if_expr(), to_implies_expr(), to_incomplete_array_type(), to_index_designator(), to_index_expr(), to_integer(), to_isfinite_expr(), to_isinf_expr(), to_isnan_expr(), to_isnormal_expr(), to_java_class_type(), to_java_generic_type(), to_jsil_union_type(), to_let_expr(), to_literal_expr(), to_mathematical_function_type(), to_member_designator(), to_member_expr(), to_minus_expr(), to_mod_expr(), to_mult_expr(), to_nondet_symbol_expr(), to_not_expr(), to_notequal_expr(), to_object_descriptor_expr(), to_or_expr(), to_plus_expr(), to_pointer_type(), to_popcount_expr(), to_power_expr(), to_range_type(), to_rational(), to_reference_type(), to_rem_expr(), to_replication_expr(), to_side_effect_expr(), to_side_effect_expr_function_call(), to_side_effect_expr_throw(), to_signedbv_type(), smt2_convt::to_smt2_symbol(), to_ssa_expr(), to_string_constant(), to_string_expr(), to_string_not_contains_constraint(), to_string_type(), to_struct_expr(), to_struct_tag_type(), to_struct_type(), to_struct_union_type(), ansi_c_declarationt::to_symbol(), to_symbol_expr(), to_symbol_type(), to_tag_type(), to_template_type(), to_trans_expr(), to_typecast_expr(), to_unary_minus_expr(), to_union_expr(), to_union_tag_type(), to_union_type(), to_unsignedbv_type(), to_update_expr(), to_vector_expr(), to_vector_type(), to_with_expr(), to_xor_expr(), trace_value_binary(), custom_bitvector_domaint::transform(), uncaught_exceptions_domaint::transform(), transt::transt(), goto_symext::trigger_auto_object(), remove_const_function_pointerst::try_resolve_expression(), constant_propagator_domaint::two_way_propagate_rec(), smt2_convt::type2id(), type2name(), type2name_symbol(), dereferencet::type_compatible(), boolbvt::type_conversion(), type_eq(), linkingt::type_to_string_verbose(), c_typecheck_baset::typecheck_arithmetic_pointer(), c_typecheck_baset::typecheck_array_type(), c_typecheck_baset::typecheck_c_bit_field_type(), c_typecheck_baset::typecheck_c_enum_tag_type(), c_typecheck_baset::typecheck_c_enum_type(), cpp_typecheckt::typecheck_cast_expr(), c_typecheck_baset::typecheck_code(), c_typecheck_baset::typecheck_code_type(), cpp_typecheckt::typecheck_compound_bases(), c_typecheck_baset::typecheck_compound_body(), cpp_typecheckt::typecheck_compound_body(), cpp_typecheckt::typecheck_compound_declarator(), c_typecheck_baset::typecheck_compound_type(), cpp_typecheckt::typecheck_compound_type(), c_typecheck_baset::typecheck_custom_type(), c_typecheck_baset::typecheck_decl(), cpp_typecheckt::typecheck_decl(), c_typecheck_baset::typecheck_declaration(), cpp_typecheckt::typecheck_enum_type(), jsil_typecheckt::typecheck_exp_binary_equal(), java_bytecode_typecheckt::typecheck_expr(), c_typecheck_baset::typecheck_expr(), cpp_typecheckt::typecheck_expr(), c_typecheck_baset::typecheck_expr_address_of(), cpp_typecheckt::typecheck_expr_address_of(), jsil_typecheckt::typecheck_expr_base(), jsil_typecheckt::typecheck_expr_binary_arith(), c_typecheck_baset::typecheck_expr_binary_arithmetic(), cpp_typecheckt::typecheck_expr_binary_arithmetic(), jsil_typecheckt::typecheck_expr_binary_boolean(), c_typecheck_baset::typecheck_expr_binary_boolean(), jsil_typecheckt::typecheck_expr_binary_compare(), c_typecheck_baset::typecheck_expr_builtin_offsetof(), jsil_typecheckt::typecheck_expr_concatenation(), jsil_typecheckt::typecheck_expr_constant(), cpp_typecheckt::typecheck_expr_cpp_name(), jsil_typecheckt::typecheck_expr_delete(), cpp_typecheckt::typecheck_expr_delete(), c_typecheck_baset::typecheck_expr_dereference(), cpp_typecheckt::typecheck_expr_dereference(), cpp_typecheckt::typecheck_expr_explicit_constructor_call(), cpp_typecheckt::typecheck_expr_explicit_typecast(), jsil_typecheckt::typecheck_expr_field(), c_typecheck_baset::typecheck_expr_function_identifier(), cpp_typecheckt::typecheck_expr_function_identifier(), jsil_typecheckt::typecheck_expr_has_field(), jsil_typecheckt::typecheck_expr_index(), c_typecheck_baset::typecheck_expr_index(), jsil_typecheckt::typecheck_expr_main(), c_typecheck_baset::typecheck_expr_main(), cpp_typecheckt::typecheck_expr_main(), c_typecheck_baset::typecheck_expr_member(), cpp_typecheckt::typecheck_expr_member(), cpp_typecheckt::typecheck_expr_new(), c_typecheck_baset::typecheck_expr_operands(), c_typecheck_baset::typecheck_expr_pointer_arithmetic(), jsil_typecheckt::typecheck_expr_proto_field(), jsil_typecheckt::typecheck_expr_proto_obj(), c_typecheck_baset::typecheck_expr_ptrmember(), cpp_typecheckt::typecheck_expr_ptrmember(), jsil_typecheckt::typecheck_expr_ref(), c_typecheck_baset::typecheck_expr_rel(), c_typecheck_baset::typecheck_expr_rel_vector(), c_typecheck_baset::typecheck_expr_shifts(), c_typecheck_baset::typecheck_expr_side_effect(), jsil_typecheckt::typecheck_expr_side_effect_throw(), c_typecheck_baset::typecheck_expr_sizeof(), cpp_typecheckt::typecheck_expr_sizeof(), jsil_typecheckt::typecheck_expr_subtype(), java_bytecode_typecheckt::typecheck_expr_symbol(), c_typecheck_baset::typecheck_expr_symbol(), cpp_typecheckt::typecheck_expr_this(), cpp_typecheckt::typecheck_expr_trinary(), c_typecheck_baset::typecheck_expr_typecast(), c_typecheck_baset::typecheck_expr_unary_arithmetic(), jsil_typecheckt::typecheck_expr_unary_boolean(), c_typecheck_baset::typecheck_expr_unary_boolean(), jsil_typecheckt::typecheck_expr_unary_num(), jsil_typecheckt::typecheck_expr_unary_string(), cpp_typecheckt::typecheck_friend_declaration(), jsil_typecheckt::typecheck_function_call(), c_typecheck_baset::typecheck_function_call_arguments(), cpp_typecheckt::typecheck_function_expr(), c_typecheck_baset::typecheck_gcc_computed_goto(), c_typecheck_baset::typecheck_ifthenelse(), cpp_typecheckt::typecheck_ifthenelse(), cpp_typecheckt::typecheck_member_function(), cpp_typecheckt::typecheck_member_initializer(), cpp_typecheckt::typecheck_method_application(), cpp_typecheckt::typecheck_method_bodies(), c_typecheck_baset::typecheck_new_symbol(), jsil_typecheckt::typecheck_non_type_symbol(), c_typecheck_baset::typecheck_redefinition_non_type(), c_typecheck_baset::typecheck_redefinition_type(), c_typecheck_baset::typecheck_return(), c_typecheck_baset::typecheck_side_effect_assignment(), c_typecheck_baset::typecheck_side_effect_function_call(), cpp_typecheckt::typecheck_side_effect_function_call(), cpp_typecheckt::typecheck_switch(), c_typecheck_baset::typecheck_symbol(), jsil_typecheckt::typecheck_symbol_expr(), cpp_typecheckt::typecheck_template_args(), cpp_typecheckt::typecheck_template_parameters(), java_bytecode_typecheckt::typecheck_type(), jsil_typecheckt::typecheck_type(), c_typecheck_baset::typecheck_type(), cpp_typecheckt::typecheck_type(), c_typecheck_baset::typecheck_typeof_type(), c_typecheck_baset::typecheck_vector_type(), cpp_typecheckt::typecheck_while(), interpretert::unbounded_size(), undefined_function_abort_path(), goto_checkt::undefined_shift_check(), underlying_width(), remove_returnst::undo_function_calls(), smt2_convt::unflatten(), unpack_rec(), unsigned_from_ns(), jsil_typecheckt::update_expr_type(), update_exprt::update_exprt(), update_index_set(), smt2_convt::use_array_theory(), cpp_typecheckt::user_defined_conversion_sequence(), value_set_dereferencet::valid_check(), validate_expr(), string_abstractiont::value_assignments(), postconditiont::weaken(), cpp_convert_typet::write(), ansi_c_convert_typet::write(), irep_serializationt::write_irep(), xml(), and cpp_typecheckt::zero_initializer().
|
inline |
Definition at line 195 of file irep.h.
References irept::dt::data, and write().
|
inline |
Definition at line 192 of file irep.h.
References id2string(), and read().
Referenced by arrayst::add_array_constraints(), goto_symext::address_arithmetic(), value_set_fit::assign_rec(), value_sett::assign_rec(), goto_checkt::bounds_check(), value_set_dereferencet::build_reference_to(), mm2cppt::check_acyclic(), goto_checkt::check_rec(), arrayst::collect_arrays(), compute_pointer_offset(), convert(), boolbvt::convert_add_sub(), smt2_convt::convert_address_of_rec(), prop_conv_solvert::convert_bool(), expr2ct::convert_byte_extract(), expr2ct::convert_byte_update(), smt2_convt::convert_constant(), smt2_convt::convert_div(), smt2_convt::convert_expr(), boolbvt::convert_floatbv_op(), smt2_convt::convert_floatbv_plus(), smt2_convt::convert_floatbv_typecast(), json_irept::convert_from_irep(), smt2_convt::convert_member(), smt2_convt::convert_minus(), smt2_convt::convert_mod(), smt2_convt::convert_mult(), boolbvt::convert_overflow(), smt2_convt::convert_plus(), bv_pointerst::convert_pointer_type(), expr2ct::convert_rec(), smt2_convt::convert_relation(), boolbvt::convert_rest(), smt2_convt::convert_type(), smt2_convt::convert_typecast(), smt2_convt::convert_with(), expr2ct::convert_with_precedence(), dereferencet::dereference_rec(), goto_program_dereferencet::dereference_rec(), goto_checkt::div_by_zero_check(), smt2_convt::find_symbols(), flatten_byte_update(), cpp_namet::get_base_name(), rw_range_sett::get_objects_rec(), value_set_fivrnst::get_reference_set_rec(), value_sett::get_reference_set_rec(), value_set_fit::get_reference_set_sharing_rec(), value_set_fivrt::get_reference_set_sharing_rec(), value_set_fit::get_value_set_rec(), value_sett::get_value_set_rec(), goto_checkt::integer_overflow_check(), irep2lisp(), irep2name(), exprt::is_one(), exprt::is_zero(), goto_checkt::mod_by_zero_check(), invariant_sett::modifies(), goto_checkt::nan_check(), format_constantt::operator()(), overflow_instrumentert::overflow_expr(), smt2_convt::parse_literal(), goto_checkt::pointer_overflow_check(), goto_checkt::pointer_rel_check(), pretty(), goto_symext::symex_assign_array(), goto_symext::symex_assign_rec(), type2name(), linkingt::type_to_string_verbose(), cpp_typecheckt::typecheck_compound_type(), c_typecheck_baset::typecheck_redefinition_type(), and goto_checkt::undefined_shift_check().
|
inlinestaticprotected |
|
inline |
Definition at line 102 of file irep.h.
References id().
Referenced by string_abstractiont::abstract_char_assign(), string_abstractiont::abstract_function_call(), string_abstractiont::abstract_pointer_assign(), disjunctive_polynomial_accelerationt::accelerate(), polynomial_acceleratort::accelerate(), add_padding_gcc(), string_abstractiont::add_str_arguments(), goto_symext::add_to_lhs(), pointer_arithmetict::add_to_offset(), linkingt::adjust_object_type_rec(), alignment(), allocate_dynamic_object(), ansi_c_entry_point(), code_contractst::apply_contract(), cpp_typecheck_resolvet::apply_template_args(), disjunctive_polynomial_accelerationt::assert_for_values(), polynomial_acceleratort::assert_for_values(), value_set_fit::assign(), value_set_fit::assign_rec(), base_type_rec(), simplify_exprt::bits2expr(), goto_checkt::bounds_check(), value_set_dereferencet::bounds_check(), ansi_c_declaratort::build(), string_abstractiont::build(), string_abstractiont::build_abstraction_type_rec(), string_abstractiont::build_symbol(), boolbvt::bv_get_unbounded_array(), c_sizeof_type_rec(), check_apply_invariants(), goto_convertt::clean_expr(), goto_program2codet::cleanup_code_ifthenelse(), cpp_declarator_convertert::combine_types(), cpp_declarator_convertert::convert(), expr2ct::convert_code_dowhile(), expr2ct::convert_code_for(), expr2ct::convert_code_ifthenelse(), expr2ct::convert_code_while(), goto_convertt::convert_for(), goto_convert_functionst::convert_function(), cpp_typecheckt::convert_function(), dump_ct::convert_global_variable(), expr2ct::convert_Hoare(), goto_convertt::convert_ifthenelse(), boolbvt::convert_index(), cpp_typecheckt::convert_initializer(), goto_convertt::convert_loop_invariant(), expr2ct::convert_member(), expr2ct::convert_object_descriptor(), cpp_typecheckt::convert_pmop(), expr2ct::convert_rec(), cpp_typecheck_resolvet::convert_template_parameter(), boolbvt::convert_update_rec(), cpp_typecheckt::cpp_constructor(), stub_global_initializer_factoryt::create_stub_global_initializer_symbols(), smt2_convt::define_object_size(), value_set_dereferencet::dereference(), dereferencet::dereference_plus(), c_typecheck_baset::designator_enter(), goto_checkt::div_by_zero_check(), goto_convertt::do_cpp_new(), c_typecheck_baset::do_designated_initializer(), value_set_fit::do_end_function(), value_set_fivrnst::do_end_function(), value_set_fivrt::do_end_function(), value_sett::do_end_function(), goto_convertt::do_function_call(), goto_convertt::do_function_call_symbol(), c_typecheck_baset::do_initializer(), c_typecheck_baset::do_initializer_list(), c_typecheck_baset::do_initializer_rec(), bv_pointerst::do_postponed(), goto_convertt::do_prob_coin(), goto_convertt::do_prob_uniform(), string_instrumentationt::do_strerror(), linkingt::duplicate_code_symbol(), linkingt::duplicate_object_symbol(), linkingt::duplicate_type_symbol(), expr_initializert< nondet >::expr_initializer_rec(), filter_out(), remove_function_pointerst::fix_return_type(), namespace_baset::follow_macros(), generate_ansi_c_start_function(), smt2_convt::get(), java_string_library_preprocesst::get_primitive_value_of_object(), local_may_aliast::get_rec(), cpp_declarator_convertert::handle_initializer(), c_typecheck_baset::increment_designator(), c_typecheck_baset::is_complete_type(), cpp_declarationt::is_empty(), array_typet::is_incomplete(), java_static_lifetime_init(), jsil_entry_point(), remove_java_newt::lower_java_new(), remove_java_newt::lower_java_new_array(), string_abstractiont::make_decl_and_def(), pointer_arithmetict::make_pointer(), jsil_typecheckt::make_type_compatible(), cpp_typecheck_fargst::match(), string_abstractiont::member(), member_offset_expr(), cpp_declaratort::merge_type(), Parser::merge_types(), goto_checkt::mod_by_zero_check(), move_label_ifthenelse(), cpp_typecheckt::move_member_initializers(), cpp_declarationt::name_anon_struct_union(), linkingt::needs_renaming_type(), graphml_witnesst::operator()(), operator<<(), value_sett::output(), goto_programt::output_instruction(), goto_inlinet::parameter_assignments(), goto_symext::parameter_assignments(), smt2_convt::parse_union(), pretty_print_invariant_with_irep(), memory_model_tsot::program_order(), Parser::rCastOperatorName(), Parser::rDeclarator(), cpp_convert_typet::read_function_type(), dereferencet::read_object(), ansi_c_convert_typet::read_rec(), cover_basic_blockst::report_block_anomalies(), cpp_typecheck_resolvet::resolve(), Parser::rOtherDeclaration(), Parser::rSimpleDeclaration(), Parser::rTypeSpecifier(), simplify_exprt::simplify_byte_update(), simplify_exprt::simplify_member(), simplify_exprt::simplify_mult(), simplify_exprt::simplify_unary_minus(), size_of_expr(), cpp_typecheckt::standard_conversion_pointer_to_member(), static_lifetime_init(), cpp_typecheckt::static_typecast(), substitute_array_access(), sum_over_map(), goto_symext::symex_allocate(), goto_symext::symex_gcc_builtin_va_arg_next(), goto_symext::symex_start_thread(), symex_bmct::symex_step(), trace_value(), c_typecheck_baset::typecheck_c_enum_tag_type(), c_typecheck_baset::typecheck_c_enum_type(), cpp_typecheckt::typecheck_class_template(), cpp_typecheckt::typecheck_compound_declarator(), c_typecheck_baset::typecheck_compound_type(), cpp_typecheckt::typecheck_enum_type(), c_typecheck_baset::typecheck_expr_builtin_offsetof(), cpp_typecheckt::typecheck_expr_cpp_name(), jsil_typecheckt::typecheck_expr_main(), c_typecheck_baset::typecheck_expr_main(), cpp_typecheckt::typecheck_expr_main(), c_typecheck_baset::typecheck_expr_member(), cpp_typecheckt::typecheck_expr_member(), c_typecheck_baset::typecheck_expr_sizeof(), c_typecheck_baset::typecheck_expr_typecast(), c_typecheck_baset::typecheck_for(), c_typecheck_baset::typecheck_function_call_arguments(), jsil_typecheckt::typecheck_ifthenelse(), c_typecheck_baset::typecheck_ifthenelse(), cpp_typecheckt::typecheck_member_initializer(), c_typecheck_baset::typecheck_redefinition_non_type(), cpp_typecheckt::typecheck_side_effect_function_call(), c_typecheck_baset::typecheck_side_effect_statement_expression(), cpp_typecheckt::typecheck_type(), goto_checkt::undefined_shift_check(), cover_basic_blockst::update_covered_lines(), jsil_typecheckt::update_expr_type(), cpp_typecheckt::user_defined_conversion_sequence(), value_set_dereferencet::valid_check(), and value_sets_to_xml().
|
inline |
Definition at line 103 of file irep.h.
References id().
Referenced by string_abstractiont::abstract_char_assign(), code_contractst::add_contract_check(), ansi_c_parsert::add_declarator(), string_abstractiont::add_dummy_symbol_and_value(), add_padding_gcc(), goto_symext::add_to_lhs(), linkingt::adjust_object_type_rec(), c_typecheck_baset::apply_asm_label(), value_sett::apply_code_rec(), code_contractst::apply_contract(), cpp_typecheck_resolvet::apply_template_args(), symex_target_equationt::assignment(), goto_checkt::bounds_check(), local_may_aliast::build(), local_bitvector_analysist::build(), build_full_lhs_rec(), build_goto_trace(), build_object_descriptor_rec(), build_sizeof_expr(), c_sizeof_type_rec(), string_abstractiont::char_assign(), check_and_replace_target(), cpp_typecheckt::check_fixed_size_array(), cpp_typecheckt::check_member_initializers(), goto_checkt::check_rec(), goto_convertt::clean_expr(), goto_program2codet::cleanup_code(), goto_program2codet::cleanup_code_ifthenelse(), dump_ct::cleanup_decl(), goto_program2codet::cleanup_expr(), smt2_solvert::command(), struct_union_typet::component_type(), _rw_set_loct::compute(), show_goto_functions_jsont::convert(), show_goto_functions_xmlt::convert(), cpp_declarator_convertert::convert(), cpp_typecheckt::convert(), convert(), expr2javat::convert_code_function_call(), expr2ct::convert_code_function_call(), expr2ct::convert_constant(), goto_convertt::convert_cpp_delete(), convert_decl(), goto_convertt::convert_decl(), goto_convertt::convert_expression(), goto_convertt::convert_for(), dump_ct::convert_global_variable(), cpp_typecheck_resolvet::convert_identifier(), cpp_typecheck_resolvet::convert_identifiers(), goto_convertt::convert_ifthenelse(), cpp_typecheckt::convert_initializer(), goto_convertt::convert_label(), java_bytecode_languaget::convert_lazy_method(), cpp_declarator_convertert::convert_new_symbol(), cpp_typecheckt::convert_non_template_declaration(), expr2ct::convert_rec(), expr2cppt::convert_rec(), java_bytecode_languaget::convert_single_method(), smt2_convt::convert_type(), expr2ct::convert_with(), goto_convertt::cpp_new_initializer(), symex_target_equationt::decl(), goto_program_dereferencet::dereference_instruction(), goto_convertt::do_atomic_begin(), goto_convertt::do_atomic_end(), string_instrumentationt::do_fscanf(), goto_convertt::do_function_call_symbol(), remove_returnst::do_function_calls(), c_typecheck_baset::do_initializer(), goto_convertt::do_printf(), goto_convertt::do_scanf(), string_instrumentationt::do_snprintf(), string_instrumentationt::do_sprintf(), cpp_typecheckt::dtor(), linkingt::duplicate_code_symbol(), linkingt::duplicate_type_symbol(), dynamic_object_upper_bound(), cpp_typecheckt::dynamic_typecast(), lazy_goto_functions_mapt::ensure_entry_converted(), interpretert::execute_function_call(), expressions_read(), expressions_written(), cpp_typecheck_resolvet::filter_for_named_scopes(), exprt::find_source_location(), find_symbols(), flatten_byte_extract(), memory_model_sct::from_read(), ansi_c_declarationt::full_type(), remove_virtual_functionst::get_child_functions_rec(), get_class_literal_initializer(), cpp_typecheckt::get_component(), get_component_rec(), function_modifiest::get_modifies(), havoc_loopst::get_modifies(), value_set_fit::get_value_set_rec(), goto_rw(), cpp_typecheck_resolvet::guess_function_template_args(), cpp_enum_typet::has_body(), struct_union_typet::has_component(), template_parametert::has_default_argument(), code_typet::parametert::has_default_value(), code_ifthenelset::has_else_case(), code_returnt::has_return_value(), cpp_enum_typet::has_tag(), rename_symbolt::have_to_rename(), replace_symbolt::have_to_replace(), goto_inlinet::insert_function_body(), cpp_typecheckt::instantiate_template(), java_bytecode_instrumentt::instrument_code(), array_typet::is_complete(), is_not_zero(), java_static_lifetime_init(), ui_message_handlert::json_ui_msg(), remove_java_newt::lower_java_new(), string_abstractiont::make_decl_and_def(), Parser::make_subtype(), string_abstractiont::make_type(), value_set_dereferencet::memory_model_bytes(), mm_io(), model_argc_argv(), linkingt::needs_renaming_type(), cpp_typecheckt::new_temporary(), object_lower_bound(), object_upper_bound(), bmc_covert::operator()(), cpp_typecheckt::operator_is_overloaded(), Parser::optPtrOperator(), goto_checkt::pointer_validity_check(), Parser::rDeclaration(), Parser::rDeclarationStatement(), Parser::rDeclarator(), cpp_convert_typet::read_function_type(), dereferencet::read_object(), remove_calls_no_bodyt::remove_call_no_body(), remove_function_pointerst::remove_function_pointer(), remove_internal_symbols(), goto_convertt::remove_temporary_object(), rename_symbolt::rename(), replace_symbolt::replace(), replace_location(), goto_inlinet::replace_return(), cpp_typecheck_resolvet::resolve(), cpp_typecheck_resolvet::resolve_scope(), goto_symext::return_assignment(), Parser::rPrimaryExpr(), Parser::rSimpleDeclaration(), show_symbol_table_brief_plain(), language_uit::show_symbol_table_plain(), show_symbol_table_plain(), bmct::show_vcc_json(), invariant_sett::simplify(), simplify_exprt::simplify_byte_extract(), simplify_exprt::simplify_byte_update(), simplify_exprt::simplify_div(), simplify_exprt::simplify_member(), simplify_exprt::simplify_minus(), simplify_exprt::simplify_mod(), simplify_exprt::simplify_mult(), simplify_exprt::simplify_object_size(), simplify_exprt::simplify_plus(), simplify_exprt::simplify_typecast(), cpp_typecheckt::standard_conversion_pointer(), cpp_typecheckt::static_and_dynamic_initialization(), static_lifetime_init(), cpp_typecheckt::static_typecast(), sum_over_map(), goto_symext::symex_allocate(), goto_symext::symex_dead(), goto_symext::symex_decl(), goto_symext::symex_function_call_code(), goto_symext::symex_step(), cpp_typecheckt::this_struct_type(), trace_value(), interval_domaint::transform(), rd_range_domaint::transform(), rd_range_domaint::transform_end_function(), rd_range_domaint::transform_function_call(), c_typecheck_baset::typecheck_array_type(), c_typecheck_baset::typecheck_c_enum_type(), cpp_typecheckt::typecheck_class_template(), java_bytecode_typecheckt::typecheck_code(), cpp_typecheckt::typecheck_compound_declarator(), c_typecheck_baset::typecheck_compound_type(), cpp_typecheckt::typecheck_compound_type(), c_typecheck_baset::typecheck_decl(), cpp_typecheckt::typecheck_decl(), c_typecheck_baset::typecheck_declaration(), cpp_typecheckt::typecheck_expr_delete(), cpp_typecheckt::typecheck_expr_dereference(), c_typecheck_baset::typecheck_expr_main(), cpp_typecheckt::typecheck_expr_member(), cpp_typecheckt::typecheck_expr_this(), c_typecheck_baset::typecheck_for(), cpp_typecheckt::typecheck_friend_declaration(), c_typecheck_baset::typecheck_function_body(), jsil_typecheckt::typecheck_function_call(), cpp_typecheckt::typecheck_function_template(), cpp_typecheckt::typecheck_member_function(), cpp_typecheckt::typecheck_member_initializer(), cpp_typecheckt::typecheck_method_bodies(), c_typecheck_baset::typecheck_new_symbol(), c_typecheck_baset::typecheck_redefinition_non_type(), c_typecheck_baset::typecheck_side_effect_function_call(), cpp_typecheckt::typecheck_side_effect_function_call(), c_typecheck_baset::typecheck_spec_expr(), cpp_typecheckt::typecheck_template_parameters(), c_typecheck_baset::typecheck_type(), cpp_typecheckt::typecheck_type(), cpp_typecheckt::user_defined_conversion_sequence(), ansi_c_convert_typet::write(), ui_message_handlert::xml_ui_msg(), and cpp_typecheckt::zero_initializer().
|
inline |
Definition at line 243 of file irep.h.
References get_nil_irep().
Referenced by shared_bufferst::add(), string_abstractiont::add_argument(), string_abstractiont::add_dummy_symbol_and_value(), add_failed_symbol(), shared_bufferst::add_initialization(), goto_symext::add_to_lhs(), ansi_c_declaratort::build(), build_goto_trace(), string_abstractiont::build_new_symbol(), string_abstractiont::build_symbol_constant(), string_abstractiont::build_unknown(), goto_convertt::clean_expr(), goto_program2codet::cleanup_code_ifthenelse(), ansi_c_convert_typet::clear(), symbolt::clear(), goto_programt::instructiont::clear(), code_function_callt::code_function_callt(), code_ifthenelset::code_ifthenelset(), code_returnt::code_returnt(), cpp_typecheckt::convert(), goto_program2codet::convert_assign_varargs(), goto_convertt::convert_cpp_delete(), goto_convert_functionst::convert_function(), cpp_typecheckt::convert_function(), goto_program2codet::convert_goto_while(), cpp_typecheck_resolvet::convert_identifier(), java_bytecode_convert_methodt::convert_invoke(), java_bytecode_convert_methodt::convert_monitorenter(), java_bytecode_convert_methodt::convert_monitorexit(), goto_convertt::convert_return(), boolbvt::convert_update_rec(), cpp_typecheckt::cpp_constructor(), cpp_declaratort::cpp_declaratort(), cpp_typecheckt::cpp_destructor(), cpp_namespace_spect::cpp_namespace_spect(), create_stub_global_symbol(), cpp_typecheckt::default_assignop(), cpp_typecheckt::default_assignop_value(), cpp_typecheckt::default_cpctor(), cpp_typecheckt::default_ctor(), cpp_typecheckt::default_dtor(), c_typecheck_baset::designator_enter(), remove_returnst::do_function_calls(), cpp_typecheckt::do_not_typechecked(), linkingt::duplicate_code_symbol(), memory_model_sct::from_read(), function_to_call(), remove_asmt::gcc_asm_function_call(), generate_ansi_c_start_function(), generate_java_start_function(), goto_trace_stept::goto_trace_stept(), smt2_convt::identifiert::identifiert(), escape_analysist::insert_cleanup(), introduce_temporaries(), jsil_entry_point(), lisp2irep(), Parser::optIntegralTypeOrClassSpec(), Parser::optPtrOperator(), pointer_arithmetict::pointer_arithmetict(), ui_message_handlert::print(), Parser::rAllocateType(), Parser::rArgDeclaration(), Parser::rCastOperatorName(), Parser::rConstructorDecl(), Parser::rDeclaration(), Parser::rDeclarationStatement(), Parser::rDeclarator(), Parser::rDeclaratorWithInit(), read_bin_goto_object_v3(), goto_convertt::remove_assignment(), goto_convertt::remove_cpp_delete(), goto_convertt::remove_cpp_new(), remove_function(), goto_convertt::remove_function_call(), goto_convertt::remove_post(), goto_convertt::remove_pre(), goto_convertt::remove_side_effect(), goto_convertt::remove_statement_expression(), Parser::rEnumBody(), Parser::rEnumSpec(), cpp_typecheck_resolvet::resolve(), cpp_typecheck_resolvet::resolve_namespace(), cpp_typecheck_resolvet::resolve_scope(), Parser::rForStatement(), Parser::rIfStatement(), Parser::rSimpleDeclaration(), Parser::rTempArgDeclaration(), Parser::rTypedefUsing(), Parser::rTypeSpecifier(), bmct::setup(), simplify_exprt::simplify_byte_update(), symex_slice_by_tracet::slice_by_trace(), cpp_typecheckt::static_and_dynamic_initialization(), jsil_languaget::to_expr(), ansi_c_languaget::to_expr(), cpp_languaget::to_expr(), java_bytecode_languaget::to_expr(), cpp_typecheckt::typecheck_compound_declarator(), cpp_typecheckt::typecheck_compound_type(), cpp_typecheckt::typecheck_enum_type(), cpp_typecheckt::typecheck_expr_member(), c_typecheck_baset::typecheck_for(), cpp_typecheckt::typecheck_function_template(), cpp_typecheckt::typecheck_member_initializer(), cpp_typecheckt::typecheck_template_parameters(), and cpp_typecheckt::user_defined_conversion_sequence().
void irept::move_to_named_sub | ( | const irep_namet & | name, |
irept & | irep | ||
) |
void irept::move_to_sub | ( | irept & | irep | ) |
Definition at line 204 of file irep.cpp.
References detach(), get_nil_irep(), and get_sub().
Referenced by convert(), cpp_typecheckt::convert_anonymous_union(), cpp_typecheckt::default_cpctor(), cpp_typecheckt::default_ctor(), cpp_typecheckt::default_dtor(), cpp_typecheckt::dtor(), cpp_typecheckt::full_member_initialization(), lisp2irep(), Parser::rAttribute(), Parser::rMemberInitializers(), cpp_typecheckt::typecheck_friend_declaration(), and cpp_typecheckt::zero_initializer().
|
staticprotected |
Does the same as remove_ref, but using an explicit stack instead of recursion.
Definition at line 140 of file irep.cpp.
References irept::dt::comments, empty_d, INVARIANT, irept::dt::named_sub, irept::dt::ref_count, stack, and irept::dt::sub.
Referenced by remove_ref().
bool irept::operator< | ( | const irept & | other | ) | const |
defines ordering on the internal representation
Definition at line 566 of file irep.cpp.
References ordering().
Definition at line 146 of file irep.h.
References data, empty_d, irept::dt::ref_count, and remove_ref().
bool irept::operator== | ( | const irept & | other | ) | const |
bool irept::ordering | ( | const irept & | other | ) | const |
defines ordering on the internal representation
Definition at line 430 of file irep.cpp.
References compare(), and INVARIANT.
Referenced by operator<().
std::string irept::pretty | ( | unsigned | indent = 0 , |
unsigned | max_indent = 0 |
||
) | const |
Definition at line 641 of file irep.cpp.
References forall_irep, forall_named_irep, get_comments(), get_named_sub(), get_sub(), id2string(), id_string(), indent_str(), and to_string().
Referenced by arrayst::add_array_constraints_update(), arrayst::add_array_constraints_with(), compilet::add_written_cprover_symbols(), invariant_sett::apply_code(), value_set_fit::apply_code(), value_set_fivrnst::apply_code(), value_set_fivrt::apply_code(), assert_l1_renaming(), assert_l2_renaming(), value_set_fit::assign(), value_set_fivrnst::assign(), value_set_fivrt::assign(), value_sett::assign(), base_type_eqt::base_type_eq_rec(), value_set_dereferencet::bounds_check(), value_set_dereferencet::build_reference_to(), goto_checkt::check_rec(), goto_convertt::clean_expr(), arrayst::collect_arrays(), smt2_solvert::command(), boolbvt::convert_add_sub(), prop_conv_solvert::convert_bool(), boolbvt::convert_bv(), boolbvt::convert_constant(), boolbvt::convert_equality(), boolbvt::convert_extractbits(), boolbvt::convert_floatbv_op(), boolbvt::convert_if(), boolbvt::convert_member(), boolbvt::convert_struct(), boolbvt::convert_verilog_case_equality(), boolbvt::convert_with_struct(), value_set_dereferencet::dereference(), dereferencet::dereference_rec(), goto_program_dereferencet::dereference_rec(), value_set_dereferencet::dereference_type_compare(), interpretert::evaluate(), cpp_typecheck_resolvet::filter_for_named_scopes(), flatten_byte_update(), format_rec(), languaget::from_expr(), languaget::from_type(), goto_convertt::get_string_constant(), cpp_typecheck_resolvet::guess_template_args(), prop_conv_solvert::ignoring(), cpp_typecheckt::implicit_typecast(), java_generic_symbol_typet::java_generic_symbol_typet(), join_types(), jsil_typecheckt::make_type_compatible(), cpp_typecheck_fargst::match(), value_set_dereferencet::memory_model_bytes(), non_byte_alignedt::non_byte_alignedt(), non_const_array_sizet::non_const_array_sizet(), non_const_byte_extraction_sizet::non_const_byte_extraction_sizet(), non_constant_widtht::non_constant_widtht(), dereferencet::operator()(), cpp_declaratort::output(), jsil_declarationt::output(), cpp_declarationt::output(), ansi_c_declarationt::output(), goto_inlinet::parameter_assignments(), goto_symext::parameter_assignments(), pretty_print_invariant_with_irep(), print_struct_alignment_problems(), Parser::rClassBody(), cpp_convert_typet::read(), cpp_convert_typet::read_rec(), goto_convertt::remove_post(), goto_convertt::remove_pre(), remove_ref(), require_parse_tree::expected_instructiont::require_instructions_equal(), goto_symext::return_assignment(), goto_convertt::rewrite_boolean(), Parser::rExprStatement(), Parser::rIntegralDeclaration(), Parser::rTemplateDecl(), symbolt::show(), cpp_languaget::show_parse(), goto_symext::symex_goto(), languaget::type_to_name(), c_typecheck_baset::typecheck_array_type(), c_typecheck_baset::typecheck_code(), jsil_typecheckt::typecheck_expr_main(), c_typecheck_baset::typecheck_expr_main(), cpp_typecheckt::typecheck_expr_main(), cpp_typecheckt::typecheck_expr_typecast(), jsil_typecheckt::typecheck_non_type_symbol(), cpp_typecheckt::typecheck_type(), c_typecheck_baset::typecheck_vector_type(), unpack_rec(), and ansi_c_convert_typet::write().
|
inline |
Definition at line 334 of file irep.h.
References data.
Referenced by get_comments(), get_named_sub(), get_sub(), merged_irept::hash(), hash(), id(), id_string(), depth_iteratort::mutate(), irep_hash_container_baset::number(), merged_irept::operator<(), and merged_irept::operator==().
void irept::remove | ( | const irep_namet & | name | ) |
Definition at line 270 of file irep.cpp.
References get_comments(), get_named_sub(), and is_comment().
Referenced by cpp_typecheckt::cast_away_constness(), goto_program2codet::cleanup_code(), goto_program2codet::cleanup_expr(), dump_ct::cleanup_expr(), c_qualifierst::clear(), dump_ct::collect_typedefs_rec(), dump_ct::convert_compound(), cpp_typecheckt::convert_template_function_or_member_specialization(), cpp_typecheck_resolvet::guess_template_args(), c_typecastt::implicit_typecast_followed(), cpp_typecheckt::instantiate_template(), nondet_volatile_rhs(), dump_ct::operator()(), cpp_typecheckt::reference_binding(), goto_program2codet::remove_const(), code_typet::remove_ellipsis(), cpp_typecheckt::standard_conversion_lvalue_to_rvalue(), cpp_typecheckt::static_typecast(), c_typecheck_baset::typecheck_c_bit_field_type(), c_typecheck_baset::typecheck_c_enum_tag_type(), c_typecheck_baset::typecheck_c_enum_type(), cpp_typecheckt::typecheck_class_template_member(), cpp_typecheckt::typecheck_compound_body(), c_typecheck_baset::typecheck_compound_type(), cpp_typecheckt::typecheck_compound_type(), c_typecheck_baset::typecheck_custom_type(), cpp_typecheckt::typecheck_expr_delete(), c_typecheck_baset::typecheck_expr_main(), cpp_typecheckt::typecheck_expr_member(), cpp_typecheckt::typecheck_expr_sizeof(), cpp_typecheckt::typecheck_member_initializer(), cpp_typecheckt::typecheck_method_application(), cpp_typecheckt::typecheck_side_effect_function_call(), and c_qualifierst::write().
|
staticprotected |
Definition at line 100 of file irep.cpp.
References irept::dt::clear(), irept::dt::data, empty_d, nonrecursive_destructor(), PRECONDITION, pretty(), and irept::dt::ref_count.
Referenced by detach(), operator=(), and ~irept().
|
inline |
Definition at line 214 of file irep.h.
Referenced by string_abstractiont::abstract_function_call(), cpp_typecheckt::add_base_components(), add_failed_symbol(), cpp_typecheckt::add_implicit_dereference(), jsil_declarationt::add_returns(), ansi_c_parsert::add_tag_with_body(), cpp_typecheckt::add_this_to_method_type(), jsil_declarationt::add_throws(), approximate_nondet_rec(), value_set_fit::assign(), value_set_fivrnst::assign(), value_set_fivrt::assign(), build_class_name(), build_sizeof_expr(), template_mapt::build_unassigned(), char16_t_type(), char32_t_type(), char_type(), checked_dereference(), cpp_typecheckt::class_template_symbol(), dump_ct::cleanup_expr(), java_string_library_preprocesst::code_assign_java_string_to_string_expr(), cpp_declarator_convertert::convert(), java_bytecode_convert_classt::convert(), java_bytecode_convert_methodt::convert(), java_bytecode_convert_methodt::convert_aload(), cpp_typecheckt::convert_anon_struct_union_member(), cpp_typecheckt::convert_anonymous_union(), goto_convertt::convert_assert(), java_bytecode_convert_methodt::convert_astore(), java_bytecode_convert_methodt::convert_athrow(), convert_float_literal(), goto_convert_functionst::convert_function(), cpp_typecheckt::convert_function(), cpp_typecheck_resolvet::convert_identifier(), cpp_typecheckt::convert_initializer(), java_bytecode_convert_methodt::convert_instructions(), convert_integer_literal(), java_bytecode_convert_methodt::convert_invoke(), cpp_declarator_convertert::convert_new_symbol(), cpp_typecheckt::convert_non_template_declaration(), cpp_typecheckt::convert_pmop(), convert_string_literal(), cpp_typecheckt::convert_template_function_or_member_specialization(), smt2_convt::convert_typecast(), copy_array(), copy_member(), copy_parent(), cpp_typecheckt::cpp_constructor(), cpp_convert_plain_type(), cpp_symbol_expr(), create_clinit_wrapper_symbols(), create_stub_global_symbol(), cpp_typecheckt::default_assignop(), cpp_typecheckt::default_assignop_value(), cpp_typecheckt::default_cpctor(), cpp_typecheckt::default_ctor(), cpp_typecheckt::default_dtor(), value_set_dereferencet::dereference(), cpp_typecheck_resolvet::do_builtin(), goto_convertt::do_cpp_new(), goto_convertt::do_function_call_symbol(), c_typecheck_baset::do_special_functions(), double_type(), cpp_typecheckt::dtor(), expr_initializert< nondet >::expr_initializer_rec(), goto_convertt::finish_computed_gotos(), float_type(), cpp_typecheckt::full_member_initialization(), ansi_c_declarationt::full_type(), function_to_call(), gcc_float128_type(), gcc_float128x_type(), gcc_float16_type(), gcc_float32_type(), gcc_float32x_type(), gcc_float64_type(), gcc_float64x_type(), gcc_signed_int128_type(), gcc_unsigned_int128_type(), generate_ansi_c_start_function(), generate_class_stub(), languaget::generate_opaque_method_stubs(), remove_virtual_functionst::get_child_functions_rec(), cpp_typecheckt::get_component(), remove_virtual_functionst::get_functions(), ssa_exprt::get_l1_object(), remove_returnst::get_or_create_return_value_symbol(), cpp_typecheck_resolvet::guess_function_template_args(), cpp_typecheckt::implicit_conversion_sequence(), c_typecastt::implicit_typecast_followed(), cpp_typecheckt::instantiate_template(), instrument_start_thread(), is_zero_string(), java_array_type(), java_bytecode_convert_method_lazy(), java_classname(), java_static_lifetime_init(), java_type_from_string(), long_double_type(), remove_java_newt::lower_java_new_array(), code_typet::make_ellipsis(), goto_functiont::make_hidden(), make_member_expr(), cpp_typecheck_fargst::match(), cpp_declarationt::name_anon_struct_union(), cpp_typecheckt::new_temporary(), dump_ct::operator()(), Parser::optPtrOperator(), remove_asmt::process_instruction(), Parser::rAllocateExpr(), Parser::rAttribute(), Parser::rBaseSpecifiers(), Parser::rClassSpec(), java_bytecode_parsert::rconstant_pool(), Parser::rDeclaratorWithInit(), cpp_convert_typet::read_function_type(), cpp_convert_typet::read_rec(), cpp_typecheckt::reference_binding(), cpp_typecheckt::reinterpret_typecast(), goto_convertt::remove_cpp_delete(), Parser::rEnumBody(), Parser::rEnumSpec(), rewrite_assignment(), Parser::rExpression(), Parser::rGCCAsmStatement(), Parser::rMSCAsmStatement(), Parser::rName(), Parser::rPrimaryExpr(), Parser::rStatement(), Parser::rTempArgDeclaration(), Parser::rTemplateDecl(), Parser::rTryStatement(), Parser::rTypeNameOrFunctionType(), Parser::rUnaryExpr(), Parser::rVarNameCore(), signed_char_type(), signed_int_type(), signed_long_int_type(), signed_long_long_int_type(), signed_short_int_type(), simplify_exprt::simplify_byte_update(), simplify_exprt::simplify_concatenation(), simplify_exprt::simplify_typecast(), select_pointer_typet::specialize_generics(), cpp_typecheckt::standard_conversion_pointer(), static_lifetime_init(), cpp_typecheckt::static_typecast(), goto_symext::symex_allocate(), goto_symext::symex_assign_struct_member(), goto_symext::symex_cpp_new(), ansi_c_declarationt::to_symbol(), ieee_float_spect::to_type(), c_typecheck_baset::typecheck_array_type(), c_typecheck_baset::typecheck_c_enum_type(), cpp_typecheckt::typecheck_compound_bases(), c_typecheck_baset::typecheck_compound_body(), cpp_typecheckt::typecheck_compound_body(), cpp_typecheckt::typecheck_compound_declarator(), c_typecheck_baset::typecheck_compound_type(), cpp_typecheckt::typecheck_compound_type(), c_typecheck_baset::typecheck_custom_type(), cpp_typecheckt::typecheck_expr(), c_typecheck_baset::typecheck_expr_address_of(), cpp_typecheckt::typecheck_expr_address_of(), c_typecheck_baset::typecheck_expr_comma(), cpp_typecheckt::typecheck_expr_cpp_name(), cpp_typecheckt::typecheck_expr_delete(), c_typecheck_baset::typecheck_expr_dereference(), cpp_typecheckt::typecheck_expr_explicit_typecast(), c_typecheck_baset::typecheck_expr_function_identifier(), cpp_typecheckt::typecheck_expr_function_identifier(), c_typecheck_baset::typecheck_expr_index(), c_typecheck_baset::typecheck_expr_main(), cpp_typecheckt::typecheck_expr_main(), c_typecheck_baset::typecheck_expr_member(), cpp_typecheckt::typecheck_expr_member(), cpp_typecheckt::typecheck_expr_new(), c_typecheck_baset::typecheck_expr_ptrmember(), c_typecheck_baset::typecheck_expr_symbol(), cpp_typecheckt::typecheck_expr_throw(), c_typecheck_baset::typecheck_expr_trinary(), cpp_typecheckt::typecheck_expr_trinary(), c_typecheck_baset::typecheck_expr_typecast(), c_typecheck_baset::typecheck_for(), c_typecheck_baset::typecheck_function_call_arguments(), cpp_typecheckt::typecheck_member_function(), cpp_typecheckt::typecheck_member_initializer(), cpp_typecheckt::typecheck_method_application(), c_typecheck_baset::typecheck_redefinition_non_type(), c_typecheck_baset::typecheck_side_effect_assignment(), cpp_typecheckt::typecheck_side_effect_assignment(), c_typecheck_baset::typecheck_side_effect_function_call(), cpp_typecheckt::typecheck_side_effect_function_call(), cpp_typecheckt::typecheck_side_effect_inc_dec(), c_typecheck_baset::typecheck_symbol_type(), cpp_typecheckt::typecheck_template_parameters(), cpp_typecheckt::typecheck_try_catch(), c_typecheck_baset::typecheck_type(), cpp_typecheckt::typecheck_type(), unsigned_char_type(), unsigned_int_type(), unsigned_long_int_type(), unsigned_long_long_int_type(), unsigned_short_int_type(), cpp_typecheckt::user_defined_conversion_sequence(), wchar_t_type(), cpp_convert_typet::write(), ansi_c_convert_typet::write(), c_qualifierst::write(), yyansi_cparse(), yyassemblerlex(), cpp_typecheckt::zero_initializer(), and zero_string_length().
|
inline |
void irept::set | ( | const irep_namet & | name, |
const long long | value | ||
) |
Definition at line 265 of file irep.cpp.
References add(), id(), and to_string().
|
inline |
Definition at line 231 of file irep.h.
References data.
Referenced by c_typecheck_baset::add_argc_argv(), goto_checkt::add_guarded_claim(), cpp_typecheckt::add_implicit_dereference(), already_typechecked(), cpp_typecheck_resolvet::apply_template_args(), disjunctive_polynomial_accelerationt::assert_for_values(), symex_slice_by_tracet::assign_merges(), build_class_identifier(), string_abstractiont::build_if(), goto_convertt::case_guard(), goto_checkt::check_rec(), goto_convertt::clean_expr(), goto_convertt::clean_expr_address_of(), goto_program2codet::cleanup_code(), goto_program2codet::cleanup_code_block(), goto_program2codet::cleanup_code_ifthenelse(), dump_ct::cleanup_decl(), goto_program2codet::cleanup_expr(), dump_ct::cleanup_expr(), dump_ct::cleanup_harness(), code_typet::code_typet(), preconditiont::compute_rec(), symex_slice_by_tracet::compute_ts_back(), cpp_typecheckt::const_typecast(), cpp_declarator_convertert::convert(), cpp_typecheckt::convert_anonymous_union(), goto_convertt::convert_assign(), jsil_convertt::convert_code(), goto_program2codet::convert_goto_break_continue(), goto_program2codet::convert_goto_goto(), goto_program2codet::convert_goto_switch(), goto_program2codet::convert_goto_while(), cpp_typecheckt::convert_initializer(), java_bytecode_convert_methodt::convert_instructions(), smt2_convt::convert_plus(), cpp_typecheckt::convert_pmop(), expr2cppt::convert_rec(), goto_program2codet::convert_start_thread(), goto_convertt::convert_switch(), cpp_typecheckt::convert_template_function_or_member_specialization(), cpp_typecheckt::cpp_constructor(), cpp_typecheckt::cpp_destructor(), goto_program_dereferencet::dereference_rec(), goto_symext::dereference_rec(), cpp_typecheckt::do_not_typechecked(), value_sett::eval_pointer_offset(), cpp_typecheckt::explicit_typecast_ambiguity(), disjunctive_polynomial_accelerationt::find_path(), disjunctive_polynomial_accelerationt::fit_polynomial(), fix_types(), flatten_byte_update(), cpp_typecheckt::full_member_initialization(), generate_ansi_c_start_function(), generate_java_start_function(), prop_conv_solvert::get(), cpp_typecheckt::get_component(), rw_guarded_range_set_value_sett::get_objects_if(), guardt::guard_expr(), cpp_declarator_convertert::handle_initializer(), instantiate_quantifier(), cpp_typecheckt::instantiate_template(), jsil_entry_point(), goto_symex_statet::l2_thread_read_encoding(), smt2_parsert::let_expression(), make_binary(), codet::make_block(), cpp_typecheck_resolvet::make_constructors(), exprt::make_not(), exprt::make_typecast(), move_label_ifthenelse(), move_to_named_sub(), cpp_typecheckt::new_temporary(), sat_path_enumeratort::next(), invariant_sett::nnf(), nondet_volatile_rhs(), cpp_typecheckt::operator_is_overloaded(), Parser::optIntegralTypeOrClassSpec(), Parser::optPtrOperator(), goto_symext::process_array_expr(), smt2_parsert::quantifier_expression(), Parser::rAdditiveExpr(), Parser::rAlignofExpr(), Parser::rAllocateExpr(), Parser::rAllocateType(), Parser::rAndExpr(), Parser::rArgDeclList(), Parser::rCastExpr(), Parser::rClassBody(), Parser::rClassSpec(), Parser::rCommaExpression(), Parser::rConditionalExpr(), Parser::rConstructorDecl(), Parser::rDeclarator(), Parser::rDeclaratorWithInit(), cpp_convert_typet::read_function_type(), cpp_typecheckt::reference_binding(), cpp_typecheckt::reference_initializer(), cpp_typecheckt::reinterpret_typecast(), goto_convertt::remove_assignment(), remove_calls_no_bodyt::remove_call_no_body(), remove_function_pointerst::remove_function_pointer(), goto_convertt::remove_gcc_conditional_expression(), goto_convertt::remove_post(), goto_convertt::remove_pre(), Parser::rEnumBody(), Parser::rEnumSpec(), goto_symext::replace_nondet(), string_abstractiont::replace_string_macros(), Parser::rEqualityExpr(), cpp_typecheck_resolvet::resolve_scope(), goto_convertt::rewrite_boolean(), goto_symext::rewrite_quantifiers(), Parser::rExclusiveOrExpr(), Parser::rExpression(), Parser::rIfStatement(), Parser::rInclusiveOrExpr(), Parser::rIntegralDeclaration(), Parser::rIntegralDeclStatement(), Parser::rLinkageSpec(), Parser::rLogicalAndExpr(), Parser::rLogicalOrExpr(), Parser::rMemberInit(), Parser::rMSCuuidof(), Parser::rMultiplyExpr(), Parser::rName(), Parser::rNewDeclarator(), Parser::rOtherDeclaration(), Parser::rOtherDeclStatement(), Parser::rPmExpr(), Parser::rPostfixExpr(), Parser::rPrimaryExpr(), Parser::rPtrToMember(), Parser::rRelationalExpr(), Parser::rShiftExpr(), Parser::rSimpleDeclaration(), Parser::rSizeofExpr(), Parser::rStatement(), Parser::rTempArgDeclaration(), Parser::rTemplateArgs(), Parser::rTemplateDecl(), Parser::rTypeName(), Parser::rTypeNameOrFunctionType(), Parser::rTypePredicate(), invariant_sett::simplify(), simplify_exprt::simplify_address_of(), simplify_exprt::simplify_address_of_arg(), simplify_exprt::simplify_bitwise(), simplify_exprt::simplify_boolean(), simplify_exprt::simplify_bswap(), simplify_exprt::simplify_byte_extract(), simplify_exprt::simplify_byte_update(), simplify_exprt::simplify_concatenation(), simplify_exprt::simplify_dereference(), simplify_exprt::simplify_div(), simplify_exprt::simplify_dynamic_object(), simplify_exprt::simplify_extractbits(), simplify_exprt::simplify_floatbv_op(), simplify_exprt::simplify_floatbv_typecast(), simplify_exprt::simplify_good_pointer(), simplify_exprt::simplify_ieee_float_relation(), simplify_exprt::simplify_if(), simplify_exprt::simplify_if_preorder(), simplify_exprt::simplify_index(), simplify_exprt::simplify_inequality(), simplify_exprt::simplify_inequality_constant(), simplify_exprt::simplify_inequality_not_constant(), simplify_exprt::simplify_member(), simplify_exprt::simplify_minus(), simplify_exprt::simplify_mod(), simplify_exprt::simplify_mult(), simplify_exprt::simplify_not(), simplify_exprt::simplify_object(), simplify_exprt::simplify_plus(), simplify_exprt::simplify_pointer_offset(), simplify_exprt::simplify_popcount(), simplify_exprt::simplify_rec(), simplify_exprt::simplify_shifts(), simplify_exprt::simplify_typecast(), simplify_exprt::simplify_unary_minus(), simplify_exprt::simplify_update(), simplify_exprt::simplify_with(), symex_slice_by_tracet::slice_by_trace(), symex_slice_by_tracet::slice_SSA_steps(), cpp_typecheckt::standard_conversion_qualification(), cpp_typecheckt::standard_conversion_sequence(), cpp_typecheckt::static_and_dynamic_initialization(), cpp_typecheckt::static_typecast(), postconditiont::strengthen(), goto_functiont::swap(), goto_symext::symex_assign_symbol(), goto_symext::symex_other(), jsil_declarationt::to_symbol(), cpp_typecheckt::typecheck_cast_expr(), cpp_typecheckt::typecheck_class_template(), c_typecheck_baset::typecheck_code_type(), cpp_typecheckt::typecheck_compound_declarator(), c_typecheck_baset::typecheck_compound_type(), cpp_typecheckt::typecheck_compound_type(), c_typecheck_baset::typecheck_decl(), cpp_typecheckt::typecheck_decl(), c_typecheck_baset::typecheck_declaration(), c_typecheck_baset::typecheck_dowhile(), cpp_typecheckt::typecheck_enum_type(), c_typecheck_baset::typecheck_expr(), c_typecheck_baset::typecheck_expr_address_of(), cpp_typecheckt::typecheck_expr_address_of(), c_typecheck_baset::typecheck_expr_alignof(), c_typecheck_baset::typecheck_expr_builtin_offsetof(), c_typecheck_baset::typecheck_expr_builtin_va_arg(), cpp_typecheckt::typecheck_expr_cpp_name(), cpp_typecheckt::typecheck_expr_explicit_typecast(), c_typecheck_baset::typecheck_expr_main(), java_bytecode_typecheckt::typecheck_expr_member(), c_typecheck_baset::typecheck_expr_member(), cpp_typecheckt::typecheck_expr_member(), cpp_typecheckt::typecheck_expr_new(), c_typecheck_baset::typecheck_expr_ptrmember(), cpp_typecheckt::typecheck_expr_ptrmember(), c_typecheck_baset::typecheck_expr_sizeof(), c_typecheck_baset::typecheck_expr_symbol(), cpp_typecheckt::typecheck_expr_trinary(), c_typecheck_baset::typecheck_expr_typecast(), c_typecheck_baset::typecheck_for(), cpp_typecheckt::typecheck_function_expr(), cpp_typecheckt::typecheck_function_template(), c_typecheck_baset::typecheck_ifthenelse(), cpp_typecheckt::typecheck_member_function(), cpp_typecheckt::typecheck_member_initializer(), cpp_typecheckt::typecheck_method_application(), c_typecheck_baset::typecheck_redefinition_non_type(), c_typecheck_baset::typecheck_redefinition_type(), cpp_typecheckt::typecheck_side_effect_assignment(), c_typecheck_baset::typecheck_side_effect_function_call(), cpp_typecheckt::typecheck_side_effect_function_call(), cpp_typecheckt::typecheck_side_effect_inc_dec(), c_typecheck_baset::typecheck_side_effect_statement_expression(), cpp_typecheckt::typecheck_switch(), cpp_typecheckt::typecheck_template_args(), cpp_typecheckt::typecheck_template_parameters(), cpp_typecheckt::typecheck_type(), c_typecheck_baset::typecheck_typeof_type(), c_typecheck_baset::typecheck_while(), cpp_typecheckt::user_defined_conversion_sequence(), cpp_convert_typet::write(), ansi_c_convert_typet::write(), yyansi_cparse(), and yyjsilparse().
|
inline |
Definition at line 339 of file irep.h.
References data, and detach().
Referenced by get_comments(), get_named_sub(), get_sub(), and id().
|
protected |
Definition at line 326 of file irep.h.
Referenced by string_dependenciest::add_constraints(), full_eq(), operator=(), operator==(), read(), swap(), and write().
|
staticprotected |
Definition at line 327 of file irep.h.
Referenced by detach(), irept(), nonrecursive_destructor(), operator=(), and remove_ref().