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 }
sharing_ptrt< class abstract_objectt > abstract_object_pointert
virtual abstract_object_pointert eval(const exprt &expr, const namespacet &ns) const
These three are really the heart of the method.
Base class for all expressions.
Definition: expr.h:54
typet & type()
Return the type of the expression.
Definition: expr.h:82
Array index operator.
Definition: std_expr.h:1243
exprt & array()
Definition: std_expr.h:1259
const irep_idt & id() const
Definition: irep.h:407
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
The NIL expression.
Definition: std_expr.h:2735
offset_entryt(abstract_object_pointert offset_value)
exprt get_access_expr() const override
Get the expression part needed to read this stack entry.
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.
abstract_object_pointert offset
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...
The plus expression Associativity is not specified.
Definition: std_expr.h:831
void adjust_access_type(exprt &expr) const override
For a simple entry, no type adjustment is needed for the access expression.
exprt get_access_expr() const override
Get the expression part needed to read this stack entry.
simple_entryt(exprt expr)
Build a simple entry based off a single expression.
const typet & subtype() const
Definition: type.h:47
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.
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
API to expression classes.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1297
Represents an entry in the write_stackt.