cprover
data_dependency_context.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: analyses variable-sensitivity data_dependency_context
4
5Author: Diffblue Ltd
6
7\*******************************************************************/
8
14#ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_DATA_DEPENDENCY_CONTEXT_H
15#define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_DATA_DEPENDENCY_CONTEXT_H
16
18
20{
21public:
22 // These constructors mirror those in the base abstract_objectt, but with
23 // the addition of an extra argument which is the abstract_objectt to wrap.
25 const abstract_object_pointert child,
26 const typet &type)
28 {
29 }
30
32 const abstract_object_pointert child,
33 const typet &type,
34 bool top,
35 bool bottom)
37 {
38 }
39
41 const abstract_object_pointert child,
42 const exprt &expr,
43 const abstract_environmentt &environment,
44 const namespacet &ns)
45 : write_location_contextt(child, expr, environment, ns)
46 {
47 }
48
50 abstract_environmentt &environment,
51 const namespacet &ns,
52 const std::stack<exprt> &stack,
53 const exprt &specifier,
54 const abstract_object_pointert &value,
55 bool merging_write) const override;
56
57 bool has_been_modified(const abstract_object_pointert &before) const override;
58
59 std::set<goto_programt::const_targett> get_data_dependencies() const;
60 std::set<goto_programt::const_targett> get_data_dominators() const;
61
62 void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns)
63 const override;
64
65protected:
66 CLONE
67
69 const abstract_object_pointert &other,
70 const widen_modet &widen_mode) const override;
72 meet(const abstract_object_pointert &other) const override;
73
75 const abstract_object_pointert &other) const override;
76
77private:
79 std::shared_ptr<const data_dependency_contextt>;
80
83 const data_dependency_context_ptrt &parent) const;
84
86 {
87 public:
90 goto_programt::const_targett other_instruction) const
91 {
92 return instruction->location_number > other_instruction->location_number;
93 }
94 };
95 typedef std::set<goto_programt::const_targett, location_ordert> dependenciest;
98
100 insert_data_deps(const dependenciest &dependencies) const;
101
103 update_location_context_internal(const locationst &locations) const override;
104
105 void set_data_deps(const locationst &locations);
106 void set_data_deps(const dependenciest &dependences);
107};
108
109#endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_DATA_DEPENDENCY_CONTEXT_H
#define CLONE
sharing_ptrt< class abstract_objectt > abstract_object_pointert
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:119
std::shared_ptr< context_abstract_objectt > context_abstract_object_ptrt
std::set< locationt > locationst
const typet & type() const override
Get the real type of the variable this abstract object is representing.
bool operator()(goto_programt::const_targett instruction, goto_programt::const_targett other_instruction) const
std::set< goto_programt::const_targett > get_data_dominators() const
Return the set of data dominators associated with this node.
CLONE abstract_object_pointert merge(const abstract_object_pointert &other, const widen_modet &widen_mode) const override
Create a new abstract object that is the result of merging this abstract object with a given abstract...
data_dependency_contextt(const abstract_object_pointert child, const typet &type, bool top, bool bottom)
std::set< goto_programt::const_targett > get_data_dependencies() const
Return the set of data dependencies associated with this node.
bool has_been_modified(const abstract_object_pointert &before) const override
Determine whether 'this' abstract_object has been modified in comparison to a previous 'before' state...
void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns) const override
Output a representation of the value of this abstract object.
data_dependency_contextt(const abstract_object_pointert child, const exprt &expr, const abstract_environmentt &environment, const namespacet &ns)
abstract_object_pointert insert_data_deps(const dependenciest &dependencies) const
Insert the given set of data dependencies into the data dependencies set for this data_dependency_con...
abstract_object_pointert abstract_object_merge_internal(const abstract_object_pointert &other) const override
Helper function for abstract_objectt::abstract_object_merge to perform any additional actions after t...
std::shared_ptr< const data_dependency_contextt > data_dependency_context_ptrt
abstract_object_pointert write(abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const exprt &specifier, const abstract_object_pointert &value, bool merging_write) const override
A helper function to evaluate writing to a component of an abstract object.
data_dependency_contextt(const abstract_object_pointert child, const typet &type)
context_abstract_object_ptrt update_location_context_internal(const locationst &locations) const override
abstract_object_pointert combine(const data_dependency_context_ptrt &other, const data_dependency_context_ptrt &parent) const
void set_data_deps(const locationst &locations)
Set the given set of data dependencies for from the locations.
abstract_object_pointert meet(const abstract_object_pointert &other) const override
Base implementation of the meet operation: only used if no more precise abstraction can be used,...
std::set< goto_programt::const_targett, location_ordert > dependenciest
Base class for all expressions.
Definition: expr.h:54
instructionst::const_iterator const_targett
Definition: goto_program.h:593
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
General implementation of an abstract_objectt which tracks the last written locations for a given abs...
Maintain a context in the variable sensitvity domain that records write locations for a given abstrac...