56 bool did_initialize_values =
false;
57 auto struct_type_it = struct_type_def.
components().begin();
59 ++param_it, ++struct_type_it)
62 struct_type_it->get_name(),
64 did_initialize_values =
true;
67 if(did_initialize_values)
81 std::cout <<
"Reading component " << member_expr.get_component_name() <<
'\n';
104 member_expr.
type(), ns,
true,
false);
112 const std::stack<exprt> &stack,
115 bool merging_write)
const
118 std::cout <<
"Writing component " << member_expr.get_component_name() <<
'\n';
124 return std::make_shared<full_struct_abstract_objectt>(
129 std::dynamic_pointer_cast<full_struct_abstract_objectt>(
mutable_clone());
135 auto const old_value =
map.
find(c);
136 if(!old_value.has_value())
139 member_expr.
type(), ns,
true,
false);
141 c, environment.
write(starting_value, value, stack, ns, merging_write));
147 environment.
write(old_value.value(), value, stack, ns, merging_write));
150 result->set_not_top();
151 DATA_INVARIANT(result->verify(),
"Structural invariants maintained");
157 std::cout <<
"Setting component" << std::endl;
161 auto const old_value = result->map.find(c);
167 DATA_INVARIANT(result->verify(),
"Structural invariants maintained");
171 INVARIANT(!result->map.empty(),
"If not top, map cannot be empty");
173 if(!old_value.has_value())
175 DATA_INVARIANT(result->verify(),
"Structural invariants maintained");
183 if(old_value.has_value())
185 result->map.replace(c, value);
189 result->map.insert(c, value);
191 result->set_not_top();
192 INVARIANT(!result->is_bottom(),
"top != bottom");
195 DATA_INVARIANT(result->verify(),
"Structural invariants maintained");
214 for(
const auto &field : type_decl.
components())
216 auto value =
map.
find(field.get_name());
217 if(value.has_value())
223 out <<
'.' << field.get_name() <<
'=';
243 std::dynamic_pointer_cast<const full_struct_abstract_objectt>(other);
260 return std::make_shared<full_struct_abstract_objectt>(*other);
265 std::dynamic_pointer_cast<full_struct_abstract_objectt>(
mutable_clone());
272 return shared_from_this();
276 INVARIANT(!result->is_top(),
"Merge of maps will not generate top");
277 INVARIANT(!result->is_bottom(),
"Merge of maps will not generate bottom");
278 DATA_INVARIANT(result->verify(),
"Structural invariants maintained");
288 std::dynamic_pointer_cast<full_struct_abstract_objectt>(
mutable_clone());
290 bool modified =
false;
293 result->map.get_view(view);
295 for(
auto &item : view)
297 auto newval = visitor.
visit(item.second);
298 if(newval != item.second)
300 result->map.replace(item.first, newval);
311 return shared_from_this();
323 for(
auto const &
object : view)
325 if(visited.find(
object.second) == visited.end())
327 object.second->get_statistics(
statistics, visited, env, ns);
An abstract version of a program environment.
std::set< abstract_object_pointert > abstract_object_visitedt
sharing_ptrt< class abstract_objectt > abstract_object_pointert
static bool merge_shared_maps(const sharing_mapt< keyt, abstract_object_pointert, false, hash > &map1, const sharing_mapt< keyt, abstract_object_pointert, false, hash > &map2, sharing_mapt< keyt, abstract_object_pointert, false, hash > &out_map)
virtual abstract_object_pointert write(const abstract_object_pointert &lhs, const abstract_object_pointert &rhs, std::stack< exprt > remaining_stack, const namespacet &ns, bool merge_write)
Used within assign to do the actual dispatch.
virtual abstract_object_pointert abstract_object_factory(const typet &type, const namespacet &ns, bool top, bool bottom) const
Look at the configuration for the sensitivity and create an appropriate abstract_object.
virtual bool is_top() const
Find out if the abstract object is top.
virtual bool is_bottom() const
Find out if the abstract object is bottom.
virtual internal_abstract_object_pointert mutable_clone() const
static abstract_object_pointert merge(abstract_object_pointert op1, abstract_object_pointert op2, bool &out_modifications)
Clones the first parameter and merges it with the second.
typet t
To enforce copy-on-write these are private and have read-only accessors.
virtual const typet & type() const
Get the real type of the variable this abstract object is representing.
This is the basic interface of the abstract interpreter with default implementations of the core func...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
typet & type()
Return the type of the expression.
void output(std::ostream &out, const class ai_baset &ai, const class namespacet &ns) const override
To provide a human readable string to the out representing the current known value about this object.
abstract_object_pointert write_component(abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const exprt &expr, const abstract_object_pointert &value, bool merging_write) const override
A helper function to evaluate writing to a component of a struct.
bool verify() const override
Function: full_struct_abstract_objectt::verify.
void statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override
abstract_object_pointert merge(abstract_object_pointert other) const override
To merge an abstract object into this abstract object.
abstract_object_pointert visit_sub_elements(const abstract_object_visitort &visitor) const override
Apply a visitor operation to all sub elements of this abstract_object.
sharing_ptrt< full_struct_abstract_objectt > constant_struct_pointert
CLONE abstract_object_pointert read_component(const abstract_environmentt &environment, const exprt &expr, const namespacet &ns) const override
A helper function to evaluate the abstract object contained within a struct.
full_struct_abstract_objectt(const full_struct_abstract_objectt &ao)
Explicit copy-constructor to make it clear that the shared_map used to store the values of fields is ...
abstract_object_pointert merge_constant_structs(constant_struct_pointert other) const
Performs an element wise merge of the map for each struct.
const irep_idt & id() const
Extract member of struct or union.
const exprt & compound() const
irep_idt get_component_name() const
static memory_sizet from_bytes(std::size_t bytes)
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
std::vector< view_itemt > viewt
View of the key-value pairs in the map.
bool empty() const
Check if map is empty.
optionalt< std::reference_wrapper< const mapped_type > > find(const key_type &k) const
Find element.
void insert_or_replace(const key_type &k, valueU &&m)
void get_view(V &view) const
Get a view of the elements in the map A view is a list of pairs with the components being const refer...
Structure type, corresponds to C style structs.
Base type for structs and unions.
const componentst & components() const
The type of an expression, extends irept.
An abstraction of a structure that stores one abstract object per field.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
API to expression classes.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Pure virtual interface required of a client that can apply a copy-on-write operation to a given abstr...
virtual abstract_object_pointert visit(const abstract_object_pointert element) const =0