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
18class namespacet;
19
21{
22public:
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{
34public:
35 explicit simple_entryt(exprt expr);
36 exprt get_access_expr() const override;
37 void adjust_access_type(exprt &expr) const override;
38
39private:
41};
42
44{
45public:
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
54private:
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.