cprover
irep.h File Reference
#include <cassert>
#include <string>
#include <vector>
#include "irep_ids.h"
#include <map>
Include dependency graph for irep.h:
This graph shows which files directly or indirectly include this file:

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 ireptget_nil_irep ()
 

Macro Definition Documentation

◆ forall_irep

◆ Forall_irep

#define Forall_irep (   it,
  irep 
)

◆ forall_named_irep

#define forall_named_irep (   it,
  irep 
)

◆ Forall_named_irep

#define Forall_named_irep (   it,
  irep 
)
Value:
for(irept::named_subt::iterator it=(irep).begin(); \
it!=(irep).end(); ++it)

Definition at line 73 of file irep.h.

◆ SHARING

#define SHARING

Definition at line 19 of file irep.h.

◆ USE_MOVE

#define USE_MOVE

Definition at line 21 of file irep.h.

Typedef Documentation

◆ irep_id_hash

Definition at line 34 of file irep.h.

◆ irep_idt

typedef dstringt irep_idt

Definition at line 31 of file irep.h.

◆ irep_namet

Definition at line 32 of file irep.h.

Function Documentation

◆ get_nil_irep()

◆ id2string()

const std::string& id2string ( const irep_idt d)
inline

Definition at line 43 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(), ci_lazy_methods_neededt::add_needed_class(), jsil_typecheckt::add_prefix(), string_abstractiont::add_str_arguments(), java_string_library_preprocesst::add_string_type(), add_to_json(), add_to_xml(), compilet::add_written_cprover_symbols(), shared_bufferst::affected_by_delay(), allocate_dynamic_object(), java_object_factoryt::allocate_nondet_length_array(), java_object_factoryt::allocate_object(), ansi_c_architecture_strings(), ansi_c_entry_point(), c_typecheck_baset::apply_asm_label(), invariant_sett::apply_code(), value_set_fit::apply_code(), value_set_fivrnst::apply_code(), value_set_fivrt::apply_code(), value_sett::apply_code_rec(), array_name(), bv_refinementt::approximationt::as_string(), source_locationt::as_string(), as_string(), assign_parameter_names(), 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(), string_abstractiont::build(), resolve_inherited_componentt::build_full_component_identifier(), string_abstractiont::build_new_symbol(), inv_object_storet::build_string(), string_abstractiont::build_symbol(), string_abstractiont::build_symbol_constant(), builtin_factory(), c_new_tmp_symbol(), 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(), dump_ct::cleanup_harness(), clinit_already_run_variable_name(), clinit_function_name(), clinit_local_init_complete_var_name(), clinit_state_var_name(), clinit_thread_local_state_var_name(), clinit_wrapper_name(), comment(), 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(), cpp_typecheckt::convert(), java_bytecode_convert_classt::convert(), java_bytecode_convert_methodt::convert(), convert_assert(), graphml_witnesst::convert_assign_rec(), boolbvt::convert_bv_literals(), expr2ct::convert_code(), expr2ct::convert_code_fence(), dump_ct::convert_compound(), dump_ct::convert_compound_enum(), smt2_convt::convert_constant(), boolbvt::convert_constant(), expr2ct::convert_constant(), smt2_convt::convert_expr(), goto_convert_functionst::convert_function(), cpp_typecheckt::convert_function(), dump_ct::convert_function_declaration(), dump_ct::convert_global_variable(), goto_program2codet::convert_goto_goto(), java_bytecode_convert_methodt::convert_instructions(), java_bytecode_convert_methodt::convert_invoke(), goto_convertt::convert_label(), goto_program2codet::convert_labels(), expr2ct::convert_member(), json_irept::convert_named_sub_tree(), expr2ct::convert_nondet_symbol(), 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_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(), cover_basic_blockst::cover_basic_blockst(), cpp_exception_list_rec(), cpp_type2name(), java_simple_method_stubst::create_method_stub(), create_stub_global_symbols(), 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(), 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(), c_typecheck_baset::do_initializer(), goto_convertt::do_scanf(), cpp_typecheckt::do_virtual_table(), document_propertiest::doit(), cpp_typecheckt::dtor(), dump_ct::dump_typedefs(), ci_lazy_methodst::entry_point_methods(), symbol_tablet::erase(), interpretert::evaluate(), interpretert::execute_function_call(), interpretert::execute_other(), simplify_exprt::expr2bits(), failed_symbol_id(), value_sett::field_sensitive(), cpp_typecheckt::find_dtor(), require_goto_statements::find_pointer_assignments(), require_goto_statements::find_struct_component_assignments(), smt2_convt::find_symbols(), require_goto_statements::find_this_component_assignment(), remove_function_pointerst::fix_return_type(), value_set_fit::flatten_rec(), value_set_fivrt::flatten_rec(), format_rec(), fixedbvt::from_expr(), ieee_floatt::from_expr(), cpp_typecheckt::full_member_initialization(), new_scopet::full_name(), function_enter(), function_exit(), function_to_call(), dump_ct::gather_global_typedefs(), java_object_factoryt::gen_nondet_array_init(), java_object_factoryt::gen_nondet_struct_init(), java_object_factoryt::gen_nondet_subtype_pointer_init(), java_object_factoryt::gen_pointer_target_init(), cpp_enum_typet::generate_anon_tag(), generate_class_stub(), generate_function_bodies(), generate_function_bodies_factory(), assert_false_generate_function_bodiest::generate_function_body_impl(), assert_false_then_assume_false_generate_function_bodiest::generate_function_body_impl(), havoc_generate_function_bodiest::generate_function_body_impl(), generate_function_bodiest::generate_parameter_names(), string_refinementt::get(), remove_virtual_functionst::get_child_functions_rec(), get_class_literal_initializer(), java_bytecode_parsert::get_class_refs(), java_bytecode_parsert::get_class_refs_rec(), document_propertiest::get_code(), value_set_fit::get_entry(), value_set_fivrnst::get_entry(), value_set_fivrt::get_entry(), value_sett::get_entry(), floatbv_typet::get_f(), cpp_declarator_convertert::get_final_identifier(), get_fresh_aux_symbol(), smt2_parsert::get_fresh_id(), remove_virtual_functionst::get_functions(), w_guardst::get_guard_symbol(), cpp_scopest::get_id(), get_inherited_component(), dynamic_object_exprt::get_instance(), fixedbv_typet::get_integer_bits(), get_isr(), get_language_from_identifier(), get_main_symbol(), get_module(), get_new_name(), get_objects_rec(), java_bytecode_convert_methodt::get_or_create_block_for_pcrange(), get_or_create_class_literal_symbol(), remove_returnst::get_or_create_return_value_symbol(), get_or_create_string_literal_symbol(), cpp_declarator_convertert::get_pretty_name(), java_string_library_preprocesst::get_primitive_value_of_object(), global_may_alias_domaint::get_rhs_aliases_address_of(), escape_domaint::get_rhs_aliases_address_of(), expr2ct::get_shorthands(), irept::get_string(), goto_convertt::get_string_constant(), get_tag(), value_set_fivrnst::get_temporary_entry(), value_set_fivrt::get_temporary_entry(), bmc_covert::get_test(), 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(), bmc_all_propertiest::goalt::goalt(), goto_program_coverage_recordt::goto_program_coverage_recordt(), value_set_fivrnst::handover(), value_set_fivrt::handover(), expr2ct::id_shorthand(), irept::id_string(), symex_slice_by_tracet::implied_guards(), infer_opaque_type_fields(), ci_lazy_methodst::initialize_instantiated_classes(), initialize_nondet_string_struct(), cpp_typecheckt::instantiate_template(), taint_analysist::instrument(), escape_analysist::instrument(), cover_location_instrumentert::instrument(), cover_assertion_instrumentert::instrument(), introduce_temporaries(), shared_bufferst::is_buffered(), source_locationt::is_built_in(), is_clinit_wrapper_function(), is_constructor(), pointer_logict::is_dynamic_object(), is_java_array_tag(), is_java_main(), is_java_string_literal_id(), is_nondet_returning_object(), event_grapht::critical_cyclet::is_not_uniproc(), is_shared(), is_store_to_slot(), system_library_symbolst::is_symbol_internal_symbol(), java_array_type(), java_bytecode_convert_method(), java_bytecode_convert_method_lazy(), java_bytecode_initialize_parameter_names(), java_bytecode_instrument_symbol(), java_enum_static_init_unwind_handler(), java_static_lifetime_init(), jsil_entry_point(), json(), json_output_function(), java_bytecode_convert_methodt::label(), label_properties(), list_eloc(), list_functions(), instrumentert::local(), namespace_baset::lookup(), ansi_c_parsert::lookup(), goto_programt::loop_id(), remove_instanceoft::lower_instanceof(), remove_java_newt::lower_java_new_array(), linker_script_merget::ls_data2instructions(), java_string_library_preprocesst::make_argument_for_format(), goto_symext::make_auto_object(), array_poolt::make_char_array_for_char_pointer(), make_function_application(), value_set_fit::make_union(), java_bytecode_languaget::methods_provided(), mm_io(), model_argc_argv(), mul_expr(), string_builtin_function_with_no_evalt::name(), cpp_declarationt::name_anon_struct_union(), cpp_scopet::new_scope(), code_contractst::new_tmp_symbol(), shared_bufferst::nondet_flush(), nondet_static(), custom_bitvector_domaint::object2id(), object_factory(), graphml_witnesst::operator()(), string_abstractiont::operator()(), bmc_all_propertiest::operator()(), taint_analysist::operator()(), rebuild_goto_start_function_baset< maybe_lazy_goto_modelt >::operator()(), bmc_covert::operator()(), dump_ct::operator()(), java_bytecode_convert_classt::operator()(), goto_symex_statet::level0t::operator()(), properties_criteriont::operator()(), internal_functions_filtert::operator()(), include_pattern_filtert::operator()(), original_return_type(), dott::output(), uncaught_exceptions_analysist::output(), value_set_fit::output(), value_set_fivrt::output(), value_sett::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(), java_bytecode_parsert::parse_local_variable_type_table(), smt2_convt::parse_struct(), irept::pretty(), pretty_java_type(), message_handlert::print(), gcc_message_handlert::print(), event_grapht::critical_cyclet::print_detail(), event_grapht::critical_cyclet::print_events(), print_global_state_size(), event_grapht::critical_cyclet::print_output(), remove_asmt::process_instruction(), cpp_scopest::put_into_scope(), java_bytecode_parsert::rbytecode(), java_bytecode_parsert::rclass_attribute(), java_bytecode_parsert::rcode_attribute(), java_bytecode_parsert::rconstant_pool(), java_bytecode_parsert::read_bootstrapmethods_entry(), structured_pool_entryt::read_utf8_constant(), _rw_set_loct::read_write_rec(), references_class_model(), goto_program2codet::remove_const(), rebuild_goto_start_function_baset< maybe_lazy_goto_modelt >::remove_existing_entry_point(), goto_convertt::remove_function_call(), graphml_witnesst::remove_l0_l1(), remove_virtual_functionst::remove_virtual_function(), linkingt::rename(), fault_localizationt::report(), bmc_all_propertiest::report(), fault_localizationt::report_xml(), require_goto_statements::require_entry_point_argument_assignment(), require_parse_tree::require_method(), require_symbol::require_symbol_exists(), resolve_friendly_method_name(), ci_lazy_methodst::resolve_method_names(), remove_returnst::restore_returns(), java_bytecode_parsert::rfield_attribute(), java_bytecode_parsert::rfields(), java_bytecode_parsert::rmethod(), java_bytecode_parsert::rmethod_attribute(), gcc_modet::run_gcc(), partial_order_concurrencyt::rw_clock_id(), configt::set_from_symbol_table(), set_properties(), java_bytecode_convert_methodt::setup_local_variables(), show_goto_trace(), cpp_typecheck_resolvet::show_identifiers(), show_locations(), show_loop_ids(), show_loop_ids_json(), show_properties(), show_symbol_table_brief_plain(), language_uit::show_symbol_table_plain(), show_symbol_table_plain(), simplify_exprt::simplify_bitwise(), simplify_exprt::simplify_dynamic_object(), simplify_exprt::simplify_extractbit(), simplify_exprt::simplify_extractbits(), simplify_json_expr(), simplify_exprt::simplify_pointer_offset(), simplify_exprt::simplify_shifts(), simplify_exprt::simplify_typecast(), slice_global_inits(), cpp_typecheckt::static_and_dynamic_initialization(), static_lifetime_init(), static_verifier(), string_from_ns(), strip_java_namespace_prefix(), substitute_array_access(), sum_expr(), goto_symext::symex_allocate(), goto_symext::symex_assign(), goto_symext::symex_cpp_new(), goto_symext::symex_function_call_symbol(), goto_symext::symex_gcc_builtin_va_arg_next(), goto_symext::symex_macro(), goto_symext::symex_other(), goto_symext::symex_step(), mm2cppt::text2c(), java_bytecode_instrumentt::throw_exception(), 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(), 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_side_effect_function_call(), c_typecheck_baset::typecheck_symbol(), jsil_typecheckt::typecheck_symbol_expr(), cpp_typecheckt::typecheck_template_parameters(), java_bytecode_typecheckt::typecheck_type(), java_bytecode_typecheckt::typecheck_type_symbol(), undefined_function_abort_path(), remove_returnst::undo_function_calls(), unsigned_from_ns(), goto_unwindt::unwind(), constant_exprt::value_is_zero_string(), value_sets_to_xml(), 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(), xml_output_function(), and yyansi_cparse().

◆ name2string()

const std::string& name2string ( const irep_namet n)
inline

Definition at line 52 of file irep.h.

References as_string().

Referenced by convert(), irep2lisp(), and irep2name().