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
An abstract version of a program environment.
sharing_ptrt< class abstract_objectt > abstract_object_pointert
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:92
offset_entryt(abstract_object_pointert offset_value)
exprt get_access_expr() const override
Get the expression part needed to read this stack entry.
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.
abstract_object_pointert offset
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...
void adjust_access_type(exprt &expr) const override
For a simple entry, no type adjustment is needed for the access expression.
exprt get_access_expr() const override
Get the expression part needed to read this stack entry.
simple_entryt(exprt expr)
Build a simple entry based off a single expression.
virtual void adjust_access_type(exprt &expr) const =0
virtual ~write_stack_entryt()=default
virtual exprt get_access_expr() const =0
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.
API to expression classes.