cprover
|
#include <util/irep.h>
Go to the source code of this file.
Functions | |
std::string | from_expr (const namespacet &ns, const irep_idt &identifier, const exprt &expr) |
std::string | from_expr (const exprt &expr) |
std::string | from_type (const namespacet &ns, const irep_idt &identifier, const typet &type) |
std::string | from_type (const typet &type) |
exprt | to_expr (const namespacet &ns, const irep_idt &identifier, const std::string &src) |
std::string | type_to_name (const namespacet &ns, const irep_idt &identifier, const typet &type) |
std::string | type_to_name (const typet &type) |
std::string from_expr | ( | const namespacet & | ns, |
const irep_idt & | identifier, | ||
const exprt & | expr | ||
) |
Definition at line 40 of file language_util.cpp.
References languaget::from_expr(), and get_language().
Referenced by goto_checkt::add_guarded_claim(), string_refinementt::add_instantiations(), string_refinementt::add_lemma(), bv_refinementt::approximationt::as_string(), as_string(), value_sett::assign(), value_set_fit::assign(), value_set_fivrnst::assign(), value_set_fivrt::assign(), constant_propagator_domaint::assign_rec(), value_sett::assign_rec(), value_set_fit::assign_rec(), interval_domaint::assume_rec(), string_refinementt::boolbv_set_equality_to_true(), value_set_dereferencet::build_reference_to(), inv_object_storet::build_string(), custom_bitvector_analysist::check(), string_refinementt::check_axioms(), symex_slice_by_tracet::compute_ts_back(), convert(), value_set_analysist::convert(), graphml_witnesst::convert_assign_rec(), string_refinementt::convert_function_application(), smt2_convt::convert_typecast(), value_set_dereferencet::dereference(), string_refinementt::display_index_set(), goto_convertt::do_function_call_symbol(), path_searcht::do_show_vcc(), interpretert::evaluate(), interpretert::evaluate_address(), path_symex_statet::expand_structs_and_arrays(), linkingt::expr_to_string(), from_expr(), string_refinementt::get_array(), value_sett::get_reference_set_rec(), value_set_fivrnst::get_reference_set_rec(), value_set_fit::get_reference_set_sharing_rec(), value_set_fivrt::get_reference_set_sharing_rec(), symex_parse_optionst::get_test(), bmc_covert::get_test(), symex_dereference_statet::get_value_set(), value_sett::get_value_set(), value_set_fit::get_value_set(), value_set_fivrnst::get_value_set(), value_set_fivrt::get_value_set(), value_sett::get_value_set_rec(), value_set_fit::get_value_set_rec(), invariant_sett::implies_rec(), string_refinementt::instantiate_not_contains(), path_symex_statet::instantiate_rec(), instrument_cover_goals(), list_calls_and_arguments(), graphml_witnesst::operator()(), dereferencet::operator()(), local_may_aliast::output(), constant_propagator_domaint::valuest::output(), rw_set_baset::output(), goto_trace_stept::output(), path_symex_stept::output(), java_bytecode_parse_treet::methodt::output(), value_sett::output(), value_set_fit::output(), symex_target_equationt::SSA_stept::output(), guarded_range_domaint::output(), value_set_fivrt::output(), value_set_fivrnst::output_entry(), smt1_convt::set_to(), smt2_convt::set_to(), show_goto_trace(), show_properties(), show_properties_json(), simplify_exprt::simplify(), simplify_exprt::simplify_node(), invariant_sett::strengthen_rec(), goto_symext::symex_step(), trace_value(), constant_propagator_domaint::two_way_propagate_rec(), arrayst::update_index_map(), string_refinementt::update_index_set(), and dott::write_dot_subgraph().
std::string from_expr | ( | const exprt & | expr | ) |
Definition at line 79 of file language_util.cpp.
References from_expr().
std::string from_type | ( | const namespacet & | ns, |
const irep_idt & | identifier, | ||
const typet & | type | ||
) |
Definition at line 53 of file language_util.cpp.
References languaget::from_type(), and get_language().
Referenced by constant_propagator_domaint::assign_rec(), value_set_dereferencet::build_reference_to(), convert(), expr2ct::convert_typecast(), from_type(), goto_program_coverage_recordt::goto_program_coverage_recordt(), value_set_dereferencet::memory_model(), value_set_dereferencet::memory_model_bytes(), value_sett::output(), value_set_fit::output(), value_set_fivrt::output(), value_set_fivrnst::output_entry(), goto_inlinet::parameter_assignments(), cpp_typecheckt::reference_binding(), and linkingt::type_to_string().
std::string from_type | ( | const typet & | type | ) |
Definition at line 85 of file language_util.cpp.
References from_type().
exprt to_expr | ( | const namespacet & | ns, |
const irep_idt & | identifier, | ||
const std::string & | src | ||
) |
Definition at line 91 of file language_util.cpp.
References get_language(), id2string(), namespacet::lookup(), symbolt::module, messaget::set_message_handler(), and languaget::to_expr().
std::string type_to_name | ( | const namespacet & | ns, |
const irep_idt & | identifier, | ||
const typet & | type | ||
) |
Definition at line 66 of file language_util.cpp.
References get_language(), and languaget::type_to_name().
Referenced by linkingt::rename_symbols(), and type_to_name().
std::string type_to_name | ( | const typet & | type | ) |
Definition at line 111 of file language_util.cpp.
References type_to_name().