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
write_stackt::integral_resultt::LHS_INTEGRAL
@ LHS_INTEGRAL
write_stackt::is_top_value
bool is_top_value() const
Is the stack representing an unknown value and hence can't be written to or read from.
Definition: write_stack.cpp:207
write_stackt::integral_resultt::RHS_INTEGRAL
@ RHS_INTEGRAL
abstract_environmentt
Definition: abstract_environment.h:36
exprt
Base class for all expressions.
Definition: expr.h:54
write_stackt::continuation_stack_storet
std::vector< std::shared_ptr< write_stack_entryt > > continuation_stack_storet
Definition: write_stack.h:22
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
write_stackt::top_stack
bool top_stack
Definition: write_stack.h:68
write_stackt
Definition: write_stack.h:19
write_stackt::construct_stack_to_lvalue
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.
Definition: write_stack.cpp:127
write_stackt::construct_stack_to_pointer
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
write_stackt::get_which_side_integral
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,...
Definition: write_stack.cpp:237
write_stackt::construct_stack_to_array_index
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.
Definition: write_stack.cpp:159
write_stackt::integral_resultt::NEITHER_INTEGRAL
@ NEITHER_INTEGRAL
index_exprt
Array index operator.
Definition: std_expr.h:1243
write_stackt::integral_resultt
integral_resultt
Definition: write_stack.h:56
write_stackt::write_stackt
write_stackt()
Build a topstack.
Definition: write_stack.cpp:24
write_stackt::add_to_stack
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.
Definition: write_stack.cpp:217
write_stackt::to_expression
exprt to_expression() const
Convert the stack to an expression that can be used to write to.
Definition: write_stack.cpp:174
write_stackt::stack
continuation_stack_storet stack
Definition: write_stack.h:67
write_stack_entry.h
Represents an entry in the write_stackt.