cprover
write_stack_entry.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3  Module: Analyses Variable Sensitivity
4 
5  Author: DiffBlue Limited.
6 
7 \*******************************************************************/
8 
11 
12 #include <unordered_set>
13 
14 #include <util/std_expr.h>
15 
16 #include "write_stack_entry.h"
17 
24  std::shared_ptr<const write_stack_entryt> new_entry,
25  const abstract_environmentt &enviroment,
26  const namespacet &ns)
27 {
28  return false;
29 }
30 
33 simple_entryt::simple_entryt(exprt expr) : simple_entry(expr)
34 {
35  // Invalid simple expression added to the stack
36  PRECONDITION(expr.id() == ID_member || expr.id() == ID_symbol);
37 }
38 
43 {
44  return simple_entry;
45 }
46 
49 {
50 }
51 
53  : offset(offset_value)
54 {
55  // The type of the abstract object should be an integral number
56  static const std::unordered_set<irep_idt, irep_id_hash> integral_types = {
57  ID_signedbv, ID_unsignedbv, ID_integer};
59  integral_types.find(offset_value->type().id()) != integral_types.cend());
60 }
61 
69 {
70  // This constructs a something that is basicallyt '(null)[offset])'
71  // meaning that we don't know what the type is at this point, as the
72  // array part will be filled in later.
73  return index_exprt(nil_exprt(), offset->to_constant());
74 }
75 
80 {
81  PRECONDITION(expr.id() == ID_index);
82  expr.type() = to_index_expr(expr).array().type().subtype();
83 }
84 
93  std::shared_ptr<const write_stack_entryt> new_entry,
94  const abstract_environmentt &enviroment,
95  const namespacet &ns)
96 {
97  std::shared_ptr<const offset_entryt> cast_entry =
98  std::dynamic_pointer_cast<const offset_entryt>(new_entry);
99  if(cast_entry)
100  {
101  plus_exprt result_offset(
102  cast_entry->offset->to_constant(), offset->to_constant());
103  offset = enviroment.eval(result_offset, ns);
104  return true;
105  }
106  return false;
107 }
write_stack_entryt::try_squash_in
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.
Definition: write_stack_entry.cpp:23
simple_entryt::adjust_access_type
void adjust_access_type(exprt &expr) const override
For a simple entry, no type adjustment is needed for the access expression.
Definition: write_stack_entry.cpp:48
typet::subtype
const typet & subtype() const
Definition: type.h:47
abstract_object_pointert
sharing_ptrt< class abstract_objectt > abstract_object_pointert
Definition: abstract_object.h:75
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1296
offset_entryt::offset
abstract_object_pointert offset
Definition: write_stack_entry.h:57
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:830
abstract_environmentt
Definition: abstract_environment.h:36
exprt
Base class for all expressions.
Definition: expr.h:54
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
simple_entryt::simple_entry
exprt simple_entry
Definition: write_stack_entry.h:42
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
nil_exprt
The NIL expression.
Definition: std_expr.h:2734
simple_entryt::simple_entryt
simple_entryt(exprt expr)
Build a simple entry based off a single expression.
Definition: write_stack_entry.cpp:33
offset_entryt::try_squash_in
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.
Definition: write_stack_entry.cpp:92
index_exprt::array
exprt & array()
Definition: std_expr.h:1258
abstract_environmentt::eval
virtual abstract_object_pointert eval(const exprt &expr, const namespacet &ns) const
These three are really the heart of the method.
Definition: abstract_environment.cpp:37
irept::id
const irep_idt & id() const
Definition: irep.h:407
offset_entryt::adjust_access_type
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...
Definition: write_stack_entry.cpp:79
offset_entryt::offset_entryt
offset_entryt(abstract_object_pointert offset_value)
Definition: write_stack_entry.cpp:52
offset_entryt::get_access_expr
exprt get_access_expr() const override
Get the expression part needed to read this stack entry.
Definition: write_stack_entry.cpp:68
simple_entryt::get_access_expr
exprt get_access_expr() const override
Get the expression part needed to read this stack entry.
Definition: write_stack_entry.cpp:42
index_exprt
Array index operator.
Definition: std_expr.h:1242
std_expr.h
API to expression classes.
write_stack_entry.h
Represents an entry in the write_stackt.