27 <<
".." << member->get_component_name();
35 return os << symbol->get_identifier();
42 set(ID_C_SSA_symbol,
true);
43 add(ID_expression, expr);
45 std::ostringstream os;
47 const std::string
id = os.str();
49 set(ID_L1_object_identifier,
id);
62 std::ostream &l1_object_os)
64 if(expr.
id()==ID_member)
73 else if(expr.
id()==ID_index)
80 os <<
"[[" << idx <<
"]]";
81 l1_object_os <<
"[[" << idx <<
"]]";
83 else if(expr.
id()==ID_symbol)
87 l1_object_os << symid;
93 l1_object_os <<
'!' << l0;
100 l1_object_os <<
'@' << l1;
119 std::ostringstream oss;
120 std::ostringstream l1_object_oss;
135 ssa.
set(ID_L1_object_identifier, idpair.second);
141 add(ID_expression, std::move(expr));
149 if(original_expr.
id() == ID_symbol)
162 root.
set(ID_L0,
get(ID_L0));
164 root.
set(ID_L1,
get(ID_L1));
177 return get(ID_L1_object_identifier);
209 if(expr.
id() == ID_symbol)
211 else if(expr.
id() == ID_member)
213 else if(expr.
id() == ID_index)
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
const irep_idt & get_value() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
typet & type()
Return the type of the expression.
const source_locationt & source_location() const
const irep_idt & get(const irep_idt &name) const
void remove(const irep_idt &name)
void set(const irep_idt &name, const irep_idt &value)
const irep_idt & id() const
Extract member of struct or union.
const exprt & struct_op() const
irep_idt get_component_name() const
Split an expression into a base object and a (byte) offset.
const exprt & root_object() const
static const exprt & root_object(const exprt &expr)
Expression providing an SSA-renamed symbol of expressions.
const irep_idt get_level_1() const
const irep_idt get_l1_object_identifier() const
void set_level_1(std::size_t i)
void set_level_2(std::size_t i)
const ssa_exprt get_l1_object() const
void set_expression(exprt expr)
Replace the underlying, original expression by expr while maintaining SSA indices.
const irep_idt get_level_2() const
const irep_idt get_level_0() const
static bool can_build_identifier(const exprt &src)
Used to determine whether or not an identifier can be built before trying and getting an exception.
const exprt & get_original_expr() const
void set_level_0(std::size_t i)
ssa_exprt(const exprt &expr)
Constructor.
irep_idt get_object_name() const
Expression to hold a symbol (variable)
void set_identifier(const irep_idt &identifier)
symbol_exprt & with_source_location(source_locationt location) &
Add the source location from location, if it is non-nil.
const irep_idt & get_identifier() const
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
copy_constructor_body add(code_assign_string_expr_to_java_string(arg_this, string_expr, symbol_table, true), loc)
API to expression classes for Pointers.
#define UNREACHABLE
This should be used to mark dead code.
static std::pair< irep_idt, irep_idt > build_identifier(const exprt &expr, const irep_idt &l0, const irep_idt &l1, const irep_idt &l2)
static void update_identifier(ssa_exprt &ssa)
static void build_ssa_identifier_rec(const exprt &expr, const irep_idt &l0, const irep_idt &l1, const irep_idt &l2, std::ostream &os, std::ostream &l1_object_os)
If expr is a symbol "s" add to os "s!l0@l1#l2" and to l1_object_os "s!l0@l1".
static std::ostream & initialize_ssa_identifier(std::ostream &os, const exprt &expr)
If expr is:
ssa_exprt remove_level_2(ssa_exprt ssa)
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.