CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
two_value_pointer_abstract_object.h
Go to the documentation of this file.
1/*******************************************************************\
2
3 Module: analyses variable-sensitivity
4
5 Author: Thomas Kiley, thomas.kiley@diffblue.com
6
7\*******************************************************************/
8#ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_TWO_VALUE_POINTER_ABSTRACT_OBJECT_H
9#define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_TWO_VALUE_POINTER_ABSTRACT_OBJECT_H
10
12
14{
15public:
23
30 const exprt &expr,
31 const abstract_environmentt &environment,
32 const namespacet &ns);
33
36 const namespacet &ns) const override;
37
39 abstract_environmentt &environment,
40 const namespacet &ns,
41 const std::stack<exprt> &stack,
42 const abstract_object_pointert &value,
43 bool merging_write) const override;
44
46 const typet &new_type,
47 const abstract_environmentt &environment,
48 const namespacet &ns) const override;
49
51 const exprt &expr,
52 const std::vector<abstract_object_pointert> &operands,
53 const abstract_environmentt &environment,
54 const namespacet &ns) const override;
55
57 const exprt &expr,
58 const std::vector<abstract_object_pointert> &operands,
59 const abstract_environmentt &environment,
60 const namespacet &ns) const override;
61};
62
63#endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_TWO_VALUE_POINTER_ABSTRACT_OBJECT_H
sharing_ptrt< class abstract_objectt > abstract_object_pointert
The base of all pointer abstractions.
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
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.
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