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
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
32simple_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:1353
const irep_idt & id() const
Definition: irep.h:396
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:2874
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:48
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:1391
Represents an entry in the write_stackt.