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 "abstract_object.h"
16 
18 class namespacet;
19 
21 {
22 public:
23  virtual ~write_stack_entryt() = default;
24  virtual exprt get_access_expr() const = 0;
25  virtual void adjust_access_type(exprt &expr) const = 0;
26  virtual bool try_squash_in(
27  std::shared_ptr<const write_stack_entryt> new_entry,
28  const abstract_environmentt &enviroment,
29  const namespacet &ns);
30 };
31 
33 {
34 public:
35  explicit simple_entryt(exprt expr);
36  exprt get_access_expr() const override;
37  void adjust_access_type(exprt &expr) const override;
38 
39 private:
41 };
42 
44 {
45 public:
46  explicit offset_entryt(abstract_object_pointert offset_value);
47  exprt get_access_expr() const override;
48  void adjust_access_type(exprt &expr) const override;
49  bool try_squash_in(
50  std::shared_ptr<const write_stack_entryt> new_entry,
51  const abstract_environmentt &enviroment,
52  const namespacet &ns) override;
53 
54 private:
56 };
57 
58 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_WRITE_STACK_ENTRY_H
abstract_objectt is the top of the inheritance heirarchy of objects used to represent individual vari...
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:91
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.