CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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:
45
48 const exprt &expr,
49 const abstract_environmentt &environment,
50 const namespacet &ns)
51 : context_abstract_objectt(child, expr, environment, ns)
52 {
53 }
54
56 {
57 }
58
59 // Standard abstract_objectt interface
60
61 bool has_been_modified(const abstract_object_pointert &before) const override;
62
64
65 void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns)
66 const override;
67
68protected:
70
72 const abstract_object_pointert &other,
73 const widen_modet &widen_mode) const override;
75 meet(const abstract_object_pointert &other) const override;
76
78 const abstract_object_pointert &other) const override;
79
81 abstract_environmentt &environment,
82 const namespacet &ns,
83 const std::stack<exprt> &stack,
84 const exprt &specifier,
85 const abstract_object_pointert &value,
86 bool merging_write) const override;
87
88 static void
89 output_last_written_locations(std::ostream &out, const locationst &locations);
90
93
94private:
96 const abstract_object_pointert &op1,
97 const abstract_object_pointert &op2)>;
99 std::shared_ptr<const write_location_contextt>;
100
103
104 // To enforce copy-on-write these are private and have read-only accessors
106
109};
110
111#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:117
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
std::shared_ptr< context_abstract_objectt > context_abstract_object_ptrt
std::set< locationt, goto_programt::target_less_than > locationst
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:56
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...
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.
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.