cprover
Loading...
Searching...
No Matches
full_struct_abstract_object.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Struct abstract object
4
5Author: Thomas Kiley, thomas.kiley@diffblue.com
6
7\*******************************************************************/
8
11#ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_FULL_STRUCT_ABSTRACT_OBJECT_H
12#define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_FULL_STRUCT_ABSTRACT_OBJECT_H
13
15#include <iosfwd>
16#include <util/sharing_map.h>
17
19 full_struct_abstract_objectt,
20 struct_aggregate_typet>
21{
22public:
28
35
38
46
52 const exprt &expr,
53 const abstract_environmentt &environment,
54 const namespacet &ns);
55
64 void output(
65 std::ostream &out,
66 const class ai_baset &ai,
67 const class namespacet &ns) const override;
68
78 write_location_context(const locationt &location) const override;
80 merge_location_context(const locationt &location) const override;
81
94 visit_sub_elements(const abstract_object_visitort &visitor) const override;
95
96 void statistics(
99 const abstract_environmentt &env,
100 const namespacet &ns) const override;
101
102private:
103 // no entry means component is top
107
118 const widen_modet &widen_mode) const;
119
120protected:
121 CLONE
122
135 const abstract_environmentt &environment,
136 const exprt &expr,
137 const namespacet &ns) const override;
138
157 abstract_environmentt &environment,
158 const namespacet &ns,
159 const std::stack<exprt> &stack,
160 const exprt &expr,
161 const abstract_object_pointert &value,
162 bool merging_write) const override;
163
172 bool verify() const override;
173
183 const abstract_object_pointert &other,
184 const widen_modet &widen_mode) const override;
185
186 exprt to_predicate_internal(const exprt &name) const override;
187};
188
189#endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_FULL_STRUCT_ABSTRACT_OBJECT_H
Common behaviour for abstract objects modelling aggregate values - arrays, structs,...
std::shared_ptr< const T > sharing_ptrt
Merge is designed to allow different abstractions to be merged gracefully.
#define CLONE
std::set< abstract_object_pointert > abstract_object_visitedt
sharing_ptrt< class abstract_objectt > abstract_object_pointert
goto_programt::const_targett locationt
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...
Definition ai.h:119
Base class for all expressions.
Definition expr.h:54
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_aggregate_objectt< full_struct_abstract_objectt, struct_aggregate_typet > abstract_aggregate_baset
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.
sharing_mapt< irep_idt, abstract_object_pointert, false, irep_id_hash > shared_struct_mapt
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
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
A map implemented as a tree where subtrees can be shared between different maps.
The type of an expression, extends irept.
Definition type.h:29
Sharing map.
Pure virtual interface required of a client that can apply a copy-on-write operation to a given abstr...