cprover
write_stack.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3  Module: Variable Sensitivity Domain
4 
5  Author: DiffBlue Limited.
6 
7 \*******************************************************************/
8 
12 
13 #ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_WRITE_STACK_H
14 #define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_WRITE_STACK_H
15 
17 
19 {
20 public:
21  typedef std::vector<std::shared_ptr<write_stack_entryt>>
23 
24  write_stackt();
25 
27  const exprt &expr,
28  const abstract_environmentt &environment,
29  const namespacet &ns);
30 
31  exprt to_expression() const;
32 
33  size_t depth() const;
34  exprt target_expression(size_t depth) const;
35  exprt offset_expression() const;
36  bool is_top_value() const;
37 
38 private:
40  const exprt &expr,
41  const abstract_environmentt &environment,
42  const namespacet &ns);
43 
45  const exprt &expr,
46  const abstract_environmentt &environment,
47  const namespacet &ns);
48 
50  const index_exprt &expr,
51  const abstract_environmentt &environment,
52  const namespacet &ns);
53 
54  void add_to_stack(
55  std::shared_ptr<write_stack_entryt> entry_pointer,
56  const abstract_environmentt environment,
57  const namespacet &ns);
58 
59  enum class integral_resultt
60  {
64  };
65 
67  const exprt &expr,
68  exprt &out_base_expr,
69  exprt &out_integral_expr);
70 
72  bool top_stack;
73 };
74 
75 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_WRITE_STACK_H
Base class for all expressions.
Definition: expr.h:54
Array index operator.
Definition: std_expr.h:1328
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
bool top_stack
Definition: write_stack.h:72
void construct_stack_to_array_index(const index_exprt &expr, const abstract_environmentt &environment, const namespacet &ns)
Construct a stack for an array position l-value.
exprt target_expression(size_t depth) const
exprt offset_expression() const
static integral_resultt get_which_side_integral(const exprt &expr, exprt &out_base_expr, exprt &out_integral_expr)
Utility function to find out which side of a binary operation has an integral type,...
void construct_stack_to_lvalue(const exprt &expr, const abstract_environmentt &environment, const namespacet &ns)
Construct a stack up to a specific l-value (i.e.
write_stackt()
Build a topstack.
Definition: write_stack.cpp:25
bool is_top_value() const
Is the stack representing an unknown value and hence can't be written to or read from.
exprt to_expression() const
Convert the stack to an expression that can be used to write to.
void construct_stack_to_pointer(const exprt &expr, const abstract_environmentt &environment, const namespacet &ns)
Add to the stack the elements to get to a pointer.
Definition: write_stack.cpp:59
size_t depth() const
continuation_stack_storet stack
Definition: write_stack.h:71
void add_to_stack(std::shared_ptr< write_stack_entryt > entry_pointer, const abstract_environmentt environment, const namespacet &ns)
Add an element to the top of the stack.
std::vector< std::shared_ptr< write_stack_entryt > > continuation_stack_storet
Definition: write_stack.h:22
Represents an entry in the write_stackt.