cprover
Loading...
Searching...
No Matches
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{
20public:
21 typedef std::vector<std::shared_ptr<write_stack_entryt>>
23
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;
36 bool is_top_value() const;
37
38private:
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
65
67 const exprt &expr,
70
73};
74
75#endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_WRITE_STACK_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
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
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.
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.
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.