cprover
|
#include <vector>
#include <string>
#include <cassert>
#include <iosfwd>
#include "irep_ids.h"
#include <map>
Go to the source code of this file.
Classes | |
class | irept |
Base class for tree-like data structures with sharing. More... | |
class | irept::dt |
struct | irep_hash |
struct | irep_full_hash |
struct | irep_full_eq |
Macros | |
#define | SHARING |
#define | USE_MOVE |
#define | forall_irep(it, irep) |
#define | Forall_irep(it, irep) |
#define | forall_named_irep(it, irep) |
#define | Forall_named_irep(it, irep) |
Typedefs | |
typedef dstringt | irep_idt |
typedef dstringt | irep_namet |
typedef dstring_hash | irep_id_hash |
Functions | |
const std::string & | id2string (const irep_idt &d) |
const std::string & | name2string (const irep_namet &n) |
const irept & | get_nil_irep () |
#define forall_irep | ( | it, | |
irep | |||
) |
Definition at line 62 of file irep.h.
Referenced by cpp_typecheckt::add_base_components(), xml_irep_convertt::add_with_childs(), cpp_typecheckt::check_component_access(), cpp_typecheckt::check_member_initializers(), convert(), xml_irep_convertt::convert(), cpp_typecheckt::convert_anonymous_union(), dump_ct::convert_compound(), expr2cppt::convert_rec(), cpp_exception_list_rec(), cpp_typecheckt::default_assignop_value(), cpp_typecheckt::default_cpctor(), cpp_typecheckt::find_dtor(), cpp_typecheckt::find_parent(), goto_convertt::finish_gotos(), irept::full_hash(), cpp_typecheckt::full_member_initialization(), cpp_enum_typet::generate_anon_tag(), cpp_typecheckt::get_bases(), cpp_declarator_convertert::get_pretty_name(), cpp_typecheckt::get_virtual_bases(), class_typet::has_base(), cpp_namet::has_template_args(), to_be_merged_irept::hash(), irept::hash(), irep2lisp(), irep2name(), cpp_namet::is_qualified(), merged_irepst::merged(), merge_irept::merged(), merge_full_irept::merged(), cpp_typecheckt::move_member_initializers(), irep_hash_container_baset::pack(), irept::pretty(), xml_irep_convertt::resolve_references(), Parser::rOtherDeclaration(), cpp_namet::to_string(), c_typecheck_baset::typecheck_expr_main(), irep_serializationt::write_irep(), and cpp_typecheckt::zero_initializer().
#define Forall_irep | ( | it, | |
irep | |||
) |
Definition at line 66 of file irep.h.
Referenced by template_mapt::apply(), cpp_typecheckt::full_member_initialization(), cpp_convert_typet::read_function_type(), cpp_convert_typet::read_template(), cpp_typecheckt::typecheck_compound_bases(), cpp_typecheckt::typecheck_enum_body(), and c_typecheck_baset::typecheck_expr_main().
#define forall_named_irep | ( | it, | |
irep | |||
) |
Definition at line 70 of file irep.h.
Referenced by xml_irep_convertt::add_with_childs(), convert(), xml_irep_convertt::convert(), irept::full_hash(), to_be_merged_irept::hash(), irept::hash(), irep2lisp(), irep2name(), merged_irepst::merged(), merge_irept::merged(), merge_full_irept::merged(), irep_hash_container_baset::pack(), irept::pretty(), xml_irep_convertt::resolve_references(), and irep_serializationt::write_irep().
#define Forall_named_irep | ( | it, | |
irep | |||
) |
typedef dstring_hash irep_id_hash |
typedef dstringt irep_namet |
const irept& get_nil_irep | ( | ) |
Definition at line 56 of file irep.cpp.
References dstringt::empty(), irept::id(), and nil_rep_storage.
Referenced by _newstack(), java_bytecode_convert_methodt::convert_instructions(), irept::find(), exprt::find_source_location(), smt1_convt::find_symbols(), goto_inlinet::get_call(), struct_union_typet::get_component(), invariant_sett::get_constant(), get_destructor(), flow_insensitive_abstract_domain_baset::get_return_lhs(), static_analysis_baset::get_return_lhs(), irep_serializationt::insert_on_read(), template_mapt::lookup(), template_mapt::lookup_expr(), template_mapt::lookup_type(), irept::make_nil(), exprt::move_to_operands(), irept::move_to_sub(), typet::move_to_subtypes(), source_locationt::nil(), Parser::optThrowDecl(), Parser::rAllocateExpr(), Parser::rDeclarator(), symex_slice_by_tracet::read_trace(), Parser::rTempArgList(), cpp_namet::source_location(), and typet::subtype().
|
inline |
Definition at line 44 of file irep.h.
References as_string().
Referenced by shared_bufferst::add(), uninitializedt::add_assertions(), string_constraint_generatort::add_axioms_for_constant(), string_constraint_generatort::add_axioms_for_function_application(), ansi_c_parsert::add_declarator(), string_abstractiont::add_dummy_symbol_and_value(), remove_exceptionst::add_exceptional_returns(), ci_lazy_methodst::add_needed_class(), jsil_typecheckt::add_prefix(), string_abstractiont::add_str_arguments(), add_to_json(), shared_bufferst::affected_by_delay(), ansi_c_architecture_strings(), ansi_c_entry_point(), c_typecheck_baset::apply_asm_label(), invariant_sett::apply_code(), value_sett::apply_code(), value_set_fit::apply_code(), value_set_fivrnst::apply_code(), value_set_fivrt::apply_code(), array_name(), bv_refinementt::approximationt::as_string(), source_locationt::as_string(), as_string(), path_symext::assign(), value_set_fit::assign_rec(), value_set_fivrnst::assign_rec(), value_set_fivrt::assign_rec(), shared_bufferst::assignment(), goto_symex_statet::assignment(), event_grapht::graph_explorert::backtrack(), branch(), build_goto_trace(), string_abstractiont::build_new_symbol(), string_abstractiont::build_symbol(), string_abstractiont::build_symbol_constant(), c_nondet_symbol_factory(), mm2cppt::check_acyclic(), shared_bufferst::choice(), java_class_loadert::class_name_to_file(), cpp_typecheckt::class_template_identifier(), cpp_typecheckt::class_template_symbol(), clean_identifier(), goto_program2codet::cleanup_expr(), dump_ct::cleanup_expr(), comment(), fence_all_sharedt::compute(), fence_volatilet::compute(), goto_program_coverage_recordt::compute_coverage_lines(), symex_coveraget::compute_overall_coverage(), symex_slice_by_tracet::compute_ts_back(), instrumentert::cfg_visitort::contains_shared_array(), convert(), show_goto_functions_jsont::convert(), show_goto_functions_xmlt::convert(), xml_goto_program_convertt::convert(), value_set_analysist::convert(), java_bytecode_convert_classt::convert(), cpp_typecheckt::convert(), java_bytecode_convert_methodt::convert(), graphml_witnesst::convert_assign_rec(), cvc_convt::convert_binary_expr(), boolbvt::convert_bv_literals(), expr2ct::convert_code(), expr2ct::convert_code_fence(), dump_ct::convert_compound(), dump_ct::convert_compound_enum(), smt1_convt::convert_constant(), smt2_convt::convert_constant(), boolbvt::convert_constant(), expr2ct::convert_constant(), cvc_convt::convert_constant_expr(), dplib_convt::convert_dplib_expr(), smt2_convt::convert_expr(), convert_float_literal(), goto_convert_functionst::convert_function(), goto_difft::convert_function(), cpp_typecheckt::convert_function(), dump_ct::convert_global_variable(), goto_program2codet::convert_goto_goto(), smt1_convt::convert_identifier(), java_bytecode_convert_methodt::convert_instructions(), goto_convertt::convert_label(), goto_program2codet::convert_labels(), expr2ct::convert_member(), json_irept::convert_named_sub_tree(), boolbvt::convert_overflow(), cpp_typecheckt::convert_parameter(), bv_pointerst::convert_pointer_type(), expr2ct::convert_rec(), expr2cppt::convert_rec(), smt2_convt::convert_rounding_mode_FPA(), goto_convertt::convert_specc_event(), goto_program2codet::convert_start_thread(), expr2ct::convert_struct_type(), expr2ct::convert_symbol(), expr2ct::convert_with(), expr2javat::convert_with_precedence(), expr2cppt::convert_with_precedence(), expr2ct::convert_with_precedence(), cpp_exception_list_rec(), cpp_type2name(), create_vtable_pointer(), java_bytecode_vtable_factoryt::create_vtable_symbol(), create_vtable_symbol(), create_vtable_type(), cpp_typecheckt::default_assignop(), cpp_typecheckt::default_cpctor(), cpp_typecheckt::default_dtor(), shared_bufferst::delay_read(), shared_bufferst::det_flush(), linkingt::detailed_conflict_report_rec(), cpp_typecheck_resolvet::do_builtin(), java_bytecode_languaget::do_ci_lazy_method_conversion(), value_set_fit::do_function_call(), value_set_fivrnst::do_function_call(), value_set_fivrt::do_function_call(), flow_insensitive_analysis_baset::do_function_call_rec(), static_analysis_baset::do_function_call_rec(), ai_baset::do_function_call_rec(), goto_convertt::do_function_call_symbol(), remove_returnst::do_function_calls(), c_typecheck_baset::do_initializer(), goto_convertt::do_scanf(), cpp_typecheckt::do_virtual_table(), document_propertiest::doit(), cpp_typecheckt::dtor(), dump_ct::dump_typedefs(), const_function_pointer_propagationt::dup_caller_and_inline_callee(), bmct::error_trace(), interpretert::evaluate(), interpretert::execute_function_call(), interpretert::execute_other(), simplify_exprt::expr2bits(), string_constraint_generatort::extract_java_string(), failed_symbol_id(), fence_all_shared_aegt::fence_all_shared_aeg_explore(), value_sett::field_sensitive(), cpp_typecheckt::find_dtor(), dplib_convt::find_symbols(), cvc_convt::find_symbols(), smt2_convt::find_symbols(), value_set_fit::flatten_rec(), value_set_fivrt::flatten_rec(), fixedbvt::from_expr(), ieee_floatt::from_expr(), cpp_typecheckt::full_member_initialization(), new_scopet::full_name(), path_symext::function_call_rec(), function_enter(), function_exit(), function_to_call(), dump_ct::gather_global_typedefs(), java_object_factoryt::gen_pointer_target_init(), cpp_enum_typet::generate_anon_tag(), java_bytecode_convert_classt::generate_class_stub(), java_bytecode_parsert::get_class_refs(), java_bytecode_parsert::get_class_refs_rec(), document_propertiest::get_code(), value_sett::get_entry(), value_set_fit::get_entry(), value_set_fivrnst::get_entry(), value_set_fivrt::get_entry(), floatbv_typet::get_f(), cpp_declarator_convertert::get_final_identifier(), get_fresh_aux_symbol(), w_guardst::get_guard_symbol(), cpp_scopest::get_id(), dynamic_object_exprt::get_instance(), fixedbv_typet::get_integer_bits(), get_isr(), get_language(), prop_conv_solvert::get_literal(), get_main_symbol(), get_max(), remove_virtual_functionst::get_method(), get_module(), get_new_name(), get_objects_rec(), cpp_declarator_convertert::get_pretty_name(), global_may_alias_domaint::get_rhs_aliases_address_of(), escape_domaint::get_rhs_aliases_address_of(), irept::get_string(), goto_convertt::get_string_constant(), value_set_fivrnst::get_temporary_entry(), value_set_fivrt::get_temporary_entry(), symex_parse_optionst::get_test(), bmc_covert::get_test(), fence_insertert::get_type(), value_sett::get_value_set_rec(), value_set_fit::get_value_set_rec(), value_set_fivrnst::get_value_set_rec(), value_set_fivrt::get_value_set_rec(), get_virtual_method_target(), get_virtual_method_targets(), java_bytecode_vtable_factoryt::get_vt_type_symbol(), bmc_all_propertiest::goalt::goalt(), goto_program_coverage_recordt::goto_program_coverage_recordt(), value_set_fivrnst::handover(), value_set_fivrt::handover(), has_vtable_info(), expr2ct::id_shorthand(), irept::id_string(), dump_ct::ignore(), symex_slice_by_tracet::implied_guards(), var_mapt::init(), path_symex_statet::instantiate_rec(), cpp_typecheckt::instantiate_template(), taint_analysist::instrument(), escape_analysist::instrument(), instrument_cover_goals(), remove_exceptionst::instrument_exception_handler(), remove_exceptionst::instrument_function_call(), remove_exceptionst::instrument_throw(), introduce_temporaries(), shared_bufferst::is_buffered(), source_locationt::is_built_in(), java_bytecode_vtable_factoryt::is_class_with_vt(), java_bytecode_convert_methodt::is_constructor(), pointer_logict::is_dynamic_object(), event_grapht::critical_cyclet::is_not_uniproc(), is_shared(), is_store_to_slot(), java_array_type(), java_bytecode_convert_method_lazy(), java_entry_point(), java_is_array_type(), java_record_outputs(), java_static_lifetime_init(), jsil_entry_point(), json(), json_output_function(), static_analyzert::json_report(), java_bytecode_convert_methodt::label(), label_properties(), list_eloc(), list_functions(), java_class_loader_limitt::load_class_file(), instrumentert::local(), namespace_baset::lookup(), symbol_tablet::lookup(), ansi_c_parsert::lookup(), goto_program_templatet< codet, exprt >::loop_id(), goto_symext::make_auto_object(), value_set_fit::make_union(), make_vtable_function(), mm_io(), model_argc_argv(), cpp_declarationt::name_anon_struct_union(), exprt::negate(), cpp_scopet::new_scope(), shared_bufferst::nondet_flush(), nondet_static(), custom_bitvector_domaint::object2id(), object_factory(), path_symext::operator()(), graphml_witnesst::operator()(), string_abstractiont::operator()(), bmc_all_propertiest::operator()(), taint_analysist::operator()(), bmc_covert::operator()(), dump_ct::operator()(), var_mapt::operator()(), properties_criteriont::operator()(), java_bytecode_vtable_factoryt::operator()(), original_return_type(), dott::output(), value_sett::output(), value_set_fit::output(), value_set_fivrt::output(), value_set_fivrnst::output_entry(), change_impactt::output_instruction(), ai_baset::output_json(), call_grapht::output_xml(), ai_baset::output_xml(), goto_symext::parameter_assignments(), smt2_convt::parse_literal(), smt2_convt::parse_struct(), irept::pretty(), message_handlert::print(), gcc_message_handlert::print(), event_grapht::critical_cyclet::print_detail(), event_grapht::critical_cyclet::print_events(), event_grapht::critical_cyclet::print_output(), remove_asmt::process_instruction(), cpp_scopest::put_into_scope(), java_bytecode_parsert::rclass_attribute(), java_bytecode_parsert::rcode_attribute(), java_bytecode_parsert::rconstant_pool(), java_class_loadert::read_jar_file(), path_symex_statet::read_symbol_member_index(), _rw_set_loct::read_write_rec(), goto_convertt::remove_cpp_new(), fence_insertert::remove_extra(), goto_convertt::remove_function_call(), graphml_witnesst::remove_l0_l1(), goto_convertt::remove_malloc(), linkingt::rename(), remove_returnst::replace_returns(), fault_localizationt::report(), bmc_all_propertiest::report(), symex_parse_optionst::report_cover(), symex_parse_optionst::report_properties(), remove_returnst::restore_returns(), java_bytecode_parsert::rfields(), java_bytecode_parsert::rmethod(), java_bytecode_parsert::rmethod_attribute(), partial_order_concurrencyt::rw_clock_id(), configt::set_from_symbol_table(), set_properties(), cvc_convt::set_to(), dplib_convt::set_to(), set_virtual_name(), java_bytecode_vtable_factoryt::set_vtable_value(), java_bytecode_convert_methodt::setup_local_variables(), should_init_symbol(), show_goto_trace(), cpp_typecheck_resolvet::show_identifiers(), show_locations(), show_loop_ids(), show_loop_ids_json(), show_properties(), show_properties_json(), show_symbol_table_plain(), language_uit::show_symbol_table_plain(), simplify_exprt::simplify_bitwise(), simplify_exprt::simplify_dynamic_object(), simplify_exprt::simplify_extractbit(), simplify_exprt::simplify_extractbits(), simplify_exprt::simplify_shifts(), simplify_exprt::simplify_typecast(), slice_global_inits(), var_mapt::var_infot::ssa_identifier(), cpp_typecheckt::static_and_dynamic_initialization(), static_lifetime_init(), string_from_ns(), strip_java_namespace_prefix(), goto_symext::symex_assign(), goto_symext::symex_cpp_new(), goto_symext::symex_function_call_code(), goto_symext::symex_function_call_symbol(), goto_symext::symex_gcc_builtin_va_arg_next(), goto_symext::symex_macro(), path_symext::symex_malloc(), goto_symext::symex_malloc(), goto_symext::symex_other(), goto_symext::symex_step(), path_symext::symex_va_arg_next(), java_bytecode_convert_methodt::tmp_variable(), to_expr(), to_integer(), inv_object_storet::to_string(), shared_bufferst::track(), goto_symext::trigger_auto_object(), type2name(), type2name_symbol(), java_bytecode_parsert::type_entry(), type_eq(), linkingt::type_to_string_verbose(), c_typecheck_baset::typecheck_array_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_declaration(), cpp_typecheckt::typecheck_enum_body(), cpp_typecheckt::typecheck_enum_type(), java_bytecode_typecheckt::typecheck_expr_java_string_literal(), java_bytecode_typecheckt::typecheck_expr_member(), c_typecheck_baset::typecheck_expr_side_effect(), java_bytecode_typecheckt::typecheck_expr_symbol(), c_typecheck_baset::typecheck_expr_symbol(), c_typecheck_baset::typecheck_function_body(), cpp_typecheckt::typecheck_function_template(), cpp_typecheckt::typecheck_member_function(), c_typecheck_baset::typecheck_symbol(), jsil_typecheckt::typecheck_symbol_expr(), cpp_typecheckt::typecheck_template_parameters(), undefined_function_abort_path(), remove_returnst::undo_function_calls(), unsigned_from_ns(), remove_static_init_loopst::unwind_enum_static(), constant_exprt::value_is_zero_string(), java_bytecode_convert_methodt::variable(), instrumentert::cfg_visitort::visit_cfg_assign(), weak_memory(), wp(), shared_bufferst::write(), write_goto_binary_v3(), irep_serializationt::write_string_ref(), xml(), static_analyzert::xml_report(), and yyansi_cparse().
|
inline |
Definition at line 53 of file irep.h.
References as_string().
Referenced by convert(), xml_irep_convertt::convert(), irep2lisp(), and irep2name().