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 "abstract_environment.h"
15 #include "write_stack_entry.h"
16 
23  std::shared_ptr<const write_stack_entryt> new_entry,
24  const abstract_environmentt &enviroment,
25  const namespacet &ns)
26 {
27  return false;
28 }
29 
32 simple_entryt::simple_entryt(exprt expr) : simple_entry(expr)
33 {
34  // Invalid simple expression added to the stack
36  expr.id() == ID_member || expr.id() == ID_symbol ||
37  expr.id() == ID_dynamic_object);
38 }
39 
44 {
45  return simple_entry;
46 }
47 
50 {
51 }
52 
54  : offset(offset_value)
55 {
56  // The type of the abstract object should be an integral number
57  static const std::unordered_set<irep_idt, irep_id_hash> integral_types = {
58  ID_signedbv, ID_unsignedbv, ID_integer};
60  integral_types.find(offset_value->type().id()) != integral_types.cend());
61 }
62 
70 {
71  // This constructs a something that is basicallyt '(null)[offset])'
72  // meaning that we don't know what the type is at this point, as the
73  // array part will be filled in later.
74  return index_exprt(nil_exprt(), offset->to_constant());
75 }
76 
81 {
82  PRECONDITION(expr.id() == ID_index);
83  expr.type() = to_index_expr(expr).array().type().subtype();
84 }
85 
94  std::shared_ptr<const write_stack_entryt> new_entry,
95  const abstract_environmentt &enviroment,
96  const namespacet &ns)
97 {
98  std::shared_ptr<const offset_entryt> cast_entry =
99  std::dynamic_pointer_cast<const offset_entryt>(new_entry);
100  if(cast_entry)
101  {
102  plus_exprt result_offset(
103  cast_entry->offset->to_constant(), offset->to_constant());
104  offset = enviroment.eval(result_offset, ns);
105  return true;
106  }
107  return false;
108 }
An abstract version of a program environment.
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:1328
exprt & array()
Definition: std_expr.h:1344
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:91
The NIL expression.
Definition: std_expr.h:2820
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:914
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:463
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1382
Represents an entry in the write_stackt.