Go to the documentation of this file.
10 #ifndef CPROVER_UTIL_SSA_EXPR_H
11 #define CPROVER_UTIL_SSA_EXPR_H
35 return static_cast<const exprt &
>(
find(ID_expression));
90 vm, !expr.has_operands(),
"SSA expression should not have operands");
92 vm, expr.id() == ID_symbol,
"SSA expression symbols are symbols");
93 DATA_CHECK(vm, expr.get_bool(ID_C_SSA_symbol),
"wrong SSA expression ID");
99 const auto &expr_sub = expr.get_named_sub();
100 const auto expr_l0 = expr_sub.find(ID_L0);
101 const auto expr_l1 = expr_sub.find(ID_L1);
102 const auto expr_l2 = expr_sub.find(ID_L2);
105 expr_l0 == expr_sub.end() || !expr_l0->second.id().empty(),
106 "L0 must not be an empty string");
109 expr_l1 == expr_sub.end() || !expr_l1->second.id().empty(),
110 "L1 must not be an empty string");
113 expr_l2 == expr_sub.end() || !expr_l2->second.id().empty(),
114 "L2 must not be an empty string");
124 static_cast<const exprt &
>(expr.
find(ID_expression)), ns, vm);
130 return expr.
id() == ID_symbol && expr.
get_bool(ID_C_SSA_symbol);
151 return static_cast<const ssa_exprt &
>(expr);
165 #endif // CPROVER_UTIL_SSA_EXPR_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
bool can_cast_expr< ssa_exprt >(const exprt &base)
void set_level_0(std::size_t i)
#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
void validate_expr(const ssa_exprt &expr)
const irep_idt get_level_0() const
irept & add(const irep_namet &name)
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
void set_level_1(std::size_t i)
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)
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 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 irep_idt & id() const
#define SINCE(year, month, day, msg)
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)
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
const irep_idt & get(const irep_namet &name) const
const irep_idt get_level_1() const
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...
API to expression classes.
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)