Go to the documentation of this file.
15 #include <unordered_set>
38 if(expr.
type().
id() == ID_array)
65 if(expr.
id() == ID_address_of)
72 else if(expr.
id() == ID_plus || expr.
id() == ID_minus)
80 "An offset must be an integral amount");
82 if(expr.
id() == ID_minus)
96 std::make_shared<offset_entryt>(offset_value), environment, ns);
104 std::shared_ptr<const write_stack_entryt> entry = *
stack.cbegin();
107 "The base should be an addressable location (i.e. symbol)");
134 if(expr.
id() == ID_member)
136 add_to_stack(std::make_shared<simple_entryt>(expr), environment, ns);
140 else if(expr.
id() == ID_symbol)
142 add_to_stack(std::make_shared<simple_entryt>(expr), environment, ns);
144 else if(expr.
id() == ID_index)
165 environment.
eval(index_expr.
index(), ns);
167 add_to_stack(std::make_shared<offset_entryt>(offset_value), environment, ns);
179 for(
const std::shared_ptr<write_stack_entryt> &entry :
stack)
181 exprt new_expr = entry->get_access_expr();
182 if(access_expr.
id() == ID_nil)
184 access_expr = new_expr;
192 new_expr.
operands()[0] = access_expr;
195 entry->adjust_access_type(new_expr);
197 access_expr = new_expr;
201 return std::move(top_expr);
218 std::shared_ptr<write_stack_entryt> entry_pointer,
224 !
stack.front()->try_squash_in(entry_pointer, environment, ns))
239 exprt &out_base_expr,
240 exprt &out_integral_expr)
244 static const std::unordered_set<irep_idt, irep_id_hash> integral_types = {
245 ID_signedbv, ID_unsignedbv, ID_integer};
246 if(integral_types.find(binary_e.lhs().type().id()) != integral_types.cend())
248 out_integral_expr = binary_e.lhs();
249 out_base_expr = binary_e.rhs();
253 integral_types.find(binary_e.rhs().type().id()) != integral_types.cend())
255 out_integral_expr = binary_e.rhs();
256 out_base_expr = binary_e.lhs();
Represents a stack of write operations to an addressable memory location.
bool is_top_value() const
Is the stack representing an unknown value and hence can't be written to or read from.
sharing_ptrt< class abstract_objectt > abstract_object_pointert
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Base class for all expressions.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
virtual exprt get_access_expr() const =0
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.
void construct_stack_to_lvalue(const exprt &expr, const abstract_environmentt &environment, const namespacet &ns)
Construct a stack up to a specific l-value (i.e.
#define PRECONDITION(CONDITION)
API to expression classes for Pointers.
The unary minus expression.
virtual abstract_object_pointert eval(const exprt &expr, const namespacet &ns) const
These three are really the heart of the method.
const irep_idt & id() const
void construct_stack_to_pointer(const exprt &expr, const abstract_environmentt &environment, const namespacet &ns)
Add to the stack the elements to get to a pointer.
static integral_resultt get_which_side_integral(const exprt &expr, exprt &out_base_expr, exprt &out_integral_expr)
Utility function to find out which side of a binary operation has an integral type,...
void construct_stack_to_array_index(const index_exprt &expr, const abstract_environmentt &environment, const namespacet &ns)
Construct a stack for an array position l-value.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Operator to return the address of an object.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
unsignedbv_typet size_type()
write_stackt()
Build a topstack.
void add_to_stack(std::shared_ptr< write_stack_entryt > entry_pointer, const abstract_environmentt environment, const namespacet &ns)
Add an element to the top of the stack.
exprt to_expression() const
Convert the stack to an expression that can be used to write to.
API to expression classes.
continuation_stack_storet stack