Go to the documentation of this file.
10 #ifndef CPROVER_UTIL_SSA_EXPR_H
11 #define CPROVER_UTIL_SSA_EXPR_H
22 set(ID_C_SSA_symbol,
true);
31 set(ID_C_SSA_symbol,
true);
32 add(ID_expression, expr);
38 static_cast<exprt &>(
add(ID_expression)).type()=
type();
43 return static_cast<const exprt &>(
find(ID_expression));
59 root.
set(ID_L0,
get(ID_L0));
60 root.set(ID_L1,
get(ID_L1));
61 root.update_identifier();
73 return get(ID_L1_object_identifier);
133 vm, !expr.
has_operands(),
"SSA expression should not have operands");
135 vm, expr.
id() == ID_symbol,
"SSA expression symbols are symbols");
146 static_cast<const exprt &>(expr.
find(ID_expression)), ns, vm);
163 expr.
id() == ID_symbol && expr.
get_bool(ID_C_SSA_symbol) &&
165 return static_cast<const ssa_exprt &>(expr);
174 expr.
id() == ID_symbol && expr.
get_bool(ID_C_SSA_symbol) &&
176 return static_cast<ssa_exprt &>(expr);
181 return expr.
id()==ID_symbol &&
185 #endif // CPROVER_UTIL_SSA_EXPR_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
#define PRECONDITION(CONDITION)
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
const irep_idt get_original_name() const
const irep_idt get_level_0() const
irept & add(const irep_namet &name)
Split an expression into a base object and a (byte) offset.
const irept & find(const irep_namet &name) const
Base class for all expressions.
irep_idt get_object_name() const
Expression to hold a symbol (variable)
const exprt & get_original_expr() const
Expression providing an SSA-renamed symbol of expressions.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
typet & type()
Return the type of the expression.
bool get_bool(const irep_namet &name) const
bool is_ssa_expr(const exprt &expr)
ssa_exprt(const exprt &expr)
Constructor.
bool has_operands() const
Return true if there is at least one operand.
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
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.
void set_level_1(unsigned i)
const irep_idt & id() const
void remove(const irep_namet &name)
const exprt & root_object() const
const irep_idt get_l1_object_identifier() const
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
const irep_idt & get(const irep_namet &name) const
void set_level_0(unsigned i)
void set(const irep_namet &name, const irep_idt &value)
const irep_idt get_level_1() const
void set_level_2(unsigned i)
void validate_full_expr(const exprt &expr, const namespacet &ns, const validation_modet vm)
Check that the given expression is well-formed (full check, including checks of all subexpressions an...
static bool can_build_identifier(const exprt &src)
void set_identifier(const irep_idt &identifier)
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)