cprover
Loading...
Searching...
No Matches
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:
18
26
33 const exprt &expr,
34 const abstract_environmentt &environment,
35 const namespacet &ns);
36
38 const abstract_environmentt &env,
39 const namespacet &ns) const override;
40
42 abstract_environmentt &environment,
43 const namespacet &ns,
44 const std::stack<exprt> &stack,
45 const abstract_object_pointert &value,
46 bool merging_write) const override;
47
49 const typet &new_type,
50 const abstract_environmentt &environment,
51 const namespacet &ns) const override;
52
54 const exprt &expr,
55 const std::vector<abstract_object_pointert> &operands,
56 const abstract_environmentt &environment,
57 const namespacet &ns) const override;
58
60 const exprt &expr,
61 const std::vector<abstract_object_pointert> &operands,
62 const abstract_environmentt &environment,
63 const namespacet &ns) const override;
64};
65
66#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.
Base class for all expressions.
Definition expr.h:54
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