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);
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) &&
181 return expr.
id()==ID_symbol &&
185 #endif // CPROVER_UTIL_SSA_EXPR_H const ssa_exprt get_l1_object() const
ssa_exprt(const exprt &expr)
Constructor.
void set_level_1(unsigned i)
const irep_idt & get_identifier() const
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
typet & type()
Return the type of the expression.
void set_level_2(unsigned i)
bool get_bool(const irep_namet &name) const
const irep_idt get_l1_object_identifier() const
const irep_idt get_level_1() const
const irep_idt & id() const
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
void set_level_0(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 void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
API to expression classes.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
#define PRECONDITION(CONDITION)
const irep_idt get_original_name() const
static bool can_build_identifier(const exprt &src)
Split an expression into a base object and a (byte) offset.
const irep_idt get_level_0() const
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
bool has_operands() const
Return true if there is at least one operand.
Base class for all expressions.
const exprt & root_object() const
irep_idt get_object_name() const
const exprt & get_original_expr() const
bool is_ssa_expr(const exprt &expr)
irept & add(const irep_namet &name)
void set_identifier(const irep_idt &identifier)
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs, expressions, instructions, etc.
Expression to hold a symbol (variable)
const irep_idt get_level_2() const
Expression providing an SSA-renamed symbol of expressions.
const irept & find(const irep_namet &name) const
void set(const irep_namet &name, const irep_idt &value)