cprover
|
#include "language_util.h"
#include <memory>
#include <util/symbol_table.h>
#include <util/namespace.h>
#include <util/std_expr.h>
#include "language.h"
#include "mode.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_type (const namespacet &ns, const irep_idt &identifier, const typet &type) |
std::string | type_to_name (const namespacet &ns, const irep_idt &identifier, const typet &type) |
std::string | from_expr (const exprt &expr) |
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 typet &type) |
std::string from_expr | ( | const namespacet & | ns, |
const irep_idt & | identifier, | ||
const exprt & | expr | ||
) |
Definition at line 20 of file language_util.cpp.
References languaget::from_expr(), and get_language_from_identifier().
Referenced by bv_refinementt::approximationt::as_string(), as_string(), interval_domaint::assume_rec(), inv_object_storet::build_string(), custom_bitvector_analysist::check(), convert(), graphml_witnesst::convert_assign_rec(), convert_decl(), convert_properties_json(), goto_convertt::do_function_call_symbol(), interpretert::evaluate(), interpretert::evaluate_address(), linkingt::expr_to_string(), from_expr(), bmc_covert::get_test(), symex_dereference_statet::get_value_set(), invariant_sett::implies_rec(), cover_condition_instrumentert::instrument(), cover_decision_instrumentert::instrument(), cover_mcdc_instrumentert::instrument(), cover_cover_instrumentert::instrument(), list_calls_and_arguments(), graphml_witnesst::operator()(), local_may_aliast::output(), rw_set_baset::output(), constant_propagator_domaint::valuest::output(), java_bytecode_parse_treet::methodt::output(), value_set_fit::output(), symex_target_equationt::SSA_stept::output(), guarded_range_domaint::output(), value_set_fivrt::output(), value_sett::output(), value_set_fivrnst::output_entry(), goto_programt::output_instruction(), show_goto_trace(), bmct::show_program(), show_properties(), bmct::show_vcc_json(), bmct::show_vcc_plain(), invariant_sett::strengthen_rec(), trace_value(), value_sets_to_xml(), and dott::write_dot_subgraph().
std::string from_expr | ( | const exprt & | expr | ) |
Definition at line 59 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 33 of file language_util.cpp.
References languaget::from_type(), and get_language_from_identifier().
Referenced by convert(), convert_decl(), 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_set_fit::output(), value_set_fivrt::output(), value_sett::output(), value_set_fivrnst::output_entry(), goto_programt::output_instruction(), goto_inlinet::parameter_assignments(), cpp_typecheckt::reference_binding(), and linkingt::type_to_string().
std::string from_type | ( | const typet & | type | ) |
Definition at line 65 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 71 of file language_util.cpp.
References get_language_from_identifier(), id2string(), namespacet::lookup(), symbolt::module, null_message_handler, 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 46 of file language_util.cpp.
References get_language_from_identifier(), 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 91 of file language_util.cpp.
References type_to_name().