cprover
language_util.cpp File Reference
#include "language_util.h"
#include <memory>
#include <util/symbol_table.h>
#include <util/namespace.h>
#include <util/language.h>
#include <util/std_expr.h>
#include "mode.h"
Include dependency graph for language_util.cpp:

Go to the source code of this file.

Functions

static languagetget_language (const namespacet &ns, const irep_idt &identifier)
 
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)
 

Function Documentation

§ from_expr() [1/2]

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(), bv_arithmetict::bv_arithmetict(), 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(), fixedbvt::fixedbvt(), 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(), ieee_floatt::ieee_floatt(), 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(), goto_programt::output_instruction(), 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(), bv_arithmetict::to_ansi_c_string(), ieee_floatt::to_ansi_c_string(), trace_value(), constant_propagator_domaint::two_way_propagate_rec(), arrayst::update_index_map(), string_refinementt::update_index_set(), and dott::write_dot_subgraph().

§ from_expr() [2/2]

std::string from_expr ( const exprt expr)

Definition at line 79 of file language_util.cpp.

References from_expr().

§ from_type() [1/2]

§ from_type() [2/2]

std::string from_type ( const typet type)

Definition at line 85 of file language_util.cpp.

References from_type().

§ get_language()

static languaget* get_language ( const namespacet ns,
const irep_idt identifier 
)
static

§ to_expr()

exprt to_expr ( const namespacet ns,
const irep_idt identifier,
const std::string &  src 
)

§ type_to_name() [1/2]

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

§ type_to_name() [2/2]

std::string type_to_name ( const typet type)

Definition at line 111 of file language_util.cpp.

References type_to_name().