Go to the documentation of this file.
25 if(
auto member = expr_try_dynamic_cast<member_exprt>(expr))
28 <<
".." << member->get_component_name();
30 if(
auto index = expr_try_dynamic_cast<index_exprt>(expr))
36 if(
auto symbol = expr_try_dynamic_cast<symbol_exprt>(expr))
37 return os << symbol->get_identifier();
44 set(ID_C_SSA_symbol,
true);
45 add(ID_expression, expr);
46 std::ostringstream os;
48 const std::string
id = os.str();
50 set(ID_L1_object_identifier,
id);
57 static void build_ssa_identifier_rec(
63 std::ostream &l1_object_os)
65 if(expr.
id()==ID_member)
69 build_ssa_identifier_rec(member.
struct_op(), l0, l1, l2, os, l1_object_os);
74 else if(expr.
id()==ID_index)
78 build_ssa_identifier_rec(index.
array(), l0, l1, l2, os, l1_object_os);
82 os <<
"[[" << idx <<
"]]";
83 l1_object_os <<
"[[" << idx <<
"]]";
85 else if(expr.
id()==ID_symbol)
89 l1_object_os << symid;
95 l1_object_os <<
'!' << l0;
102 l1_object_os <<
'@' << l1;
115 static std::pair<irep_idt, irep_idt> build_identifier(
121 std::ostringstream oss;
122 std::ostringstream l1_object_oss;
124 build_ssa_identifier_rec(expr, l0, l1, l2, oss, l1_object_oss);
129 static void update_identifier(
ssa_exprt &ssa)
137 ssa.
set(ID_L1_object_identifier, idpair.second);
143 add(ID_expression, expr);
151 if(original_expr.
id() == ID_symbol)
164 root.set(ID_L0,
get(ID_L0));
166 root.set(ID_L1,
get(ID_L1));
179 return get(ID_L1_object_identifier);
211 if(expr.
id() == ID_symbol)
213 else if(expr.
id() == ID_member)
215 else if(expr.
id() == ID_index)
#define UNREACHABLE
This should be used to mark dead code.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
void set_level_0(std::size_t i)
const irep_idt get_level_0() const
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
irept & add(const irep_namet &name)
Split an expression into a base object and a (byte) offset.
Base class for all expressions.
irep_idt get_object_name() const
Expression to hold a symbol (variable)
const exprt & get_original_expr() const
void set_level_1(std::size_t i)
Expression providing an SSA-renamed symbol of expressions.
typet & type()
Return the type of the expression.
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.
ssa_exprt(const exprt &expr)
Constructor.
const exprt & struct_op() const
const irep_idt & get_identifier() const
const ssa_exprt get_l1_object() const
const irep_idt get_level_2() const
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const irep_idt & id() const
void remove(const irep_namet &name)
Extract member of struct or union.
const irep_idt get_l1_object_identifier() const
void set_level_2(std::size_t i)
void set_expression(const exprt &expr)
Replace the underlying, original expression by expr while maintaining SSA indices.
ssa_exprt remove_level_2(ssa_exprt ssa)
const irep_idt & get(const irep_namet &name) const
void set(const irep_namet &name, const irep_idt &value)
const irep_idt get_level_1() const
static std::ostream & initialize_ssa_identifier(std::ostream &os, const exprt &expr)
If expr is:
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
irep_idt get_component_name() const
void set_identifier(const irep_idt &identifier)
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.