cprover
Loading...
Searching...
No Matches
write_location_context.h
Go to the documentation of this file.
1/*******************************************************************\
2
3 Module: analyses variable-sensitivity write_location_context
4
5 Author: Diffblue Ltd.
6
7\*******************************************************************/
8
16#ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_WRITE_LOCATION_CONTEXT_H
17#define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_WRITE_LOCATION_CONTEXT_H
18
20#include <iostream>
21#include <stack>
22
35{
36public:
38 const abstract_object_pointert child,
39 const typet &type)
41 {
42 }
43
45 const abstract_object_pointert child,
46 const typet &type,
47 bool top,
48 bool bottom)
50 {
51 }
52
54 const abstract_object_pointert child,
55 const exprt &expr,
56 const abstract_environmentt &environment,
57 const namespacet &ns)
58 : context_abstract_objectt(child, expr, environment, ns)
59 {
60 }
61
63 {
64 }
65
66 // Standard abstract_objectt interface
67
68 bool has_been_modified(const abstract_object_pointert &before) const override;
69
70 locationst get_location_union(const locationst &locations) const;
71
72 void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns)
73 const override;
74
75protected:
76 CLONE
77
79 const abstract_object_pointert &other,
80 const widen_modet &widen_mode) const override;
82 meet(const abstract_object_pointert &other) const override;
83
85 const abstract_object_pointert &other) const override;
86
88 abstract_environmentt &environment,
89 const namespacet &ns,
90 const std::stack<exprt> &stack,
91 const exprt &specifier,
92 const abstract_object_pointert &value,
93 bool merging_write) const override;
94
95 static void
96 output_last_written_locations(std::ostream &out, const locationst &locations);
97
99 void set_last_written_locations(const locationst &locations);
100
101private:
103 const abstract_object_pointert &op1,
104 const abstract_object_pointert &op2)>;
106 std::shared_ptr<const write_location_contextt>;
107
109 combine(const write_location_context_ptrt &other, combine_fn fn) const;
110
111 // To enforce copy-on-write these are private and have read-only accessors
113
115 update_location_context_internal(const locationst &locations) const override;
116};
117
118#endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_WRITE_LOCATION_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
const typet & type() const override
Get the real type of the variable this abstract object is representing.
Base class for all expressions.
Definition expr.h:54
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...
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...
std::function< abstract_objectt::combine_result(const abstract_object_pointert &op1, const abstract_object_pointert &op2)> combine_fn
write_location_contextt(const abstract_object_pointert child, const typet &type, bool top, bool bottom)
virtual locationst get_last_written_locations() const
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...
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.
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,...
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.
write_location_contextt(const abstract_object_pointert child, const exprt &expr, const abstract_environmentt &environment, const namespacet &ns)
static void output_last_written_locations(std::ostream &out, const locationst &locations)
Internal helper function to format and output a given set of locations.
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...
locationst get_location_union(const locationst &locations) const
Construct the union of the location set of the current object, and a the provided location set.
write_location_contextt(const abstract_object_pointert child, const typet &type)
void set_last_written_locations(const locationst &locations)
Sets the last written locations for this context.
std::shared_ptr< const write_location_contextt > write_location_context_ptrt
context_abstract_object_ptrt update_location_context_internal(const locationst &locations) const override
abstract_object_pointert combine(const write_location_context_ptrt &other, combine_fn fn) const
General implementation of a an abstract_objectt which can track side information in the form of a 'co...
Clones the first parameter and merges it with the second.