50 bool did_initialize_values =
false;
51 auto struct_type_it = struct_type_def.
components().begin();
53 ++param_it, ++struct_type_it)
56 struct_type_it->get_name(),
58 did_initialize_values =
true;
61 if(did_initialize_values)
99 member_expr.
type(), ns,
true,
false);
107 const std::stack<exprt> &stack,
110 bool merging_write)
const
119 return std::make_shared<full_struct_abstract_objectt>(
124 std::dynamic_pointer_cast<full_struct_abstract_objectt>(
mutable_clone());
130 auto const old_value =
map.
find(c);
131 if(!old_value.has_value())
134 member_expr.
type(), ns,
true,
false);
136 c, environment.
write(starting_value, value, stack, ns, merging_write));
142 environment.
write(old_value.value(), value, stack, ns, merging_write));
145 result->set_not_top();
146 DATA_INVARIANT(result->verify(),
"Structural invariants maintained");
152 std::cout <<
"Setting component" << std::endl;
156 auto const old_value = result->map.find(c);
162 DATA_INVARIANT(result->verify(),
"Structural invariants maintained");
166 INVARIANT(!result->map.empty(),
"If not top, map cannot be empty");
168 if(!old_value.has_value())
170 DATA_INVARIANT(result->verify(),
"Structural invariants maintained");
181 if(old_value.has_value())
183 result->map.replace(c, value);
187 result->map.insert(c, value);
189 result->set_not_top();
190 INVARIANT(!result->is_bottom(),
"top != bottom");
193 DATA_INVARIANT(result->verify(),
"Structural invariants maintained");
212 for(
const auto &field : type_decl.
components())
214 auto value =
map.
find(field.get_name());
215 if(value.has_value())
221 out <<
'.' << field.get_name() <<
'=';
242 std::dynamic_pointer_cast<const full_struct_abstract_objectt>(other);
254 return std::make_shared<full_struct_abstract_objectt>(*other);
257 std::dynamic_pointer_cast<full_struct_abstract_objectt>(
mutable_clone());
264 return shared_from_this();
268 INVARIANT(!result->is_top(),
"Merge of maps will not generate top");
269 INVARIANT(!result->is_bottom(),
"Merge of maps will not generate bottom");
270 DATA_INVARIANT(result->verify(),
"Structural invariants maintained");
291 std::dynamic_pointer_cast<full_struct_abstract_objectt>(
mutable_clone());
293 bool is_modified =
visit_map(result->map, visitor);
295 return is_modified ? result : shared_from_this();
299 const exprt &name)
const
307 member_exprt(name, compound_type.get_component(field.first));
308 auto field_expr = field.second->to_predicate(field_name);
310 if(!field_expr.is_true())
311 all_predicates.push_back(field_expr);
314 if(all_predicates.empty())
316 if(all_predicates.size() == 1)
317 return all_predicates.front();
329 for(
auto const &
object : view)
331 if(visited.find(
object.second) == visited.end())
333 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, const widen_modet &widen_mode)
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
goto_programt::const_targett locationt
static combine_result merge(const abstract_object_pointert &op1, const abstract_object_pointert &op2, const locationt &merge_location, const widen_modet &widen_mode)
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.
std::vector< exprt > operandst
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 write_location_context(const locationt &location) const override
Update the location context for an 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.
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.
abstract_object_pointert merge_location_context(const locationt &location) const override
Update the merge location context for an 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(const abstract_object_pointert &other, const widen_modet &widen_mode) const override
To merge an abstract object into this abstract object.
exprt to_predicate_internal(const exprt &name) const override
to_predicate implementation - derived classes will override
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
bool empty() const
Check if map is empty.
sorted_viewt get_sorted_view() const
Convenience function to get a sorted view of the map elements.
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 Boolean constant true.
The type of an expression, extends irept.
An abstraction of a structure that stores one abstract object per field.
bool visit_map(mapt &map, const visitort &visitor)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
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...
abstract_object_pointert object