Go to the documentation of this file.
57 bool did_initialize_values =
false;
58 auto struct_type_it = struct_type_def.
components().begin();
60 ++param_it, ++struct_type_it)
63 struct_type_it->get_name(),
65 did_initialize_values =
true;
68 if(did_initialize_values)
82 std::cout <<
"Reading component " << member_expr.get_component_name() <<
'\n';
100 return value.value();
105 member_expr.
type(), ns,
true,
false);
113 const std::stack<exprt> &stack,
116 bool merging_write)
const
119 std::cout <<
"Writing component " << member_expr.get_component_name() <<
'\n';
125 return std::make_shared<full_struct_abstract_objectt>(
130 std::dynamic_pointer_cast<full_struct_abstract_objectt>(
mutable_clone());
136 auto const old_value =
map.
find(c);
137 if(!old_value.has_value())
140 member_expr.
type(), ns,
true,
false);
142 c, environment.
write(starting_value, value, stack, ns, merging_write));
148 environment.
write(old_value.value(), value, stack, ns, merging_write));
151 result->set_not_top();
152 DATA_INVARIANT(result->verify(),
"Structural invariants maintained");
158 std::cout <<
"Setting component" << std::endl;
162 auto const old_value = result->map.find(c);
168 DATA_INVARIANT(result->verify(),
"Structural invariants maintained");
172 INVARIANT(!result->map.empty(),
"If not top, map cannot be empty");
174 if(!old_value.has_value())
176 DATA_INVARIANT(result->verify(),
"Structural invariants maintained");
187 if(old_value.has_value())
189 result->map.replace(c, value);
193 result->map.insert(c, value);
195 result->set_not_top();
196 INVARIANT(!result->is_bottom(),
"top != bottom");
199 DATA_INVARIANT(result->verify(),
"Structural invariants maintained");
218 for(
const auto &field : type_decl.
components())
220 auto value =
map.
find(field.get_name());
221 if(value.has_value())
227 out <<
'.' << field.get_name() <<
'=';
248 std::dynamic_pointer_cast<const full_struct_abstract_objectt>(other);
260 return std::make_shared<full_struct_abstract_objectt>(*other);
263 std::dynamic_pointer_cast<full_struct_abstract_objectt>(
mutable_clone());
270 return shared_from_this();
274 INVARIANT(!result->is_top(),
"Merge of maps will not generate top");
275 INVARIANT(!result->is_bottom(),
"Merge of maps will not generate bottom");
276 DATA_INVARIANT(result->verify(),
"Structural invariants maintained");
297 std::dynamic_pointer_cast<full_struct_abstract_objectt>(
mutable_clone());
299 bool is_modified =
visit_map(result->map, visitor);
301 return is_modified ? result : shared_from_this();
305 const exprt &name)
const
312 auto field_expr = field.second->to_predicate(field_name);
314 if(!field_expr.is_true())
315 all_predicates.push_back(field_expr);
318 if(all_predicates.empty())
320 if(all_predicates.size() == 1)
321 return all_predicates.front();
333 for(
auto const &
object : view)
335 if(visited.find(
object.second) == visited.end())
337 object.second->get_statistics(
statistics, visited, env, ns);
const componentst & components() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
sharing_ptrt< class abstract_objectt > abstract_object_pointert
virtual bool is_top() const
Find out if the abstract object is top.
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.
goto_programt::const_targett locationt
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, const widen_modet &widen_mode)
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
bool visit_map(mapt &map, const visitort &visitor)
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.
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
sharing_ptrt< full_struct_abstract_objectt > constant_struct_pointert
The type of an expression, extends irept.
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...
Base type for structs and unions.
abstract_object_pointert merge_constant_structs(constant_struct_pointert other, const widen_modet &widen_mode) const
Performs an element wise merge of the map for each struct.
virtual const typet & type() const
Get the real type of the variable this abstract object is representing.
sorted_viewt get_sorted_view() const
Convenience function to get a sorted view of the map elements.
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.
Base class for all expressions.
abstract_object_pointert write_location_context(const locationt &location) const override
Update the location context for an abstract object.
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 ...
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.
An abstraction of a structure that stores one abstract object per field.
std::vector< view_itemt > viewt
View of the key-value pairs in the map.
static combine_result merge(const abstract_object_pointert &op1, const abstract_object_pointert &op2, const locationt &merge_location, const widen_modet &widen_mode)
void statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
const exprt & compound() const
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.
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.
#define PRECONDITION(CONDITION)
An abstract version of a program environment.
void insert_or_replace(const key_type &k, valueU &&m)
bool empty() const
Check if map is empty.
const irep_idt & id() const
std::vector< exprt > operandst
abstract_object_pointert merge(const abstract_object_pointert &other, const widen_modet &widen_mode) const override
To merge an abstract object into this abstract object.
std::set< abstract_object_pointert > abstract_object_visitedt
Pure virtual interface required of a client that can apply a copy-on-write operation to a given abstr...
Extract member of struct or union.
Structure type, corresponds to C style structs.
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
abstract_object_pointert merge_location_context(const locationt &location) const override
Update the merge location context for an abstract object.
This is the basic interface of the abstract interpreter with default implementations of the core func...
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.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
irep_idt get_component_name() const
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
virtual bool is_bottom() const
Find out if the abstract object is bottom.
abstract_object_pointert object
exprt to_predicate_internal(const exprt &name) const override
to_predicate implementation - derived classes will override
The Boolean constant true.
bool verify() const override
Function: full_struct_abstract_objectt::verify.
API to expression classes.
static memory_sizet from_bytes(std::size_t bytes)
virtual internal_abstract_object_pointert mutable_clone() const
typet t
To enforce copy-on-write these are private and have read-only accessors.
optionalt< std::reference_wrapper< const mapped_type > > find(const key_type &k) const
Find element.