cprover
write_stack_entry.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3  Module: Analyses Variable Sensitivity
4 
5  Author: DiffBlue Limited.
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_WRITE_STACK_ENTRY_H
13 #define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_WRITE_STACK_ENTRY_H
14 
15 #include <memory>
16 #include <stack>
17 
19 #include <util/namespace.h>
20 #include <util/std_expr.h>
21 
23 {
24 public:
25  virtual ~write_stack_entryt() = default;
26  virtual exprt get_access_expr() const = 0;
27  virtual void adjust_access_type(exprt &expr) const = 0;
28  virtual bool try_squash_in(
29  std::shared_ptr<const write_stack_entryt> new_entry,
30  const abstract_environmentt &enviroment,
31  const namespacet &ns);
32 };
33 
35 {
36 public:
37  explicit simple_entryt(exprt expr);
38  exprt get_access_expr() const override;
39  void adjust_access_type(exprt &expr) const override;
40 
41 private:
43 };
44 
46 {
47 public:
48  explicit offset_entryt(abstract_object_pointert offset_value);
49  exprt get_access_expr() const override;
50  void adjust_access_type(exprt &expr) const override;
51  bool try_squash_in(
52  std::shared_ptr<const write_stack_entryt> new_entry,
53  const abstract_environmentt &enviroment,
54  const namespacet &ns) override;
55 
56 private:
58 };
59 
60 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_WRITE_STACK_ENTRY_H
simple_entryt
Definition: write_stack_entry.h:35
write_stack_entryt::try_squash_in
virtual bool try_squash_in(std::shared_ptr< const write_stack_entryt > new_entry, const abstract_environmentt &enviroment, const namespacet &ns)
Try to combine a new stack element with the current top of the stack.
Definition: write_stack_entry.cpp:23
simple_entryt::adjust_access_type
void adjust_access_type(exprt &expr) const override
For a simple entry, no type adjustment is needed for the access expression.
Definition: write_stack_entry.cpp:48
abstract_object_pointert
sharing_ptrt< class abstract_objectt > abstract_object_pointert
Definition: abstract_object.h:75
offset_entryt::offset
abstract_object_pointert offset
Definition: write_stack_entry.h:57
offset_entryt
Definition: write_stack_entry.h:46
write_stack_entryt
Definition: write_stack_entry.h:23
abstract_environmentt
Definition: abstract_environment.h:36
exprt
Base class for all expressions.
Definition: expr.h:54
namespace.h
write_stack_entryt::get_access_expr
virtual exprt get_access_expr() const =0
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
write_stack_entryt::adjust_access_type
virtual void adjust_access_type(exprt &expr) const =0
write_stack_entryt::~write_stack_entryt
virtual ~write_stack_entryt()=default
simple_entryt::simple_entry
exprt simple_entry
Definition: write_stack_entry.h:42
abstract_environment.h
An abstract version of a program environment.
simple_entryt::simple_entryt
simple_entryt(exprt expr)
Build a simple entry based off a single expression.
Definition: write_stack_entry.cpp:33
offset_entryt::try_squash_in
bool try_squash_in(std::shared_ptr< const write_stack_entryt > new_entry, const abstract_environmentt &enviroment, const namespacet &ns) override
Try to combine a new stack element with the current top of the stack.
Definition: write_stack_entry.cpp:92
offset_entryt::adjust_access_type
void adjust_access_type(exprt &expr) const override
For an offset entry, the type of the access expression can only be determined once the access express...
Definition: write_stack_entry.cpp:79
offset_entryt::offset_entryt
offset_entryt(abstract_object_pointert offset_value)
Definition: write_stack_entry.cpp:52
offset_entryt::get_access_expr
exprt get_access_expr() const override
Get the expression part needed to read this stack entry.
Definition: write_stack_entry.cpp:68
simple_entryt::get_access_expr
exprt get_access_expr() const override
Get the expression part needed to read this stack entry.
Definition: write_stack_entry.cpp:42
std_expr.h
API to expression classes.