CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
two_value_pointer_abstract_object.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3 Module: analyses variable-sensitivity
4
5 Author: Jez Higgins
6
7\*******************************************************************/
8
11
12#include <util/pointer_expr.h>
13
15 const typet &type,
16 bool top,
17 bool bottom)
18 : abstract_pointer_objectt(type, top, bottom)
19{
20}
21
23 const exprt &expr,
24 const abstract_environmentt &environment,
25 const namespacet &ns)
26 : abstract_pointer_objectt(expr, environment, ns)
27{
28}
29
39
42 const namespacet &ns,
43 const std::stack<exprt> &stack,
44 const abstract_object_pointert &value,
45 bool merging_write) const
46{
47 if(is_top() || is_bottom())
48 {
49 env.havoc("Writing to a 2value pointer");
50 return shared_from_this();
51 }
52
53 return std::make_shared<two_value_pointer_abstract_objectt>(
54 type(), true, false);
55}
56
58 const typet &new_type,
59 const abstract_environmentt &environment,
60 const namespacet &ns) const
61{
62 INVARIANT(is_void_pointer(type()), "Only allow pointer casting from void*");
63 return std::make_shared<two_value_pointer_abstract_objectt>(
65}
66
68 const exprt &expr,
69 const std::vector<abstract_object_pointert> &operands,
70 const abstract_environmentt &environment,
71 const namespacet &ns) const
72{
73 return environment.eval(nil_exprt(), ns);
74}
75
77 const exprt &expr,
78 const std::vector<abstract_object_pointert> &operands,
79 const abstract_environmentt &environment,
80 const namespacet &ns) const
81{
82 return nil_exprt();
83}
An abstract version of a program environment.
sharing_ptrt< class abstract_objectt > abstract_object_pointert
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:235
virtual abstract_object_pointert eval(const exprt &expr, const namespacet &ns) const
These three are really the heart of the method.
virtual bool is_top() const
Find out if the abstract object is top.
virtual bool is_bottom() const
Find out if the abstract object is bottom.
virtual const typet & type() const
Get the real type of the variable this abstract object is representing.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Base class for all expressions.
Definition expr.h:56
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:3208
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
const typet & base_type() const
The type of the data what we point to.
abstract_object_pointert write_dereference(abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const abstract_object_pointert &value, bool merging_write) const override
Evaluate writing to a pointer's value.
abstract_object_pointert typecast(const typet &new_type, const abstract_environmentt &environment, const namespacet &ns) const override
abstract_object_pointert read_dereference(const abstract_environmentt &env, const namespacet &ns) const override
A helper function to read elements from an array.
two_value_pointer_abstract_objectt(const typet &type, bool top, bool bottom)
Start the abstract object at either top or bottom or neither Asserts if both top and bottom are true.
abstract_object_pointert ptr_diff(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const override
exprt ptr_comparison_expr(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const override
The type of an expression, extends irept.
Definition type.h:29
API to expression classes for Pointers.
bool is_void_pointer(const typet &type)
This method tests, if the given typet is a pointer of type void.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423