82 std::cout <<
"Reading component " <<
member_expr.get_component_name() <<
'\n';
100 return value.value();
113 const std::stack<exprt> &stack,
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());
137 if(!old_value.has_value())
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");
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());
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());
305 const exprt &name)
const
333 for(
auto const &
object :
view)
335 if(visited.find(
object.second) == visited.end())
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...
ait supplies three of the four components needed: an abstract interpreter (in this case handling 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.
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.
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.
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...