cprover
full_struct_abstract_object.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Struct abstract object
4 
5 Author: 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 {
22 public:
28 
35 
37  explicit full_struct_abstract_objectt(const typet &type);
38 
45  full_struct_abstract_objectt(const typet &type, bool top, bool bottom);
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(
98  abstract_object_visitedt &visited,
99  const abstract_environmentt &env,
100  const namespacet &ns) const override;
101 
102 private:
103  // no entry means component is top
107 
118  const widen_modet &widen_mode) const;
119 
120 protected:
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
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
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
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...