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  bool is_top_value() const;
33 
34 private:
36  const exprt &expr,
37  const abstract_environmentt &environment,
38  const namespacet &ns);
39 
41  const exprt &expr,
42  const abstract_environmentt &environment,
43  const namespacet &ns);
44 
46  const index_exprt &expr,
47  const abstract_environmentt &environment,
48  const namespacet &ns);
49 
50  void add_to_stack(
51  std::shared_ptr<write_stack_entryt> entry_pointer,
52  const abstract_environmentt environment,
53  const namespacet &ns);
54 
55  enum class integral_resultt
56  {
60  };
61 
63  const exprt &expr,
64  exprt &out_base_expr,
65  exprt &out_integral_expr);
66 
68  bool top_stack;
69 };
70 
71 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_WRITE_STACK_H
Base class for all expressions.
Definition: expr.h:54
Array index operator.
Definition: std_expr.h:1243
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
bool top_stack
Definition: write_stack.h:68
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.
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:24
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:58
continuation_stack_storet stack
Definition: write_stack.h:67
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.